Skip to content

use opam-based CI

Ralf Jung requested to merge opam-ci into master

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 do make 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 a cd here and there, but the nicer thing to do would be to rename coq/ra to coq/theories and move Makefile and _CoqProject up into coq.
  • Currently, if you make install this 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 opam file also needs changing because it uninstalls things by deleting that directory).

Cc @janno @haidang

Merge request reports