Adjust makefile and build instructions to platform supplied compcert, flocq, ...

[MSoegtropIMC]

This PR does the following changes:

• change makefile and build instructions to support platform supplied compcert and flocq
• do not use any -R or -Q flags for platform supplied libraries
• restructure makefile for better maintainability

Note: the changes to the makefile look massive, but I mostly restructured it into sections for configuration, flags, file lists, rules and targets. It mostly was already like this but I moved things like configuration variables, notes, checks, ... all into the configuration section at the beginning.

The only real changes are:

COMPCERT ?= 
:
:
COQLIB=$(shell $(COQC) -where)
:
:
ifeq ($(COMPCERT),)
  COMPCERT=$(COQLIB)/user-contrib/compcert
  PLATFORM_COMPCERT=yes
else
  PLATFORM_COMPCERT=no
endif
:
:
ifeq ($(PLATFORM_COMPCERT),yes)
  COMPCERT_R_FLAGS=
  EXTFLAGS=
else
  COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
  EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
endif

[andrew-appel]

There's a problem: our travis-ci continuous integration fails
https://travis-ci.org/github/PrincetonUniversity/VST/jobs/677608668

The error message is,

cat: /home/travis/.opam/4.07.1/lib/coq/user-contrib/compcert/VERSION: No such file or directory
Makefile:77: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.7 buildnr= tag= but /home/travis/.opam/4.07.1/lib/coq/user-contrib/compcert/VERSION=.  Stop.

It seems like the opam installation of CompCert does not have a VERSION file.

[MSoegtropIMC]

Sorry, yes - you don't have the patched CompCert as yet. There are a few ways to fix this:

1.) Wait until PR (coq/opam#1246) is merged and then use the platform-flocq variant of CompCert
2.) Work with a local addon opam repo to get this beforehand (quite easy)
2.a.) Put this repo as opam folder under VST (requires that the VST repo is cloned in travis before compcert is installed via opam, which I think is the case)
2.b.) Have this patch opam repo as separate git repo somewhere.
3.) For the time being work with internal CompCert (which is done by writing a CONFIGURE file with COMPCERT=compcert).

I can do any of these. Which one would you prefer? I would think 2.) is most flexible long term. I would prefer 2.a) in case it works (I think it should).

But I must admit I don't fully understand what is going on. CompCert 3.7. does install a VERSION file, but since there is no opam file for CompCert 3.7, I guess you are using CompCert 3.6 - I am not sure what this does.

One more note: I replaced the use of CompCert Makefile.config with compcert.ini, which 3.7 writes to <root>/share/. I did a change that it also writes it to `/lib/coq/user-contrib/compcert/, where VST can easily find it.

[MSoegtropIMC]

I implemented method 2a, that is provide a folder with patched opam files within the VST git tree. I think you will need this from time to time when by default using libraries from opam, so I think it makes sense to keep this as general mechanism. In case no patches are required, the folder can just be empty.

I think this would work now (VST starts to build and gets pretty far) but travis times out because a full CompCert build is done now which takes about 13 minutes. Can you extend the travis time (it is 50 min) or is this a hard limit?

[Zimmi48]

Can you extend the travis time (it is 50 min) or is this a hard limit?

That's a hard limit.

What could be done OTOH would be a setup to cache the build output of CompCert (especially if it's a fixed released version rather than a moving target). There are several ways this can be achieved. One way is through Nix + Cachix and another is through opam + Docker (cc @erikmd). Let us know if you are interested in hearing more.

Another (less optimized) solution is simply to move to another CI provider that allows longer build times. For instance, we now have good support for GitHub Actions (thanks to @erikmd) and it allows 6-hour-long builds.

[andrew-appel]

I am in the process of switching from travis-ci.org to travis-ci.com where Princeton University has a paid account. Therefore it might be possible to relax the 30-minute restriction. However, I have some concerns about this: I really would like to avoid building all of CompCert in the VST CI, when only a few files (leading up to the specification of the Clight semantics) are really needed.

It might also be possible/advisable to switch from travis-ci to GitHub Actions, where Princeton University also has a commercial account.

[MSoegtropIMC]

However, I have some concerns about this: I really would like to avoid building all of CompCert in the VST CI, when only a few files (leading up to the specification of the Clight semantics) are really needed.

Mid term (within < 6 months) the goal is to have a platform installer which automatically looks for precompiled binary packages at least for common platforms. This would solve this on average, but the CI system should still be able to build from sources, in case a binary package is not yet available.

One can of cause also think about having a strip down compcert package in opam and stating that VST can live with either the full package or the strip down package. Let me see if I can prototype this here.

Btw.: I also plan to do a 64 bit compcert package. The current opam package always installs the 32 bit version for the host OS/platform.

[andrew-appel]

There's another advantage to a stripped-down CompCert package in opam: That stripped-down package is fully open-source, whereas full CompCert is not open-source.

[MSoegtropIMC]

There's another advantage to a stripped-down CompCert package in opam: That stripped-down package is fully open-source, whereas full CompCert is not open-source.

That is an option indeed, although most people would need clightgen. One could create separate packages for the compcert frontend and for the clightgen binary. I have to see what changes in the CompCert makefiles this would require.

Btw.: the 64 bit part shouldn't be an issue - I will create CompCert-64 opam packages.

Regarding the compcert.ini file (which is currently blocking the CompCert opam PR): it seems to go into the direction of creating a separate file with configuration information for Coq-end users of CompCert. So I guess I can update this PR soon.

[andrew-appel]

I believe the clightgen binary is now covered by the open-source license. (Look at CompCert/LICENSE -- everything in the exportclight directory is dual-licensed.) This was not previously the case, but it has been true for at least a year now.

[Zimmi48]

That's good to hear. @MSoegtropIMC In this case, does it make sense to continue distributing the full CompCert as part of the Coq platform (as opposed to distributing a fully open source platform that would only contain the open source core of CompCert, since this is what VST needs anyway)?

[MSoegtropIMC]

I believe the clightgen binary is now covered by the open-source license. (Look at CompCert/LICENSE -- everything in the exportclight directory is dual-licensed.) This was not previously the case, but it has been true for at least a year now.

That would definitely require confirmation - I will review and discuss this. I won't comment about the implications before I confirmed this.

[MSoegtropIMC]

I believe the clightgen binary is now covered by the open-source license. (Look at CompCert/LICENSE -- everything in the exportclight directory is dual-licensed.) This was not previously the case, but it has been true for at least a year now.

I don't think this is the case - at least not when I look at what is used when I build just clightgen. The dependency resolution in the compcert makefile is automated, so this seems to be what is technically actually used. You can build (after configure) just clightgen with

make depend
make -j 16 clightgen

This includes many files which are not open source. Of course it might be that there are not necessary dependencies, but this would need a deeper analysis. Anyway, I think we should ask what the intention is.

I will create one more opam package:

coq-compcert.3.7~opensource

which just contains the open source part as per LICENSE file. Let's see if this is sufficient for VST. I make this a coq-compcert "version" so in case VST can live with it, VST can take either variant.

[andrew-appel]

I suspect that the clightgen depends on a certain "extraction" file that is common to both clightgen and ccomp; and that it might be possible to reconfigure the extraction process so that clightgen depends on only the open-source files. But this would take some investigation.

[andrew-appel]

Correction: clightgen is not open-source, because it relies on the SimplExpr and SimplLocals passes of CompCert, which are not open-source.

[MSoegtropIMC]

@palmskog : can you please have a look at the opam installation in the travis log - I don't understand this. I have:

opam show coq-compcert

<><> coq-compcert: information on all versions ><><><><><><><><><><><><><><><><>
name         coq-compcert
all-versions 2.0.0  2.3.2  2.4.0  2.5.0  2.6.0  2.7.1  3.0.0  3.0.1  3.1.0
             3.2.0  3.3.0  3.4  3.5  3.5+8.10  3.6  3.6+8.11  3.7~coq-platform
             3.7~coq-platform~open-source  3.7

but I get

[ERROR] Package coq-compcert has no version coq-compcert.3.7~coq-platform~open-source.

Search and replace tells me that the version listed by opam show and the version it says it doesn't have in the error message are identical. What concerns me a bit is that opam-show lists 3.7~coq-platform~open-source after 3.7~coq-platform. Shouldn't it be before? Did I misunderstand opam's version comparison rules or is this a bug in opam? Can this be the reason that it doesn't find it?

I also thought about making separate packages coq-compcert and coq-compcert-open-source and have mutex rules for them and or dependencies in VST. Do you think that would be preferable?

[MSoegtropIMC]

P.S.: locally this works fine - maybe I should check the opam version on travis.

Btw.: the local opam repo in VST CI is intended to be just temporary. I did this to give @andrew-appel the flexibility he might need when working with a platform approach for testing changes to e.g. compcert opam packages in VST CI while they are published (as in this case). The repo and repo registration in CI is intended to stay, but usually it should be empty.

[MSoegtropIMC]

@andrew-appel : since I can't reproduce this issue locally, I would need a bit of random testing on your Travis CI. Would this be a problem, e.g. do you have project limitations?

We can also wait until the opam compcert PR is merged which might resolve this issue.

[andrew-appel]

Go ahead and test in travis-ci, there are no global limitations, only the per-job limitation of 50 minutes.

[MSoegtropIMC]

@andrew-appel : Two notes on CI reliability:

• the opam packages build during CI seem to be cached. This means that if an opam package is ever changed without changing the version number, one has to explicitly uninstall it - otherwise one gets the old one. Since the caching is likely per runner and since there might be many runners with non reproducible allocation, I guess you have to keep such an explicit uninstall until the version changes. Maybe for CompCert it is better to always build it. I prefer a CI setup using prebuilt but not cached environments since this can lead to all sorts of CI reliability issues.

• the VST make can fail with success without producing a result. This happens e.g. when the compcert.config file is not found. The awk using this is in a variable assignment and I guess make treats this as "don't care fail" - it was like this before - but I don't understand why it doesn't give an error later. I guess the issues is that make fails while building the dependencies and then has nothing to build or so. You can reproduce this by deleting the compcert.config file in the install phase of travis.

[MSoegtropIMC]

@andrew-appel : can you please help me with the failure of the 64bit progs check? Otherwise CI seems to be fine now. Is this an incompatibility with CompCert 3.7?

[MSoegtropIMC]

@andrew-appel : I enhanced the makefile to support various sources of CompCert, including the two bundled variants, platform supplied variants (default) and also arbitrary sources and installations. I tested all this locally. It might make sense to add a travis test for at least the usual bundled CompCert variant and maybe another one for a few ARM platforms. I hope the make interface and documentation are reasonably clean.

The bundled compcert_new variant does not build - as far as I can tell there are simply missing files in the compcert_new folder.

One note: it might make sense to revise the way VST configures CompCert. It should support substantially more architectures than you can configure this way. With the makefile as is, it should work to point it to arbitrary pre compiled CompCert instances, but it VST compiles the CompCert files it needs, this is substantially more restricted. One option would be to just document this and add a few tests for this to Travis.

Sorry for the delay - it was quite a bit of work.

The version which is in 8.12 beta should be identical in terms of what it builds, but the make file is different. I think we should leave it like this and aim to get this into the 8.12.0 Coq platform release, which I plan to do during this year's Coq workshop.

[MSoegtropIMC]

@andrew-appel : did you have time to look at this?

[andrew-appel]

In BUILD_ORGANIZATION.md, change "nundled_new" to "bundled_new"; change "blow" to "below"; change "does configure" to "configures"; change "teh" to "the".

I have pulled this branch, set COMPCERT=bundled, and using Coq 8.12+beta1 it works just fine. If you can merge the master branch into this branch, so that it's completely up to date w.r.t. the master, then we will be completely ready to merge this pull request into the master.

[MSoegtropIMC]

@andrew-appel : I rebased and fixed the typos.

Please note that the instructions don't apply until the VST opam files are in place. Shall I create VST 2.6 beta opam files as soon as this is merged or wait for a release of VST?

[andrew-appel]

Before I answer the question, "shall we make a VST 2.6", it would be helpful to know, "Is there likely to be a new release of CompCert very soon?" Or even a CompCert 3.7.1 updated for Coq 8.12 and for clightgen's new canonical-identifiers feature. Maybe @xavierleroy can advise . . .

[andrew-appel]

I have tagged the current master branch as v2.6+beta, so you can experiment with making an opam version of VST with that label.

[MSoegtropIMC]

I have tagged the current master branch as v2.6+beta, so you can experiment with making an opam version of VST with that label.

Perfect, I will do the opam files PR tomorrow. It is anyway not much extra work to do a beta and definitely worthwhile for testing.

[MSoegtropIMC]

P.S.: I need this PR merged before I can make the opam files. Opam files for current master without this would be quite different.

[MSoegtropIMC]

Unfortunately the tag is on the wrong commit. How about a tag v2.6-beta-coq-platform?

[andrew-appel]

I suggest you add that tag to the appropriate commit, so there's no confusion.

[liyishuai]

Is it worth having a copy of coq-vst.opam in this repo and check it continuously? per #406 (comment) there will be.
@MSoegtropIMC are you preparing for two OPAM packages, one for released and one for extra-dev?

[MSoegtropIMC]

@liyishuai : the beta will go into extra-dev. As soon as there is a final release it will go into released.

It might make sense to have e.g. a weekly or nightly build of the opam package to see if the dependencies are still in place, but since opam packages usually don't change - one just adds new ones - the risks of failure are pretty slim.

[xavierleroy]

Is there likely to be a new release of CompCert very soon?

I was planning a CompCert release early September, perhaps late August.

[MSoegtropIMC]

I suggest you add that tag to the appropriate commit, so there's no confusion.

I see if this is possible without disabling GitHub's master branch force push protection - I am not sure if this applies to tags.

[Zimmi48]

The protected branch GitHub feature does not apply to tags.

[andrew-appel]

Did you need me to tag the master branch?

[MSoegtropIMC]

@Zimmi48 : thanks for the clarification!

@andrew-appel : I will try today evening (in 5 or 6 hours from now). From what @Zimmi48 said it should work.

[MSoegtropIMC]

@andrew-appel : changing the tag did work. I will create the opam files now.