Added latest CompCert version (3.7) and platform Flocq variant

[MSoegtropIMC]

This adds a opam file for the latest version of CompCert (3.7) including a variant which is patched to use a platform supplied Flocq rather than the integrated Flocq.

The change to a platform supplied Flocq is done with a patch file for maintainability and cross platform reasons (sed is quite different on OSX).

The patched variant uses a tilde version name, so that users get the standard variant unless they explicitly request the patched variant.

FYI: @xavierleroy, @jhjourdan

[MSoegtropIMC]

@palmskog : can you please help me with the error message:

/builds/coq/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam: Errors.
              error 53: Mismatching 'extra-files:' field: "platform-flocq.patch"

I don't see what should be wrong with this. Locally this does work without a warning (and also does apply the patch) and I double checked the SHA256. What could be wrong with this?

[silene]

Is the uppercase Files intended? I would not be surprised if that is the cause for the failure.

[MSoegtropIMC]

Is the uppercase Files intended? I would not be surprised if that is the cause for the failure.

Thanks - well spotted. This is indeed the issue (OSX FS is by default also case insensitive).

[MSoegtropIMC]

Note: I added one more little patch which installs compcert.ini also under lib/coq/user-contrib/compcert, where coq based tools (like VST) can find it more reliably.

[jhjourdan]

Thanks for the work.

Concerning compcert.ini: I understand your desire, but I find it strange that this is something specific to the platform-coq variant. Could you add it to the default variant?

[jhjourdan]

This seems completely unrelated to installing compcert.ini at the right place.

[MSoegtropIMC]

Ehm yes, I also added a bitsize field to the file afterwards, since it was missing and VST needs it - and fixed the spacing on the way (it was a mix of tabs and spaces from one line to another).

[jhjourdan]

Same remark as bellow : if the patch (or PR AbsInt/CompCert#348) is not only about installing the .ini file, then document it accordingly.

[MSoegtropIMC]

Concerning compcert.ini: I understand your desire, but I find it strange that this is something specific to the platform-coq variant. Could you add it to the default variant?

I would prefer to have the 3.7 release a plain unmodified 3.7 release. I did so much patch hacking in all the Coq Windows releases I did in the past that I started to get nitpicky about such things. VST anyway won't work well with the non platform version and it requires the platform version as dependency (opam package is on the way), so I don't see a good reason to publish a patched release for compcert 3.7 on opam. I also created a PR for upstream CompCert (https://github.com/AbsInt/CompCert/pull/348/files) to have this in the future.

But this is more a 70% don't vs 30% do opinion, so if you have strong feelings about doing this for both, I am happy to do it.

[jhjourdan]

This is a matter of documentation. If the description of this variant is "using the platform supplied version of Flocq", then this is what the only difference with the main variant should be. So I think we should either change the description (and name) of the "flocq" variant into something like "variant patched for VST" or integrate this patch to the main variant.

Given that 1- the patch may be integrated to CompCert (thanks to AbsInt/CompCert#348) and 2- installing one more file and adding this line to a .ini file is unlikely to cause any incompatibility, I preferred patching the main variant.

[xavierleroy]

I would prefer to have the 3.7 release a plain unmodified 3.7 release

I would prefer this too.

If the description of this variant is "using the platform supplied version of Flocq", then this is what the only difference with the main variant should be. So I think we should either change the description (and name) of the "flocq" variant into something like "variant patched for VST" or integrate this patch to the main variant.

"CompCert patched for the needs of VST" would be a fine description of the alternative package.

Given that 1- the patch may be integrated to CompCert (thanks to AbsInt/CompCert#348) and 2- installing one more file and adding this line to a .ini file

I have reservations about adding stuff to a .ini file that is not configurable. I mean, the bit width is not a configuration parameter, it's a function of other parameters. Plus, it's already described in the Archi.v file of the target platform.

[MSoegtropIMC]

"CompCert patched for the needs of VST" would be a fine description of the alternative package.

Of cause we can do this, but this is not the intention behind the changes. The intention is to have a "platform friendly" variant of CompCert. For me this means:

• not duplicating libraries which are available in the (to come) Coq platform
• putting information other libraries need in a place where they can find it in a consistent way (based on what coqc -where says).

And I fully agree that putting Flocq in the name and the description is misleading - it is the main thing but not the only one. The name is historic - I started with Flocq and later found I need more changes. I will change the name and description.

I have reservations about adding stuff to a .ini file that is not configurable. I mean, the bit width is not a configuration parameter, it's a function of other parameters. Plus, it's already described in the Archi.v file of the target platform.

Archi.v is not installed (at least not in a place I would look for it). I get the following:

~$ cd .opam/coq_opam/lib/coq/user-contrib/compcert/
compcert$ find . -type f -and -not -name "*.vo"
./compcert.ini
./README
./VERSION

VST needs the bitsize during make, not just during coqc runs. VST developments frequently depend on the bitsize but less frequently on other architectural parameters. So while the view of CompCert on what is important and what not is obviously more low level, the abstraction CompCert delivers up to VST is mainly parameterised by the bitsize. Afaik non of the VST developments provided as examples depends on something else then the bitsize - in the sense of .v source code, of course compiled .vo files depend on the detailed architecture. Not putting this parameter in the upwards interface of CompCert destroys this abstraction.

I am completely open to extracting the bitsize in another reliable way. Originally VST was extracting it from CompCert's Makefile.config, but I thought that this is not the best way of doing it, since it requires access to the folder in which CompCert has been compiled.

[jhjourdan]

Of cause we can do this, but this is not the intention behind the changes. The intention is to have a "platform friendly" variant of CompCert. For me this means:

• not duplicating libraries which are available in the (to come) Coq platform

Then you should update the name and use the provided package for MenhirLib, since it is also available in another opam package.

I am completely open to extracting the bitsize in another reliable way. Originally VST was extracting it from CompCert's Makefile.config, but I thought that this is not the best way of doing it, since it requires access to the folder in which CompCert has been compiled.

An obvious solution would be to run a simple .v file which imports Archi.vo, and does a Print ptr64. Sure, this is a bit convoluted, a requires a bit of parsing, but this surely works.

[MSoegtropIMC]

Then you should update the name and use the provided package for MenhirLib, since it is also available in another opam package.

Indeed - I tend to overlook the menhir coq library. I will change this (it might require some additional require statement patching though).

An obvious solution would be to run a simple .v file which imports Archi.vo, and does a Print ptr64. Sure, this is a bit convoluted, a requires a bit of parsing, but this surely works.

I thought about that, but since VST needs other information as well which is available in the compcert.ini file it looked a bit contrived. On the other hand it is for sure the safest and most portable method to extract that information. I will see if I can get all information VST needs that way.

Should I copy the compcert.ini file to the coq library folder anyway (even though VST doesn't need it then). I think it might be good documentation on what compcert has been installed.

[jhjourdan]

Should I copy the compcert.ini file to the coq library folder anyway (even though VST doesn't need it then). I think it might be good documentation on what compcert has been installed.

I don't have a strong opinion. But if VST does not need it, then we should be able to wait for AbsInt/CompCert#348.

[MSoegtropIMC]

Regarding retrieving architecture flags for VST: I need bitsize and arch. I can get this from running:

From compcert Require Import Archi.

Locate Archi.

Print Archi.ptr64.

but neither output is somehow direct. I get Module compcert.x86_32.Archi from which I would have to extract the x86 (without the _32). Not sure how this would look in the Arm case. Converting the bool for ptr64 is less of an issue.

I can do this - no problem - but please let me know if this is really what you want. I would say it doesn't hurt to supply a file which contains the most important architecture information to the user in a way which looks like it is designed to be used like this. I can't say that of this method. In the compcert.ini file it looks like this:

arch=x86
bitsize=32

[jhjourdan]

Given what happened in AbsInt/CompCert#348, could you either use a similar solution by patching CompCert to suit your needs or use Locate/Print in VST as discussed?

[MSoegtropIMC]

Given what happened in AbsInt/CompCert#348, could you either use a similar solution by patching CompCert to suit your needs or use Locate/Print in VST as discussed?

Yes, this is the plan - I am working on it (it is a bit of a chain from compcert over opam to VST).

[MSoegtropIMC]

I did the following updates

• included the latest makefile changes in compcert as patch
• removed the installation of the VERSION file in opam since the makefile does this
• added a variant which only builds the open source part of compcert (this is sufficient for teaching VST, but not for using it for own code).

[jhjourdan]

What about coq-MenrhiLib?

There is now one additional variant (the open source one). Could you clarify its point? This cannot be about the license, since it also install builtins1.vo.

[MSoegtropIMC]

What about coq-MenrhiLib?

The Flocq patch is prepared with comments in the CompCert sources. The Menhir patch not, which might make it less stable. The platform patches might be quite long term (until it is decided to remove the duplications from CompCert). Also for Flocq the duplication leads to massive problems, e.g. one can't use CoqInterval or Gappa to prove C code correct cause of the duplication of definitions. Maybe there are also issues with duplicating Menhirlib, but I am not aware of such issues. The plan is to first prepare the patch in the sources and then do it. So 3.8.

There is now one additional variant (the open source one). Could you clarify its point? This cannot be about the license, since it also install builtins1.vo.

The main point is that VST CI runs into hard time limits when building the complete CompCert. There are also other non urgent reasons, see (AbsInt/CompCert#351) for a discussion. But even if @xavierleroy makes this file dual licensed soon, I can't remove the note in 3.7 because I don't think it is agreeable to patch license files and opam does not support direct cherry picking. So for 3.7 I think this is the best option. I don't want to use a non release commit as source for clarity.

[MSoegtropIMC]

@jhjourdan : are there remaining issues or can we merge this now?

[jhjourdan]

The patch for using an opam supplied coq-menhirlib is rather simple:

diff --git a/Makefile b/Makefile
index df5fb03f..001f147d 100644
--- a/Makefile
+++ b/Makefile
@@ -247,7 +247,7 @@ driver/Version.ml: VERSION
 
 cparser/Parser.v: cparser/Parser.vy
        @rm -f $@
-       $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
+       $(MENHIR) --coq cparser/Parser.vy
        @chmod a-w $@
 
 depend: $(GENERATED) depend1

But I agree that this is probably not essential since it is unlikely that any external developments will refer to Compcert's parser.

[MSoegtropIMC]

@jhjourdan : can you please hold this back for a day? @xavierleroy modified the license to include the one missing file, so I want to clean up the open source package. It might also make sense to split this PR into the two main packages (plain release and coq-platform) and do the open source variant later. Would you prefer this?

[MSoegtropIMC]

-       $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
+       $(MENHIR) --coq cparser/Parser.vy

Ah ok, I didn't see this variant - I thought about patching the sources. Indeed this is a reasonable option. I will implement it since I anyway also have to adjust the open-source package to the license changes.

[jhjourdan]

Another thing which worries me is that we are introducing two new variants of the CompCert package for the sole purpose of one third-party software, VST... This seems overkill.

But all in all, I don't think there is a strong argument against this PR. Hence, I am not opposed to merging this (even without the patch for coq-menhirlib). So, as long as @xavierleroy is not opposed, feel free to merge.

[MSoegtropIMC]

Another thing which worries me is that we are introducing two new variants of the CompCert package for the sole purpose of one third-party software, VST... This seems overkill.

This is not how it is intended. The main goal of this PR is to prepare the Coq platform release for Coq 8.12. I don't know if you are aware of the discussion but the basic idea is to split the Coq releases into 2 phases - a Coq core release and a short while later a Coq platform release which includes an extended set of packages useful for teaching and exploring Coq related technology in an easy to setup way. See (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md). I would say that there is a broad consensus for this among the Coq maintainers.

The main goal of this PR is to provide opam packages for CompCert which play nicely in the context of a Coq platform which means using packages provided by the platform and providing required configuration information for other packages in the platform. Sure, VST is currently the only user of CompCert in the platform, but still this is not done purely for the benefit of VST but for the benefit of the Coq platform in general.

The open source package is also there because there are discussions if the platform should contain non open source software at all. The open source package offers a choice suitable for teaching and exploration in case it is decided that full compcert is not included.

[MSoegtropIMC]

@jhjourdan : I changed it to use the opam version of menhirlib and also added the license changes as patches from (AbsInt/CompCert#351). @xavierleroy agreed to include the license file changes as patches (which I wouldn't do otherwise).

I locally tested VST with both coq-platform variants and it works fine.

So from my point of view, this is good to go.

[Aurel300]

Just stumbling upon this from #940. With this merged, it will be possible to opam install coq-compcert and opam install coq-vst from the extra-dev archive? Or does there need to be another patch applied for VST specifically?

[MSoegtropIMC]

Just stumbling upon this from #940. With this merged, it will be possible to opam install coq-compcert and opam install coq-vst from the extra-dev archive? Or does there need to be another patch applied for VST specifically?

The VST opam file PR as such is not there yet and this depends on some changes in VST, which in turn depend on this PR (I am currently working with a local patch opam repo in the VST source tree to parallelise things a bit). The VST PR is hanging on issues with CI (timeouts, strange effects with the local opam patch repo, ...). See (PrincetonUniversity/VST#406).

So the chain of events is:

• merge this PR
• merge the VST PR (Adjust makefile and build instructions to platform supplied compcert, flocq, ... PrincetonUniversity/VST#406)
• create a VST opam PR (I have the file locally tested with all the above locally patched but it doesn't make sense without the two above merged)

[jhjourdan]

From my side, this is ready to merge. I would still prefer to have @xavierleroy's approval for this specific PR, though, since there are license changes.

[MSoegtropIMC]

@jhjourdan : FYI: @xavierleroy explicitly answered in (AbsInt/CompCert#351 (comment)) that it is ok to take his latest commits changing the license file as patch in opam. But if you prefer, I can wait.

[jhjourdan]

Alright, then let's merge!

[jhjourdan]

@silene? @clarus?

[clarus]

Done!

[xavierleroy]

Apologies for leaving you hanging. I confirm that everything is fine license-wise.

[MSoegtropIMC]

@jhjourdan, @xavierleroy : do you have objections against adding the same three opam package for 64 bit compcert? I would name it coq-compcert-64 and install it to user-contrib/compcert64. This way both variants can coexist. I am just adding support for this in VST. Another option would be to have coq-compcert use the system bit size (64 bit usually these days) and have coq-compcert-32 and coq-compcert-64 which set the bitsize explicitly. It might also make sense to add packages for the most common cross variants, say a common 32 bit and 64 bit ARM variant.

[jhjourdan]

Indeed, we could have a variety of packages for various architectures. If you are willing to do the work, this should be merged. Not sure there would be many users (aka. testers for the packages), though.

If we do that, we should consider making coq-compcert a pseudo-package which depends on the package corresponding to the current architecture. But I do not know whether opam supports conditional dependencies depending on the architecture.

[Zimmi48]

It supports conditional stuff in the build process at least. It might also work in the dependencies. Cf. https://github.com/ocaml/opam-repository/blob/acbec000d209ea977d778e9b014297c7ebef5eb7/packages/coqide/coqide.8.11.1/opam#L30 and https://opam.ocaml.org/doc/Manual.html#Global-variables.

[MSoegtropIMC]

If we do that, we should consider making coq-compcert a pseudo-package which depends on the package corresponding to the current architecture. But I do not know whether opam supports conditional dependencies depending on the architecture.

My suggestion was to keep the OS resolution in the package (that is the coq-compcert-64 package would build linux on linux, windows on windows and OSX on OSX), but I can also create separate packages for each major platform variant (I guess this would be 8, 32 and 64 bit x86 on Linux, Windows and OSX + arm 32 and 64 on Linux) and make coq-compcert a virtual package choosing the most sensible of these. Both variants would be easy to do. I guess in the end your suggestion is better since people might want to verify Linux code on non Linux OS.

So if this is agreed, I will prepare a PR.

[jhjourdan]

If conditional dependencies are possible, then I would indeed prefer my solution (not only for the hardware architecture, but also for the OS). In the end, the user will see the same result as far as the coq-compcert package is concerned. But then, when the coq-compcert package is installed another coq-compcert-xxx package is installed, and some other package may depend on one of the two indifferently.

BTW, you should not forget to add conflicts between these pacakges.

[MSoegtropIMC]

BTW, you should not forget to add conflicts between these pacakges.

The plan is to install each variant in a different folder under user-contrib, say compcert_ia32_win, so that there wouldn't be a conflict. One could install all of them in parallel. At least for 32 and 64 bit, I think quite a few users would use this. The virtual package should just create a symlink under user-contrib for the choice it made, possibly via a compcert32 and compcert64 symlink which link to the final variant. For the executables I would do the same as well as for the libraries and headers.

[jhjourdan]

This looks like a plan, indeed.