Docker image of the Rocq Prover (rocq/rocq-prover:9.0)

Announcements
1

Dear Rocq users and developers,

The Rocq Team is happy to announce the immediate availability of the Rocq Prover Docker image 9.0. The Rocq Docker images are an official Rocq project, they are currently maintained in a coq-community GitHub repository but we plan to migrate it to a GitHub repository like https://github.com/rocq-prover/docker-rocq when transitioning to the rocq-prover organization.

  • The Docker image of the Rocq Prover 9.0+rc1 is available when running sudo docker run -it rocq/rocq-prover:9.0, and it is recommended to use neither …:9.0-rc1 nor …:9.0.0 tags but the synonymous tag rocq/rocq-prover:9.0 which will automatically migrate upon 9.0.0’s release.

  • The rocq organization on Docker Hub now has the Sponsored OSS badge (which is useful to lift the docker-pull rate limits).

  • All Docker images for previous versions of Coq ≤ 8.20.1 are kept (and rebuilt) in the coqorg/coq namespace.

  • The dev tag has been removed from the coqorg/coq namespace, it is only available as the rocq/rocq-prover:dev image (and rebuilt at each upstream merge).

  • If you use the docker-coq-action and you use the permissions workaround (cf. the docker-coq-action v1.5.1 release notes): you may need to replace sudo chown -R coq:coq . with sudo chown -R 1000:1000 .

  • If you use the docker-coq-action and the coq_version: field, no further update is needed (it will work out-of-the-box with coq_version: "9.0" and coq_version: "dev").

1 Like