Create new opam packages for VST

[MSoegtropIMC]

This issue is intended as a discussion platform for the desired structure of opam packages for VST (and also CompCert).

What I am currently thinking about is how to handle different platforms (say 32 and 64 bit or x86 and ARM). Obviously only one of them can be available as VST at a time. There are essentially four options:

1. Make compcert / VST for different architectures mutually exclusive in opam

2. Have different root names for different platforms, say VST_X86_32, VST_X84_64, VST_ARM_32, VST_ARM_64 - the same for CompCert

3. Use the same root name for different platforms (VST) and do some -Q / symlink tricks to link "the" VST to the desired folders

4. Have one variant readily accessible as VST and require -Q options for all others.

Since one might want to verify the same code for different platforms, I would think that option 1 and 2 are not very practical. 1.) would require to constantly reinstall VST and CompCert - something opam is not very efficient in - and 2.) would require to adjust the package names in the Coq sources.

4.) is the status quo for CompCert and the opam packages I suggested to @andrew-appel (attached as zip to this issues) and agreeable but raises the question which one should be "the" VST - Xavier recently said that if there is the "CompCert" in opam, it should be x86 64, not 32 as is.

If we agree on option 3.), I would propose the following mechanism(s):

• have specific opam packages, say VST_X86_32, VST_X86_64, VST_ARM_64 and put these into special locations (as is done already for coq-vst-64) where Coq usually does not find them. All of these packages can be installed in parallel. The folder structure is <special_package_root>/VST_/VST so that when <special_package_root>/VST_ is linked in with (just one) -Q option, VST is still known as VST. Which VST it is, depends on the -Q option.

• have selection opam packages, which depend on the specific packages and symlink one of them to the default location and root path VST. The selection packages are mutually exclusive, but can be uninstalled / installed very fast since they just create a folder symlink (a few more for CompCert). This should hardly take a second.

This gives the VST user the following choices:

• install just one selection package (which automatically installs the specific package) and use VST without -Q. Possibly switch between selection packages when switching between platforms.

• Install several specific packages and use VST with -Q options to point to the specific packages.

• point with -Q options to the root of the special package folder and use long qualified names (something like Require Import VST_X86_64.VST.xyz). This would allow to create single proofs which involve several platforms, but it would take some thinking to make sure the respective VSTs find the respective CompCerts.

The current status of CompCert and the currently proposed VST opam packages is that VST X86 32 installs as "VST" in the default location and everything else installs in special locations. So one can use VST X86 32 without -Q but needs -Q for all other platforms.

[MSoegtropIMC]

Suggested opam files (method 4. above)
devrepo_share.zip

[MSoegtropIMC]

P.S.: since VST and CompCert are closely tied, such changes obviously need to be done together for CompCert and VST - CompCert first. So my suggestion is to first go for VST with method 4 - which matches the current approach of CompCert - then move CompCert to method 3 and then move VST to method 3. A Method 4 VST should be able to work with a method 3 CompCert as long as CompCert X86 32 is installed as select package.

I already discussed this with the CompCert opam maintainer and I would summarize this such that they agree with 3.). See

coq/opam#1246 (comment)

[andrew-appel]

What about the fact that symlinks don't always work in cygwin? Will this be an issue for Coq following -Q options via symlink, in the Windows build?

[andrew-appel]

Regarding what is the "default": Although the "default" VST has been 32-bit in the past, I think it would be fine if the "default" VST installation were 64-bit.

I regularly need to have two or three different VST builds installed and working on the same machine, for use in different applications. Option 1 seems unacceptable.

If we are to have -Q options, is there a portable way to do it, so that the pathnames look the same on each different machine's opam installation? That is, to get 64-bit-ARM VST, one does -Q VST_ARM_64 VST or something?

[MSoegtropIMC]

What about the fact that symlinks don't always work in cygwin? Will this be an issue for Coq following -Q options via symlink, in the Windows build?

Yes, this will take some experiments. The options I am aware of are:

• Windows (NTFS) native symlinks (MKLINK) - afaik these require a special policy setting people usually don't have.
• Windows (NTFS) directory junction points (MKLINK /J) - not sure what rights this requires
• Copy the directory structure and hard link the files (should work for any user on NTFS)
• Copy the directory structure including the files (the only option for FAT file systems)

Cygwin symlinks don't work for MinGW apps, since they are implemented in the cygwin DLL. So this is not an option.

I will probably supply a command which just does whatever is appropriate on the respective OS and use this.

If we are to have -Q options, is there a portable way to do it, so that the pathnames look the same on each different machine's opam installation? That is, to get 64-bit-ARM VST, one does -Q VST_ARM_64 VST or something?

Currently the portable way is $(coqc -where)/../coq-variant/VST64. I would simply store $(coqc -where)/../coq-variant - possibly with normalization to remove the /../ - as COQ_VARIANT in the makefile.

As far as I can tell one needs only one -Q option for CompCert and one for VST - in this respect the new setup should be simpler than the previous method.

[MSoegtropIMC]

P.S.: the main downside of variant 3) is that we are talking about a lot of opam packages - maybe more than 12 for each release of VST since per platform one needs the real package and the switch package. For CompCert it would be 3 times that since one also has the coq-platform and open source variants, so 36 opam packages per release. I think the platforms people use frequently are:

• x86 32+64
• ARM 32+64, possibly a few variants
• RiscV 32+64

So I think option 4 is not that bad either. Besides requiring only half the number of packages (still a lot) it also avoids the messy symlink on Windows issue. The main downside of 4 is that only one platform can be used easily without -Q options. But I would think for the majority - especially courses and homework - this is sufficient. One can just open a .v file in CoqIDE and things should work. The advanced users should be able to handle the -Q options.

I am open to implement either variant. I think which one is chosen mostly depends on the requirements of teachers. Industry people likely anyway use only one platform and/or can handle the -Q issue.

[MSoegtropIMC]

P.P.S.: one more question to decide: if VST x86 64 becomes the default, how do we name VST x83 32? Should it be

• VST32 (Coq path) / coq-vst-32 (opam name)
• VST_X86_32 (Coq path) / coq-vst-x86-32 (opam name)

One could have packages coq-vst-x86-64 and coq-vst which are identical except that they install into different folders. People using multiple platforms might prefer to always give the -Q option for symmetry reasons.

[andrew-appel]

P.S.: the main downside of variant 3) is that we are talking about a lot of opam packages
Isn't that also true for variant 4) ?

And a separate question: Can we make the "platform-independent -Q option" work smoothly with coq_makefile etc?

[MSoegtropIMC]

And a separate question: Can we make the "platform-independent -Q option" work smoothly with coq_makefile etc?

I think this should be doable with a few lines in the Makefilie.coq.local file. What is more tricky is to make CoqIDE happy since it just reads the _CoqProject file and afaik this doesn't allow any tricks.

With the tools as they are I think one should use a small outer driver make file which creates _CoqProject. At one point in time one has to talk to the Coq team how such uses cases could be better supported, say by having a -V option which works a bit like -Q but uses folders from a pre-defined variant root folder, so that one just would have to give -V VST_X86_64 to state that the folder /VST_X86_64 should be treated in the same way as user-contrib.

Do you have an example project I could look at?

Btw.: the VST makefile handles this for CompCert already - the logic is in lines 80..90 and 234..240. The logic for a a VST application would be quite a bit simpler - the majority of the logic in VST makefile is there to handle the bundled CompCert builds and being able to build parts of CompCert.

[MSoegtropIMC]

I just added (coq/coq#12686) to propose a -V option.

[intoverflow]

@MSoegtropIMC I noticed that coq-vst.opam and coq-vst-32.opam both seem to work. Does that mean this issue can be closed?

[MSoegtropIMC]

I think we left it open as a sort of reminder that the way we choose between the 32 and 64 bit version needs to be improved in one way or another. What I proposed to the Coq team - but wasn't liked a lot - is to have an option -V which is similar to -Q or -R but maps package variants from a pre defined variants folder, so that -V options wouldn't have to deal with installation dependent paths. But then I think using -Q or -R with $(coqc -where) is not that unreasonable an approach. I am not sure what other VST users think about this.

One problem is that afaik there is no way to include the 32 bit version with a system independent _CoqProject file, which is not so nice e.g. for teaching.

What is your opinion on this?

[intoverflow]

I saw the discussion around coq/coq#12686. I agree with your assessment: the current approach to variants is not ideal, and if Coq is going to support _CoqProject, then Coq also needs to support variants.

I have been experimenting with using make, echo, and find to generate _CoqProject files for CertiGraph and uvrooster. Indeed, typically I generate two separate files: _CoqProject.lib and _CoqProject. The idea is that _CoqProject.lib contains only the stuff you'd want to actually install, while _CoqProject includes all of _CoqProject.lib together with any in-repo examples. This setup makes vscode and opam happy.

My approach uses logic similar to VST's to calculate the right path for compcert and vst based on BITSIZE. This works well with opam. It also works fairly well for vscode, though obviously it means _CoqProject depends on BITSIZE (a minor inconvenience, though I'd still prefer a first-class variant solution).

Edit Here's an example: https://gist.github.com/intoverflow/6896430492576d4087cf2709057f67a5

[MSoegtropIMC]

Yes, it is possible to generate _CoqProject files this way. But what I would prefer is if one could create a downloadable example including a CoqProject file and it would just work in CoqIDE and VSCoq. Afaik this is currently not possible. I guess the right approach is to go ahead and write a CEP. I was just too busy to do so. Maybe we can do this together?

[intoverflow]

I think I can offer you some relief re: including _CoqProject file in a downloadable example.

I've updated my example to support BITSIZE=opam (and to use this value by default). With this setting, the generated _CoqProject* files will not include -Q directives for compcert or VST.

In particular, the generated _CoqProject* files will not contain any system-specific paths, rendering them safe for inclusion in the repo/downloadable example.

Since these files do not provide -Q directives for compcert or VST, CoqIDE and VSCoq will search coqc -where for these packages. If coq-compcert and coq-vst are installed, this search will succeed (at time of writing, these packages are bound to CompCert's x86_64-linux target, aka BITSIZE=64).

Users who would prefer to work with a different target architecture can re-generate _CoqProject* with a single command. I know 1 command is more than 0, but this procedure probably won't be useful to all users, so on average let's say it's 0.5 commands :)

Happy to collaborate on a CEP. I'll first need to catch myself up on some of the details about opam's handling of variants, though.

[andrew-appel]

Does P.R. #644 address any of these issues? That P.R. is to help insure that on ARM-architecture Macs, the default VST configuration is for the ARM-64 architecture; before that, the default was x86-64 even on ARM-native machines, which was inconvenient.

[MSoegtropIMC]

PR #644 is about configuring VST. What is discussed here is using several already configured (by opam) VST installations in an effective way, so I would say this are independent issues.