Docker image for 8.12 · Coq users

@Erik Martin-Dorel just wanted to check whether it's on the table to set up a Docker image for the 8.12 alpha (rebuilt daily as for dev?), or if you prefer to wait for the beta?

Karl Palmskog (Jun 07 2020 at 16:25):

the main benefit (of image for 8.12 alpha) is that coq-community projects can test 8.12 using opam even before the beta.

Théo Zimmermann (Jun 07 2020 at 16:26):

Note that the beta should come pretty soon (at least the tag, I'd bet on Tuesday).

Erik Martin-Dorel (Jun 07 2020 at 16:26):

Sure @Karl Palmskog, this had been working for 8.11 alpha so I can re-enable that feature for 8.12 alpha indeed, thanks for the heads-up.
I'll post again when this is ready.

Also I'm working on migrating the infra from "Docker Hub automated builds" to GitLab CI for upcoming builds; the migration takes some time but I hope this will be ready for 8.12.0… (BTW, is there a known tagging date for 8.12.0?)

Erik Martin-Dorel (Jun 07 2020 at 17:24):

coq is now pinned to git+https://github.com/coq/coq#1b55bd6967590d1b41560b45f00b588b54ef7899 (version 8.12+alpha)
+ opam install -y -v -j 2 coq coq-bignums

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq.8.12+alpha: git]
[coq.8.12+alpha] no changes from git+https://github.com/coq/coq#1b55bd6967590d1b41560b45f00b588b54ef7899
The following dependencies couldn't be met:
- coq-bignums -> coq (< 8.12~ | >= dev)
not available because the package is pinned to version 8.12+alpha
No solution found, exiting
'opam install -y -v -j 2 coq coq-bignums' failed.

Erik Martin-Dorel (Jun 07 2020 at 17:37):

Karl Palmskog (Jun 07 2020 at 18:08):

merged now. Will coq-bignums.8.12.dev work for Coq 8.12+beta1 image, or do we need a release coq-bignums.8.12+beta1 in opam there?

Théo Zimmermann (Jun 07 2020 at 18:08):

Erik Martin-Dorel (Jun 07 2020 at 18:10):

thanks @Karl Palmskog ; yes it will smoothly work for Coq 8.12+beta1 as coqorg/coq:8.12-beta1 will incorporate the core-dev and extra-dev packages, and the version string will be compatible, so I guess there's no need to create yet another package of bignums in extra-dev

Karl Palmskog (Jun 07 2020 at 18:16):

@Erik Martin-Dorel what was the issue with dune and bignums? ... Ah, it's the native compilation, still, right?

Erik Martin-Dorel (Jun 07 2020 at 18:22):

@Karl Palmskog yes, when we had tested bignums with native_compute some time ago with @Pierre Roux (cf. https://github.com/coq/coq/issues/11476 for more context), the workaround we found was to switch to coq_makefile (just temporarily of course, but it seemed to me just now that it was better to have the various bignums .opam files rely on the same build system, just for consistency / principle of least surprise) → hence the PR https://github.com/coq/opam-coq-archive/pull/1278

Erik Martin-Dorel (Jun 07 2020 at 19:14):

@Karl Palmskog the coqorg/coq:8.12-alpha image is available (with OCaml 4.05.0 and 4.07.1 like the other current images):

$ docker pull coqorg/coq:8.12 && \
  docker run --rm -it coqorg/coq:8.12 bash -c 'coqtop --version; opam list'
…
The Coq Proof Assistant, version 8.12+alpha (June 2020)
compiled on Jun 7 2020 18:33:59 with OCaml 4.05.0
# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 base        Num library distributed with the OCaml compiler
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-m4                  1           Virtual package relying on m4
coq                      8.12+alpha  pinned to version 8.12+alpha at git+https://github.com/coq/coq#1b55bd6967590d1b41560b45f00b588b54ef7899
coq-bignums              8.12.dev    Bignums, the Coq library of arbitrary large numbers
dune                     2.5.1       pinned to version 2.5.1
num                      0           pinned to version 0
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.8.1       pinned to version 1.8.1
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compiler
opam-depext              1.1.3       Query and install external dependencies of OPAM packages

Karl Palmskog (Jun 07 2020 at 19:28):

many thanks, will set up to use this in at least aac-tactics and stalmarck in coq-community

Erik Martin-Dorel (Jun 07 2020 at 19:35):

also just FYI, regarding the opam switches, the coqorg/coq images still have two switches (4.05.0 and 4.07.1+flambda), but there is also (not-yet-documented) images with OCaml 4.09.0+flambda (e.g., coqorg/coq:8.11-alpha-ocaml-4.09.0-flambda), that will be ultimately migrated to OCaml 4.09.1+flambda… and announced in the wiki!

Karl Palmskog (Jun 07 2020 at 19:37):

@Erik Martin-Dorel I've seen information about those floating by, thanks. What we need to do in the templates is to allow configuring arbitrary Docker images, I'll try to address this issue in the next week: https://github.com/coq-community/templates/issues/39

Karl Palmskog (Jun 07 2020 at 19:38):

yeah the OPAM ci seems to currently take about 2x the time of the Nix ci, probably flambda would help.

Karl Palmskog (Jun 07 2020 at 19:42):

the amount of expertise needed to build Coq stuff from scratch in all various environments is just ridiculous, or getting ridiculous

Erik Martin-Dorel (Jun 07 2020 at 19:43):

also basically there is already a 2x slowdown in the download time :-) explained by the fact coqorg/coq:8.12 (for example) contains two opam switches! but I plan to finalize https://github.com/coq-community/docker-coq/issues/4 next week as well, in order to have single-switches images (that could just as well be combined with the coq-community/templates feature issue you mention). I'll ping you when it is ready.

Erik Martin-Dorel (Jun 07 2020 at 19:46):

I'd not be that pessimistic :-) DevOps matters and/or build automation is known be time-consuming in general… anyway I guess your remark is not specific to Coq: e.g., when I had tried compiling learn-ocaml on Windows for the first time, it had been very difficult!

Karl Palmskog (Jun 07 2020 at 19:51):

I guess the issue itself is not tightly tied to Coq, but since we are in some sense one additional layer of complexity on top of OCaml's infrastructure, that brings with it some ties to the system level one might not have on a "virtual machine" platform, like Java

Stream: Coq users

Topic: Docker image for 8.12

Karl Palmskog (Jun 07 2020 at 16:23):