Fixes #437 - Removed files from local opam patch repo already merged upstream

[MSoegtropIMC]

No description provided.

[liyishuai]

Should the repo and version files under opam-release folder be removed as well?

Also, is some coq-vst.opam file available somewhere? (depends on #436)

[MSoegtropIMC]

Should the repo and version files under opam-release folder be removed as well?

If you remove this, you have to remove the repo add in Travis as well. I would keep this since it gives you the flexibility to work with patched opam packages any time you need to - say during the release process of a new CompCert or for experimentation. You can just drop some opam files into the packages folder and they will take precedence in Travis. If the folder is empty, it simply has no effect.

Also, is some coq-vst.opam file available somewhere? (depends on #436)

it does no really depend on #436 - the opam files also work without this.

There is one quite old opam file for VST:

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

I have opam files for the intermediate versions, but they are all patched to solve the Flocq issue. We might want to publish them anyway.

[liyishuai]

coq-vst.dev seems broken. Is a fix pending?

#=== ERROR while compiling coq-vst.dev ========================================#
# context     2.0.7 | macos/x86_64 | ocaml-system.4.09.0 | https://coq.inria.fr/opam/extra-dev#2020-07-03 12:00
# path        ~/.opam/8.11/.opam-switch/build/coq-vst.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build make IGNORECOQVERSION=true -j7 COMPCERT=/Users/yishuai/.opam/8.11/lib/coq/user-contrib/compcert floyd progs
# exit-code   2
# env-file    ~/.opam/log/coq-vst-69841-e3ca28.env
# output-file ~/.opam/log/coq-vst-69841-e3ca28.out
### output ###
# cat: /VERSION: No such file or directory
# cat: /VERSION: No such file or directory
# Makefile:125: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.7 buildnr= tag= but /VERSION=.  Stop.

[MSoegtropIMC]

@liyishuai : this is quite old for CompCert 3.3. I would just remove it. A dev build should be newer than the latest release and should be removed when the release is out. But I think usually people don't expect that year old stuff in the beta repos still works.

Actually I would prefer if dev would just build current master. If you want, I can update it in this way.

I think it would make more sense to provide opam files for the 2.3, 2.4 and 2.5. As I said, I have such files but they don't correspond to your tags because I had to use the system supplied Flocq (otherwise one can't use any tools to prove numeric code correct, and that's it what I do since ever with VST). But it wouldn't be difficult to supply opam files which correspond to what you have in your tags. They wouldn't be usable for my work but it hardly would take me an hour to do so. If you are willing to test these opam files, I can send them to you, you can test them locally (I can tell you how to set up a local opam repo for testing) and then we can push them. I could only do very basic tests - say a few examples - because non of my developments works without the Flocq patch.

[liyishuai]

I'd recommend maintaining a coq-vst.opam in this repository, which always works with the master branch (tested by CI), and is synchronized with coq-vst.dev on extra-dev, so that users can access the bleeding version via OPAM.

Always having a dev version is helpful when a critical fix (e.g. #428) is merged, I can tell my colleagues to "upgrade your coq-vst.dev", rather than "recompile VST on commit 96c92ea".

Moreover, maintaining an OPAM file within this repo allows users to fork, modify, and install with simply opam install ..

[MSoegtropIMC]

There is one difficulty with this - the opam files require a cryptographic hash checksum of the files. I am not sure one can get around this. I will ask. I agree that in general this is what one wants for a "dev" build, but package system maintainers tend to have a different opinion on that.

In case one can't get around this, I think it wouldn't be difficult to write a short shell script which sets up and registers a local opam patch repo, which has a VST opam file for an arbitrary tag, commit hash or branch.

[liyishuai]

There is one difficulty with this - the opam files require a cryptographic hash checksum of the files.

Not required for extra-dev where the source is Git. I can help with the extra-dev releasing process.

---

For now my problem is compiling with COMPCERT=platform failed with:

Makefile:125: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.7 buildnr= tag= but /Users/yishuai/.opam/8.11/lib/coq/user-contrib/compcert/VERSION=version=3.7 buildnr= tag= branch=. Stop.

[MSoegtropIMC]

Not required for extra-dev where the source is Git. I can help with the extra-dev releasing process.

I see - thanks! Good to know.

Makefile:125: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.7 buildnr= tag= but
/Users/yishuai/.opam/8.11/lib/coq/user-contrib/compcert/VERSION=version=3.7 buildnr= tag= branch=. Stop.

The Makefile compares the literal content of the VERSION file between the bundled CompCert, that is file (in the VST repo):

compcert/VERSION

and the VERSION file in the user-contrib/compcert. The latter seems to have the additional field "branch=". To get further, you can simply edit the VERSION file in user-contrib/compcert or in your local compcert folder, but we need to find out where this branch= field comes from. I have never seen this.

To summarize: the Makefile expects that the local VERSION file and the VERSION file of the installed CompCert are identical except for newlines.

[MSoegtropIMC]

P.S.: will you create a coq-vst-dev file based on git master or shall I do it?

[liyishuai]

I've created the OPAM files on my side, now testing.

[MSoegtropIMC]

I've created the OPAM files on my side, now testing.

OK. good. How about the issue with the CompCert version comparison. Shall I make a PR to extract just the version number from the file? I thought it was safer to compare the complete contents and this did work for me so far, but there seem to be variations in this file which have nothing to do with the version.

[liyishuai]

I have it in https://github.com/liyishuai/VST/commit/12e751ffa29457cda72b7304bea73a6eac90e4ed which will be included in my PR.

[MSoegtropIMC]

I have it in liyishuai@12e751f which will be included in my PR.

Looks good to me.

I wonder if one could have a significantly different CompCert with the same version number if tag or branch is not empty, but I guess this would happen only to experts which should be able to handle the resulting error messages. I also expect that such experts would work with the bundled CompCert.

[MSoegtropIMC]

Btw.: I yesterday sent Andrew opam files for VST 2.6-beta for testing. Did he forward these files to you?

[liyishuai]

No I haven't seen those files. My files in #440 are adapted from extra-dev.

[liyishuai]

Back to the opam-release folder: Travis CI is failing on my fork: https://travis-ci.com/github/liyishuai/VST/jobs/360279714#L800-L803
Does the build depend on some existing cache of .opam?

[MSoegtropIMC]

No I haven't seen those files. My files in #440 are adapted from extra-dev.

Ah ok - so it was just a coincidence that you started to work on opam files for VST - I have been discussing this with @andrew-appel for a while and recently also changed the structure of the CompCert opam files quite a bit.

I opened a new issue #441 to discuss the structure of the opam files.

https://travis-ci.com/github/liyishuai/VST/jobs/360279714#L800-L803

Hmm - it looks like the now empty packages folder has been removed (sometimes). Either we need to take care that the folder is there are add a --yes to the opam repo add command.

[MSoegtropIMC]

https://travis-ci.com/github/liyishuai/VST/jobs/360279714#L800-L803

I created PR #443 which hopefully fixes this.

[MSoegtropIMC]

@liyishuai : I just wanted to ask if #443 fixes your CI issues.

[liyishuai]

Yes seems fixed in https://travis-ci.com/github/liyishuai/VST/builds/175569831