coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Erik Martin-Dorel <e.mdorel AT gmail.com>
- To: coq-club AT inria.fr, ssreflect AT msr-inria.inria.fr
- Cc: Erik Martin-Dorel <erik.martin-dorel AT irit.fr>, Cyril Cohen <cyril.cohen AT inria.fr>
- Subject: [Coq-Club] [ANN] OS+OPAM Upgrade for Docker images of Coq and MathComp
- Date: Fri, 2 Aug 2019 16:06:31 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e.mdorel AT gmail.com; spf=Pass smtp.mailfrom=e.mdorel AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f66.google.com
- Ironport-phdr: 9a23:aWHDaBZDbeUD3bhn1cJc1zP/LSx+4OfEezUN459isYplN5qZpsy6ZR7h7PlgxGXEQZ/co6odzbaP6eaxCCdcvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6twHcu80ZjYZtJas61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOJ+ZWr4fzqVgToxWgGQahH/ngxiNSi3LswaE2z+YsHAfb1wIgBdIOt3HUoc36OqcIUOC1z7TDwzLZYPNMxTf96Y7Ifgkvr/GLR7J/b87RwlQoGgzblFmQrJHqPzSP1usTt2iW9OVgVee1hG4mrwF9uCSgxsApioTQgI8e117K9SJ8wIkvJN24TlZ2bsOjEJRMtCGVKZF2Ttk+TGFvvSY20rgGuZ+ncygQz5Qo3ATQZOGIc4eW+BLvTvqeITB9hH59d7K/hgqy8Ui9yuLnTMW7zFFKri9dntnJrH8NzQDT6smBSvdk40ih3iyP2B7X6u1eJkA0j6XbJpg8ybAzjpoeqVrPEjPylUnsj6Kbdl8o9va15+nleLnrp56ROolpgQ/kKKsugNawAeEgPwgOQWeb/eO82aXm/ULjQbVKiuQ6krfCsJzHPMgbqK+0Dg5P3oYs7Ba/CDim0NAGknUdMF1FfxeHg5DoO1HIPv/4Ee+yj0qwnDpv3fzLPb3sDo/TInTekrrtZ7dw5k9ExAo2199f5pZUCr8bIPL0X0/8rMLXAgU8MwOpxObnEsty1ocFVGKAB6+WKqLSsVuS6u0zJOmMYZcZuCzhJPg9+/7ukXg5lEcBcqmuxJsbcWy3HvB7I0qCenfsmdcAEWISvgUkVuDqiVuCUSRSZ3moRa486Cs7Apq8DYjfXoCtnKCB3CCjE5JKem9GDVCMHmnud4ifWvYMaSeSLdR7kjMeT7ShSokh1QuvtADg0bZnIPDUqWUkssfo08Ew7OnOnzkz8yZ1BoKTySXFVHpuk20MSjQq9KVkuwl8zE2C2O55heZZHJpd/aBzXx8+JKLbmuFgCtO0XwvbYtaPDVqhWNiiKTw3VZc10tgIJUFnFIaMlBfGigewArxdsrWRGJ0yt47bxXX1b5JwjXPK07Msi3EpR8JOMSutgasppFubPJLAj0jMz/XiTq8bxiOYsT7blTPS7nEdaxZ5VOD+ZV5aflHf9I2r6UbLTrvoArMiYFMYlJyyb5BSY9istm1oAffuPNOEPjC0kma0QAiTn/aCMtSsdGIa0yHQTkMDllJLpCfUBU0FHi6k5lnmInlrHFPrbVnr9LAn+ny+R04wiQqNah842g==
Dear Coq users and developers,
For your information, the following Docker Hub repositories have been recently updated to use the latest release of Debian stable (Debian 10) and OPAM (2.0.5):
https://hub.docker.com/r/coqorg/coq
https://hub.docker.com/r/mathcomp/mathcomp
https://hub.docker.com/r/mathcomp/mathcomp-dev
The Docker images gathered there can thus be used to setup Continuous Integration for your projects (e.g., using Travis CI or GitLab CI, see [1]), or to do some experiments with a specific version of Coq, e.g.:
$ docker pull coqorg/coq:8.10
other examples:
$ docker pull mathcomp/mathcomp:latest-coq-dev
$ docker run --rm -it mathcomp/mathcomp:latest-coq-dev opam list
$ docker pull mathcomp/mathcomp-dev:coq-dev
$ docker run --rm -it mathcomp/mathcomp-dev:coq-dev opam list
Note 2: The detail of the opam switches and packages available in the coqorg/coq images is described in the front page of the wiki, see [3].
Note 3: coqorg/coq:dev and the two other images based upon it that are mentioned above, are rebuilt every night from 00:15 UTC+2. Then, the underlying Coq commit can be seen from the badge "commit" on page [4] or from the metadata at URL [5] or directly by using the "opam show" command after fetching the image:
$ docker pull coqorg/coq:dev
$ docker run --rm -it coqorg/coq:dev opam show -f pin coq
git+https://github.com/coq/coq#8f52956f5b19b3b80b1cd6155e28e0af265f2d79
$ docker run --rm -it coqorg/coq:dev opam show -f source-hash coq
8f52956f
No compatibility issue is expected w.r.t. the previous version of the images that used Debian 9, and we recall that you may use following command (mentioned in [1]) to install additional Debian packages in containers derived from coqorg/coq:
$ sudo apt-get update -y -q && \
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q $package_names
[5] https://microbadger.com/images/coqorg/coq:dev
Kind regards,
Erik
--
For your information, the following Docker Hub repositories have been recently updated to use the latest release of Debian stable (Debian 10) and OPAM (2.0.5):
https://hub.docker.com/r/coqorg/coq
https://hub.docker.com/r/mathcomp/mathcomp
https://hub.docker.com/r/mathcomp/mathcomp-dev
The Docker images gathered there can thus be used to setup Continuous Integration for your projects (e.g., using Travis CI or GitLab CI, see [1]), or to do some experiments with a specific version of Coq, e.g.:
$ docker pull coqorg/coq:8.10
$ docker run -it coqorg/coq:8.10
(coqorg/coq:8.10 being currently an alias of coqorg/coq:8.10-beta2)other examples:
$ docker pull mathcomp/mathcomp:latest-coq-dev
$ docker run --rm -it mathcomp/mathcomp:latest-coq-dev opam list
$ docker pull mathcomp/mathcomp-dev:coq-dev
$ docker run --rm -it mathcomp/mathcomp-dev:coq-dev opam list
Note 1: Guidelines to install Docker on one's personal workstation
are also available in the docker-coq wiki [2] (but it is not necessary to do
so for preparing a CI configuration for Travis or GitLab).
$ docker pull coqorg/coq:dev
$ docker run --rm -it coqorg/coq:dev opam show -f pin coq
git+https://github.com/coq/coq#8f52956f5b19b3b80b1cd6155e28e0af265f2d79
$ docker run --rm -it coqorg/coq:dev opam show -f source-hash coq
8f52956f
No compatibility issue is expected w.r.t. the previous version of the images that used Debian 9, and we recall that you may use following command (mentioned in [1]) to install additional Debian packages in containers derived from coqorg/coq:
$ sudo apt-get update -y -q && \
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q $package_names
[5] https://microbadger.com/images/coqorg/coq:dev
Kind regards,
Erik
--
- [Coq-Club] [ANN] OS+OPAM Upgrade for Docker images of Coq and MathComp, Erik Martin-Dorel, 08/02/2019
Archive powered by MHonArc 2.6.18.