use opam-based CI
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-dep
will use opam to install and/or upgrade everything you need (Coq, ssreflect, Iris) in the right version. Of course you can still domake install
in 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.)
TODOs:
- Which name should this project have in opam? I picked
coq-gps
. - 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,
Makefile
and_CoqProject
are in the same folder that is mapped as library folder for Coq. I made things work by adding acd
here and there, but the nicer thing to do would be to renamecoq/ra
tocoq/theories
and moveMakefile
and_CoqProject
up intocoq
. - Currently, if you
make install
this project, stuff is installed to a folderra
. This is determined by the first line in_CoqProject
. It should probably be changed (and then theopam
file also needs changing because it uninstalls things by deleting that directory).