This repository provides a Docker image with MathComp-Analysis installed on top of a Rocq base image. The image is intended for users who want a ready-to-use environment for formalizing mathematics with the Rocq prover and the MathComp-Analysis library.

• Based on the rocq/rocq-prover Coq Docker image
• Pre-installed MathComp-Analysis library
• Fully configured OPAM environment for Coq development

The prebuilt image is available on Docker Hub: https://hub.docker.com/r/yoshihiro503/mathcomp-analysis

You can pull it directly with:

docker pull yoshihiro503/mathcomp-analysis

Launch a container with an interactive shell:

docker run -it --rm yoshihiro503/mathcomp-analysis:1.14.0-rocq-9.0 /bin/bash

Once inside, you can see the environment.

rocq -v
opam list

You can build the image locally using the provided build.sh script:

./build.sh

This script will:

1. Build a docker image
2. Push the image to Docker Hub

You can customize the base image or the MathComp-Analysis version by modifying the Dockerfile or passing build arguments:

docker build --build-arg BASE="rocq/rocq-prover:9.0" \
             --build-arg ANALYSIS_VERSION="1.14.0" \
             -t yourusername/mathcomp-analysis .

This repository and Docker image are released under the MIT License.