Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Dear math-comp developers and users,

We are happy to announce the immediate availability of Docker images
of the math-comp library in the Docker Hub registry:
https://hub.docker.com/u/mathcomp/

These images are based on the official images of Coq
https://hub.docker.com/r/coqorg/coq (that are documented in this wiki:
https://github.com/coq-community/docker-coq/wiki) and additionally
contain the coq-mathcomp-character package.

These images are split in two parts:

* Stable versions <https://hub.docker.com/r/mathcomp/mathcomp>
  * mathcomp/mathcomp:1.7.0-coq-8.6 (opam switch: 4.02.3)
  * mathcomp/mathcomp:1.7.0-coq-8.7 (opam switches: 4.05.0, 4.07.0+flambda)
  * mathcomp/mathcomp:1.7.0-coq-8.8 (opam switches: 4.05.0, 4.07.0+flambda)
  * mathcomp/mathcomp:1.7.0-coq-8.9 (opam switches: 4.05.0, 4.07.0+flambda)
  * nightly build of Coq:
    mathcomp/mathcomp:1.7.0-coq-dev (opam switches: 4.05.0, 4.07.0+flambda)

* Development version <https://hub.docker.com/r/mathcomp/mathcomp-dev>:
  * mathcomp/mathcomp-dev:coq-8.6 (opam switch: 4.02.3)
  * mathcomp/mathcomp-dev:coq-8.7 (opam switch: 4.07.0+flambda)
  * mathcomp/mathcomp-dev:coq-8.8 (opam switch: 4.07.0+flambda)
  * mathcomp/mathcomp-dev:coq-8.9 (opam switch: 4.07.0+flambda)
  * nightly build of Coq (at the time math-comp master was built on GitLab 
CI):
    mathcomp/mathcomp-dev:coq-dev (opam switch: 4.07.0+flambda)

So you can now use these images in a CI context, or get a coqtop REPL
with math-comp by running e.g.:

$ docker run --rm -it mathcomp/mathcomp:1.7.0-coq-8.9 rlwrap coqtop

Kind regards,
Erik

-- 
Érik Martin-Dorel, PhD
Maître de Conférences, Lab. IRIT, Univ. Toulouse 3


https://www.irit.fr/~Erik.Martin-Dorel