Compile on Coq Platform in CI

Make sure Prosa compiles cleanly in a default Coq Platform environment.

This will be easy once there's a standard Docker image for Coq Platform.

assigned to @bbb

It’s not exactly what you described, but would you be interested in an esy packaging for Prosa? It’s an npm-like tool designed for reproducibility, by preventing the use of unlisted dependencies and pinning the exact version of each of these (a bit like Opam, but with more guarantees). I think that I can set one up relatively easily if it can help.

Oh, interesting. I'm not familiar with esy at all. What would be the benefit to us?

I started using it when getting a reproducibility issue: I had a Coq repository that compiles on some computer, but not another (probably because of a different version in a dependency that we did not foresee). esy claims to remove/mitigate this kind of issues. They claim to have advantages for compositionality, but as esy is not very much used in the Coq community, I don’t think that this really applies here. It’s more meant for OCaml, but I’m able to use Coq within it.

I think the best would be for me to open a branch and try it out: it should be less than an hour to set it up, and we can then discuss whether it’s a good idea or not.

If you'd like to do that, sure, go ahead and let's see. :-)

That said, I wasn't facing any reproducibility problems. It's just that for new, inexperienced users (like interns), it's easiest to just point at Coq platform and say "go install that". So I'd like to make sure Prosa actually works on that (by all accounts, it currently does, but it's still a good idea to check in CI).

Installation could be an argument for esy, actually: one first have to install esy (through the source or npm—it’s not a JavaScript program by the way: they just use npm as a code hoster), then running it in the repository. This will download and compile all dependencies and compile the repository. (On the bad side, this also means that Coq will be compiled, so the first time, compilation will be slow.)

(I’m feeling like an advertiser of some sorts here, sorry: I’m not saying that this should replace Coq Platform in anyway.)

If it's easy to support, it would be nice to have it. But at least currently I'm comfortable maintaining it, so we'd someone ;-) to promise to take care of it in the foreseeable future.

OK, I did that: ff163b17

At first sight, it seems to work. There are a lot of files in this commit, so just to explain: the package.json is the file I wrote, and everything under esy.lock are files esy generated. They correspond to the precise version or URL of every dependency. It is generally included for reproducibility reasons: assuming that all these URL are sustainable, there is there all the information needed to reproduce exactly the environment I had to compile the source.

There is room for improvement in this branch: there are a lot of warning because $HOME is unset in esy’s environment (to prevent accessing folders like .opam). I could add a fake $HOME within the Makefile to avoid this, by changing the Makefile.patch. (And it has to be in the Makefile and not the environment to enable emacs/CoqIDE to access it.)

It should give an idea on how esy looks like, though

Update: 3424d873 fixes the issue of the warnings.

CC: @mmaida @sbozhko

Marco, Sergey, what do you think?

I don't have a strong opinion. I never had big versioning issues, though this is so because we always make sure to compile on the latest Coq. If this is not intrusive/constraining, we can support it.

Is there a way to support esy without all this stuff below the esy.lock directory? It sort of "pollutes" the diff stat and project history, and it looks like quite version-specific (i.e., will have to be updated frequently).

I agree that it pollutes the history and that it’s going to regularly change. We can ignore it and only commit the package.json file: the esy.lock is useful for reproducability, but I agree that it’s overkill (all versions of everything are stored). Just having the package.json still enables to use esy, but we won’t be assured to have the same version of our dependencies: this means that we would only use esy to have a quick way to install Coq and SSReflect in a container (and I’m fine with this ).

Having just the package.json file sounds like a very good outcome to me. It's a nice feature to have esy support, but having full binary reproducibility is probably a bit overkill for the project at the current stage. And, if I understand correctly, adding the lock files back in (in a separate branch) is trivial if someone really needs full reproducibility.

Would you mind submitting a MR with just the package.json file?

mentioned in merge request !162 (merged)

mentioned in commit 798d2dc5

mentioned in merge request !186 (merged)