Changed installation target folders for 64 bit CompCert

[MSoegtropIMC]

This is a modification of my PR #1318. The main change is that 64 bit compcert coq library is installed outside of the usual Coq search path, so that -Q / -R options must be used to link it to compcert.

Working with the previous setup proved not to be very practical. In the end naming the module compcert64 means that all files supporting both 32 and 64 bit need to be duplicated or patched. Putting it in Coq's default load path also has bad side effects, it leads to a lot of warnings when the package is renamed with -Q or -R.

The solution proposed here is more practical.

The 64 bit binaries and C library are installed in a folder /variants/compcert64.

FYI: @xavierleroy @jhjourdan @palmskog

[MSoegtropIMC]

@palmskog : thanks for merging!

Is there somewhere a discussion on how opam should handle variants? Some people might want to install CompCert and VST for various platforms and bitsizes. The method I chose here works, but I wonder if others have similar problems and how these are handled. I guess it would be most convenient to install all variants in a non standard location (as I did here under opam-root/variants) and have a way to set symlinks to one of these variants quickly.

As I did it know the link between VST and CompCert is essentially a hack - the VST makefile knows where the non standard compcerts are installed.

[MSoegtropIMC]

P.S.: here is the corresponding VST makefile PR: (PrincetonUniversity/VST#406). I will do a VST opam PR as soon as this is merged.

[xavierleroy]

I don't know what possibilities are supported by OPAM to handle multiple configurations of a package. What I would like to say is that if one configuration of CompCert is to be selected as the default CompCert package, it should be x86-64. x86-32 is no longer supported by macOS, and Linux support is getting spotty. On the contrary, ARM64 is on the rise (cf. recent Apple announcements).

[MSoegtropIMC]

I don't know what possibilities are supported by OPAM to handle multiple configurations of a package.

The only reasonable idea I came up with so far is to have packages which install everything to non default locations, then have mutual exclusive packages which just reference these packages and symlinks one of these packages to the default location and a default package which references one of these symlink packages. Users can then choose if they refer to the architecture specific non default location or to the default location. The advantage of having symlink packages is that these would be very quick to install and change.

The downside of this is that we are talking about quite a few packages:

• plain CompCert
• platform friendly CompCert (using platform Flocq and Menhirlib)
• open source only package

times

• x86 32
• x86 64
• arm 64
• maybe RiscV

times

• real package
• symlink package

would be at least 18 + 1 default package. If this agreeable, I can do this - I have meanwhile a fairly clear picture about how I would do this.

What I would like to say is that if one configuration of CompCert is to be selected as the default CompCert package, it should be x86-64

Would you make this change already for 3.7 or would you wait for 3.8?