opam package for VST 2.4

[clarus]

Hi,

I report here an issue submitted on the Coq opam repository:
"Please update vst to 2.4 version" coq/opam#940

[MSoegtropIMC]

Dear VST Team,

I would indeed appreciate if the coq opam archive at

https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-vst

would contain package descriptions for VST 2.3, VST 2.4 and VST 2.5. I plan to switch the build process for the Coq Windows installer to opam for Coq 8.12 and VST is one of the few packages I include in the Windows installer which doesn't have a recent opam package file.

You might also want to put opam files for upcomming VST releases into

https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-vst

This makes it easier to build master versions of VST (or of complex tool chains including VST).

If you tell me the additional authors for each version and the Coq and CompCert dependencies, I can also do a PR for the opam files for you. The dependencies I could also try with scripts.

Best regards,

Michael

[MSoegtropIMC]

I just wanted to let you know that I started to work on opam files for VST 2.3 ... 2.5 which should be technically OK. I will create a PR for the coq-released opam archive but will ask for review here, so that you can adjust e.g. the author list.

[MSoegtropIMC]

@andrew-appel : I have one question regarding the opam files: I think it would make sense to have separate packages for "VST using the VST supplied compcert front end" and for "VST using a separate compcert". The first one obviously doesn't depend on compcert, so it is more flexible - compcert is fairly picky regarding coq and OCaml versions. I would patch this version the same way I patch the version in the Windows installer (change Require compcert to Require VST.compcert) so that it can coexist with compcert in case there is one (e.g. for clightgen).

The version with external compcert would work only for a few very specific combinations of Coq and OCaml (which Opam can figure out).

Having this as top level package rather than an option makes the options clearer to the user. I would call the packages coq-vst-ci (for compcert integrated) and coq-vst (for external compcert). Or would you prefer if I switch the names and make the "internal compcert" variant the default named coq-vst and name the external version coq-vst-ce?

[lennartberinger]

@MSoegtropIMC : I suggest you include Karl Palmskog (https://setoid.com ) in the
discussion on VST in opam. Karl is an opam maintainer and has
participated in several Coq verification projects, incl Verdi/Disel.

[MSoegtropIMC]

@lennartberinger : Thanks, I will discuss the opam technicalities with Karl then (I know him from coq gitter). Regarding the author list in the opam file: can I reuse the one from VST 2.2. for VST 2.3 .. 2.5 or are there additional authors (which want to be named)?

[palmskog]

@MSoegtropIMC There are indeed some tricky design decisions in OPAM packages concerning optional dependencies and compilation, but I think a package for 2.5 based on the 2.2 one (unconditionally using an external CompCert) should be a good starting point. Note that VST seems to be subject to the "flaky parallel build bug" on OCaml < 4.06 as described in AbsInt/CompCert#327 so one needs to have make "-j%{jobs}%" {ocaml:version >= "4.06"}. We can discuss more details on Gitter.

[lennartberinger]

@MSoegtropIMC It seems the file was not updated since VST2.0. At least William Mansky should be added.

[MSoegtropIMC]

Fine, I will add William.

[andrew-appel]

This issue should be resolved by pull request #406.

[MSoegtropIMC]

This issue should be resolved by pull request #406.

Not quite. There is still a PR for the VST opam packages missing, which I will do as soon as #406 is finished and merged.

[liyishuai]

The latest OPAM release is still 2.2. Is there a plan to resolve coq/opam#940?

[MSoegtropIMC]

Yes, it should come soon.

[MSoegtropIMC]

opam files for VST 2.6 have just been merged:

(coq/opam#1359 (comment))

These files should be compatible with Coq 8.11.X and Coq 8.12.0 (currently only the latter is really tested).