run test and compile-test jobs in CI with different emacs versions

[hendriktews]

@erikmd : Do you have plans/ideas about running the coq related tests in CI with different emacs versions?

After looking a bit around I see three options:

• install emacs via nix in the coq containers
• base the coq containers on debian stretch, which has packages emacs24 and emacs25
• use nix in the same way as purcell/setup-emacs for different coq versions

[hendriktews]

I have Dockerfile's now for creating docker images with arbitrary coq and emacs combinations. They are based on the coqorg/coq images and add emacs via nix. Using these images in CI would have caught #534. @erikmd : Do you have any opinion about creating a PR for those Dockerfile's in the coq-community/docker-coq repo?

[erikmd]

Hi @hendriktews, thanks a lot for looking at this!

and sorry for being less responsive… the Spring term is going to resume on Jan 4th so I'm extremely busy these days.

Some first comments:

• I had done some experiments with dockerizing emacs (both -nox and graphical version), just with the standard Debian packages, but not with Nix, and what you propose (testing more emacs × coq combinations) definitely seems the way to go;
• basing the images upon coqorg/coq then adding emacs thanks to Nix seems a nice strategy;
• but I wouldn't suggest to add emacs readily "upstream" in coqorg/coq because:
  • emacs is not useful for most people using coqorg/coq (the main use case being CI for projects independently of the front-end)
  • that would add a large commitment on the size of the "build matrix" (ocaml × coq × emacs)
• however, I guess the docker-keeper infrastructure I now use to maintain coqorg/coq could be used to easily build (using your Dockerfiles and a GitLab CI pipeline) then automatically deploy Docker images of coq+emacs.

maybe we could arrange some video call (e.g. from mid-January) to discuss this topic further and implement this idea?

[erikmd]

BTW−FYI, I had already created (to save the name) a Docker Hub organization at URL https://hub.docker.com/u/proofgeneral, so we may use it for hosting some of these images :)

[hendriktews]

and sorry for being less responsive… the Spring term is going to resume on Jan 4th so I'm extremely busy these days.

No problem!

* basing the images upon coqorg/coq then adding emacs thanks to Nix seems a nice strategy;

I use two stages of course. The first adds nix and the second adds emacs. nix seems to have only nox emacs versions, but this is probably fully sufficient.

* but I wouldn't suggest to add emacs readily "upstream" in coqorg/coq because:

Sure.

* however, I guess the [docker-keeper] infrastructure I now use to maintain coqorg/coq could be used

OK, I'll try this.