Subject: Ssreflect Users Discussion List
List archive
- From: Erik Martin-Dorel <>
- To: ,
- Cc: Erik Martin-Dorel <>, Cyril Cohen <>
- Subject: [ssreflect] [ANN] OS+OPAM Upgrade for Docker images of Coq and MathComp
- Date: Fri, 2 Aug 2019 16:06:31 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:rxV/pBZcRhz2GgYmCVvMdRv/LSx+4OfEezUN459isYplN5qZrsi5bnLW6fgltlLVR4KTs6sC17OM9fGxEjBcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmsqQjcssYajIRtJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAOUbPehYoYfzpEYAowWiCgS3Huzj1iVFi2Xq0aEm0eksFxzN0gw6H9IJtXTZtNr7NL0TUeC20aLGyi/Mb+lK2Tf87ojEax4vofaWXb1udcra1E4iGB3fglWVtIPlOCmV2foJs2WA4OpgUPigi28jqw1rvjevwcIsh5DPi4kIxF7E8iB5z5w0Jd2+UEN0fNmkH4dTty6ELYt6WN8tQ2ZtuCoiz70GuIK0fDINyJs83RHQdvOHfJaS4h75SOmRJjJ4iGpqeLK+mxay8VWgxfbmWsao11ZKqzJJktzWuXAXyxzT686HRuJg8UemwzaAyQTT5vtDIUAumqrWLYMqzL0olpcLr0jPAiv7lF/1gaKWbEko5PWk5ub9brjnpZKRMZJ/hBvkPaQ0gMO/BPw1MggQUGif/uSxzLjj8lf4QLVOl/E2jLLZvI3DKcQVp6O0ABVZ0okk6xa4ADem1MoXkWMbI1JCfRKLl4npO1fQL/DkFfqznUignTNxy/3FPrDtGIvBImXBnbv7fLtw6FZQyA8pwtBe45JUBKsBIPX2WkLpqtPUFBo5PBGzw+b9Ftp90pgTWW2KAqCDMaPStUWE6f4oI+mJfIMVoiryK+A55/7yin80gUQdfbKz3ZQJZnC4GuppLFmFYXf3mdcAEWIKvhIkQ+DwiV2CVyRTZ3eoUK4m6DE7EtHuMYCWTYe0xbeFwS2TH5tMZ2kABErIWWzzbYiKX/oHdAqXOdUkkzoeVLHnSok71BjouhWp8bd/Kvvo/XgVr5Pgkt18/fHSk1Q+8iZ5C+yQ1XrIS3BzmCUPXTBl8rp4pBlQ0FaAmY1xmeBZE5l/4OlEVk9uONjZw+tgBtTaVQfIf9PPQ1GjFIb1SQotR848loddK312HM+v21Wah3LzXu0l0oeTDZlxyZrymnj8I8EnliTD3aglykc9G45Baz3gial4+AzeQYXOlhfBzvr4ReEnxCfIsVy74y+WpkgBCVx/VKzEWTYUYU6E9Y2otHOHdKenDPEcCiUEzMeDLqVQbdiw1AdJQf7iPJLVZGfjwmo=
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
--
- [ssreflect] [ANN] OS+OPAM Upgrade for Docker images of Coq and MathComp, Erik Martin-Dorel, 08/02/2019
Archive powered by MHonArc 2.6.18.