mathcomp/mathcomp-dev repository overview

⁠mathcomp/mathcomp-dev

This repository provides Docker⁠ images of the development version (latest build of branch master) of the Mathematical Components⁠ library for the Rocq Prover⁠.

These images are based on the rocq/rocq-prover⁠ images, itself based on Debian 12 Slim⁠ and relying on the last version of opam 2.x⁠.

See also the docker-coq wiki⁠ for details about how to use such images locally or in a CI context.

This Docker registry is populated from math-comp's GitLab CI⁠ but issues⁠ are tracked in the docker-mathcomp GitHub repository.

⁠Note on opam switches

Both mathcomp/mathcomp⁠ stable images and these mathcomp/mathcomp-dev images contain one opam switch (the "default" one from docker-coq⁠).