This switches the CI to use opam to build dependencies -- the only mode that will be supported on the new CI machine. opam is also used to cache build dependencies, so we no longer rely on keeping old files in the CI directory. (The build mode can be set to "git clone" once this is merged.) It is also trivial now to change the Coq version that is used. If you want, I can add a second job that builds GPS against Coq 8.6.dev (the current revision of the 8.6 branch), or we could even entirely ditch Coq 8.5 and build only against 8.6.dev. (Iris is currently tested against both 8.5.3 and 8.6.dev; we will use the dev version only until 8.6 is released, of course.) You can also easily use
make quick && make vio2vo or so instead of just
make because this no longer needs Iris to be built the same way.
There are two observable differences for the user:
- No more iris submodule. Instead, the file opam.pins tracks the git commit of Iris that is to be used. As a user,
make build-depwill use opam to install and/or upgrade everything you need (Coq, ssreflect, Iris) in the right version. Of course you can still do
make installin Iris manually if you don't want to or can't use opam.
- No more separate stages for updating build-deps and building GPS itself. If you really want to keep those separate, I can make that happen, but it will overall slow things down because the cache has to be copied back and forth. (Also, it may break if we ever have two CI runners.)
- Which name should this project have in opam? I picked
- I didn't know of any homepage for this project so currently, opam doesn't give any.
- The folder structure is somewhat weird because unlike the other projects,
_CoqProjectare in the same folder that is mapped as library folder for Coq. I made things work by adding a
cdhere and there, but the nicer thing to do would be to rename
- Currently, if you
make installthis project, stuff is installed to a folder
ra. This is determined by the first line in
_CoqProject. It should probably be changed (and then the
opamfile also needs changing because it uninstalls things by deleting that directory).