Coq Docker镜像文档（v8.4至8.20）：Rocq-community项目

![pipeline status]([***]

镜像概述和主要用途

本仓库提供Coq证明助手（版本8.4.6至8.20.1） 的Docker镜像，作为Rocq-community项目的一部分进行维护。注意，Coq版本<8.7的Docker标签不再主动重建，因此不会显示在下方的"支持标签"列表中：这些旧版Coq镜像因opam-repository PR #27273（归档了旧版OCaml编译器）而停滞。对于Rocq Prover ≥9.0的最新版本，请使用rocq/rocq-prover镜像。

这些镜像基于coqorg/base父镜像构建，而base镜像本身基于Debian 12 Slim并依赖最新版opam 2.x。

核心功能和特性

• 多版本支持：涵盖Coq 8.4.6至8.20.1的完整版本谱系，满足不同项目的兼容性需求
• 稳定基础架构：基于Debian 12 Slim操作系统，确保运行环境的稳定性和安全性
• 灵活编译配置：提供多种OCaml编译器版本（4.05.0至4.14.2）和优化选项（如flambda优化、native编译）
• 完整工具链集成：预装opam 2.x包管理器，支持无缝安装Coq库和OCaml依赖
• CI/CD友好：配套提供docker-coq-action GitHub Action，便于集成到自动化工作流

使用场景和适用范围

• Coq项目开发：提供隔离的开发环境，避免系统级依赖冲突，支持本地代码挂载和实时编译
• 自动化验证流程：作为CI/CD流水线的基础组件，用于项目构建、证明验证和版本兼容性测试
• 教学与研究：快速部署标准化的Coq环境，适用于形式化方法课程教学或数学定理证明研究
• 跨平台一致性：在不同操作系统（Linux、macOS、Windows）上提供一致的Coq运行环境

详细使用方法和配置说明

支持的标签命名规则

镜像标签采用结构化命名，格式为：
{coq-version}[-ocaml-{ocaml-version}[-{compiler-options}]]

• coq-version：Coq版本号（如8.20.1、8.19）
• ocaml-version：OCaml编译器版本（如4.13.1、4.14.2）
• compiler-options：编译优化选项，包括：
  • flambda：启用OCaml的flambda优化器
  • native：使用Coq native编译模式（提升执行性能）

主要支持标签示例

（完整标签列表见Docker Hub）

基本使用命令

拉取镜像

bash
# 拉取最新稳定版
docker pull coqorg/coq:latest

# 拉取指定版本（示例：Coq 8.20.1 + OCaml 4.13.1 + flambda）
docker pull coqorg/coq:8.20.1-ocaml-4.13.1-flambda

交互式运行Coq顶层（coqtop）

bash
docker run -it --rm coqorg/coq:latest coqtop

挂载本地项目并编译

将当前目录下的Coq项目挂载到容器中进行编译：

bash
# 假设本地项目位于./my_coq_project，包含test.v文件
docker run -it --rm -v $(pwd)/my_coq_project:/workspace coqorg/coq:latest bash

# 在容器内执行编译
cd /workspace
coqc test.v  # 编译单个文件
make  # 若项目包含Makefile，执行完整构建

Docker Compose配置示例

创建docker-compose.yml文件：

yaml
version: '3.8'
services:
  coq-prover:
    image: coqorg/coq:8.20.1-ocaml-4.13.1-flambda
    volumes:
      - ./src:/app/src        # 挂载源代码目录
      - ./theories:/app/theories  # 挂载理论库目录
    working_dir: /app
    command: bash -c "opam update && opam install . --deps-only -y && make"  # 安装依赖并构建

启动服务：

bash
docker-compose up

安装额外依赖

通过opam安装Coq库或OCaml包：

bash
docker run -it --rm coqorg/coq:latest bash

# 在容器内执行
opam update  # 更新包索引
opam install coq-mathcomp  # 安装数学组件库
opam install ocamlformat  # 安装OCaml代码格式化工具

镜像层级和相关资源

注：本Dockerfile仓库在GitLab有镜像，但issues和pull requests仅在GitHub上跟踪。更多使用细节请参考docker-coq wiki。