Portable build of progs/ and progs64/ directories

[andrew-appel]

Portable build of progs/ and progs64/ directories

[MSoegtropIMC]

I also came across this and wanted to create a CompCert and VST ARM Opam package. I dropped it since Timothy Carstens (@intoverflow) wanted to look into it, but since there is apparently no progress, I can pick this up again.

A mechanism to install multiple CompCert and VST versions is already prepared, although I still would like to have the discussed -V option in Coq to drag in variants without system dependent -Q paths.

Ideally we should also provide a simple emulator.

[andrew-appel]

Actually, I had in mind something different. This is only for the purpose of building the test cases in progs/ and progs64/ (and also sha, tweetnacl, etc.); and only for running clightgen, not for compiling to executable code. Once the .c files are clightgenned into .v files (and checked into the github repo), we don't need the underlying target-specific CompCert anymore; we can run the verifications of the testcases in a VST build with the internal "bundled" CompCert (which does not have a clightgen in it).
This means that a person wanting to rebuild the .c->.v files will just need to build two CompCert directories enough for clightgen, but will not need to install them in user-contrib. And the users of those .v files will not even need those clightgens.
What you suggest is perfectly reasonable, but it would be for a different purpose, I think

[MSoegtropIMC]

That doesn't seem to be very modular. Things should be done such that users can go through example files with checked in clightgen generated files with an installed VST (from CoqPlatform e.g.). As far as I can see what you suggest will only work with VST compiled from sources.

[andrew-appel]

Whether or not the clightgen comes from a platform-installed VST, there is still the other issue of include files. If I'm running on a Mac, using a clightgen built to target x86_32, where do the include files come from? My original note points out that CompCert suggests using a gcc cross-compile installation, but I'm suggesting intead that we build a special-purpose include directory for 32-bit test cases (progs/, sha/, etc.) and another for 64-bit test cases (progs64/, etc.).

[MSoegtropIMC]

Indeed the CompCert opam package would depend on a cross gcc opam package (which I would also provide).

With the process you suggest I see the issue that it will make it much harder for people to use VST on their own code (and compile it in the end). One would have to switch the header files then. Also one has to be very careful then to be sure about the meaning of the verification one did.

[andrew-appel]

OK, your plan looks good. It's not urgent, there are probably higher-priority things to worry about first. I will leave this issue open for now.