jasmin-lang
Eliminating all the proof parts of `make CIL`
Currently, the compilation of jasminc depends on proof files (psem.v, asmgen.v, linear_proof.v, etc.). This is due to the algorithmic and proof parts being mixed in such files. Extracting these parts and moving them, or splitting the files, should help clean the architecture and reduce the compilation time for those who do not need the proofs.
One difficult point is allocation.v, since it plays with functors. This seems doable, but the fully satisfying solution has not been found yet.
I’ve tried to improved on this in f4decb8bb00eddd237093cb3e3a36699fbb02bbb (branch glob_array3).
@vbgl A good first step. I did not look closely at the contents of the files, I guess you did nothing more than just splitting them. Probably the names of the files included in compiler_proof.v should be changed, but we can do that later when we completely fix the proof.
Exactly, I just moved things around. Many of these proofs indeed need to be reworked and the compiler-proof file is a big work-in-progress (in that branch).
I think so. The number of dependencies was reduced, but some of them are still there for no good reason. I need to check.