热门搜索:

rocq/rocq-prover

rocq

Rocq Prover的Docker镜像，基于Debian 12 Slim和opam 2.x，提供便捷的形式化证明环境，支持稳定版（如9.1、9.0）和开发版（dev）等多种标签，适用于本地开发与CI场景。

2 次收藏下载次数: 0状态：社区镜像维护者：rocq仓库类型：镜像最近更新：14 天前

让 AI 帮你使用轩辕镜像？ · 展开查看说明

如果你使用 DeepSeek、元宝 AI、Copilot、ChatGPT 等 AI 工具，协助配置轩辕镜像、编写 docker pull 命令、修改 Docker Compose 镜像地址、配置镜像加速、排查镜像拉取失败、分析报错日志等问题，请先让 AI 阅读并遵守轩辕镜像的规则文档。

只需在 AI 对话中先发送下面这句话即可：

请先完整阅读并严格遵守以下文档中的全部规则与要求：

https://xuanyuan.cloud/agents.md

在未充分阅读并理解该文档前，不要生成任何命令、配置、修改建议、故障排查方案或技术回答。后续所有输出都必须严格以该文档中的规范为最高优先级执行。

查看 agents.md 用法指南与完整示范。国内用户首推元宝 AI、DeepSeek 的深度思考模式，不推荐豆包 AI；Cursor 等编辑器可在对话 @ 该链接，或加入 User Rules。若 AI 无法访问外链，可打开说明文档复制全文粘贴。文档会随站点更新，复制内容可能过期，建议定期检查。

镜像标签列表与下载命令

rocq/rocq-prover

该仓库提供Rocq Prover的Docker镜像。

这些镜像基于https://hub.docker.com/r/rocq/base/%E6%9E%84%E5%BB%BA%EF%BC%8C%E8%80%8Crocq/base%E9%95%9C%E5%83%8F%E6%9C%AC%E8%BA%AB%E5%9F%BA%E4%BA%8Ehttps://hub.docker.com/_/debian/%EF%BC%8C%E5%B9%B6%E4%BE%9D%E8%B5%96%E6%9C%80%E6%96%B0%E7%89%88%E6%9C%AC%E7%9A%84opam 2.x：

	GitHub仓库	类型	Docker Hub
	https://github.com/coq-community/docker-coq-action	GitHub Action	N/A
⊙	https://github.com/coq-community/docker-rocq	Dockerfile	https://hub.docker.com/r/rocq/rocq-prover/
↳	https://github.com/coq-community/docker-base	Dockerfile	https://hub.docker.com/r/rocq/base/
↳	Debian	Linux发行版	https://hub.docker.com/_/debian/

有关如何在本地或CI环境中使用此类镜像的详细信息，另请参阅https://github.com/coq-community/docker-coq/wiki%E3%80%82

此Dockerfile仓库在GitLab上有镜像，但https://github.com/coq-community/docker-rocq/issues%E5%92%8Chttps://github.com/coq-community/docker-rocq/pulls%E5%9C%A8GitHub%E4%B8%8A%E8%B7%9F%E8%B8%AA%E3%80%82

[!NOTE]

请注意，本仓库仅包含Rocq Prover ≥9.0的Docker镜像。
对于Coq Proof Assistant ≤8.20.1的早期版本，请使用https://hub.docker.com/r/coqorg/coq%E9%95%9C%E5%83%8F%E3%80%82

[!TIP]

对于大多数使用场景，标签9.1（稳定版）和dev（开发版）最为常用。
建议在CI中省略补丁版本号（使用9.1而非9.1-rc1或9.1.0），这样当Rocq Prover发布新的补丁版本时，无需更改所选的Docker标签。

核心功能与特性

基础架构

底层依赖：基于rocq/base镜像，该镜像构建于Debian 12 Slim之上，确保轻量级且稳定的运行环境
包管理：集成opam 2.x，提供OCaml生态系统的包管理支持，便于依赖管理和环境配置

版本支持

最低版本：仅支持Rocq Prover ≥9.0，早期版本需使用coqorg/coq镜像
多版本覆盖：提供稳定版本（如9.1、9.0系列）和开发版本（dev系列），满足不同阶段的使用需求

标签多样性

版本标识：标签包含Rocq Prover版本（如9.1.0、9.0）、OCaml版本（如4.14.2、4.13.1）、编译特性（如native、flambda）等信息
简化标签：提供省略次要版本或补丁版本的标签（如9.1、latest），便于自动适配更新

使用场景

本地开发

为形式化证明开发提供隔离、一致的环境，避免本地环境配置冲突。

CI/CD集成

可无缝集成到GitHub Actions、GitLab CI等持续集成流程中，实现证明脚本的自动化验证。

版本测试

通过切换不同标签（如稳定版与开发版），便捷测试不同版本Rocq Prover的兼容性。

使用方法

拉取镜像

从Docker Hub拉取指定标签的镜像：

bash
# 拉取稳定版9.1
docker pull rocq/rocq-prover:9.1

# 拉取开发版
docker pull rocq/rocq-prover:dev

运行容器

基本交互式运行

启动容器并进入交互式shell：

bash
docker run -it --rm rocq/rocq-prover:9.1 bash

挂载本地项目

将本地项目目录挂载到容器中，进行证明开发：

bash
docker run -it --rm -v $(pwd):/home/coq/project rocq/rocq-prover:9.1 bash

进入容器后，可在/home/coq/project目录下执行Rocq Prover命令（如rocqtop、rocqc）。

支持的标签及对应Dockerfile链接

dev-ocaml-4.14.2-flambda, dev-ocaml-4.14-flambda, dev
dev-native-ocaml-4.14.2, dev-native-ocaml-4.14, dev-native
dev-native-ocaml-4.14.2-flambda, dev-native-ocaml-4.14-flambda, dev-native-flambda
9.1.0-ocaml-4.14.2-flambda, 9.1-ocaml-4.14-flambda, 9.1.0, 9.1, latest-ocaml-4.14-flambda, latest
9.1.0-native-ocaml-4.14.2, 9.1-native-ocaml-4.14, 9.1.0-native, 9.1-native, latest-native-ocaml-4.14, latest-native
9.1.0-native-ocaml-4.14.2-flambda, 9.1-native-ocaml-4.14-flambda, 9.1.0-native-flambda, 9.1-native-flambda, latest-native-ocaml-4.14-flambda, latest-native-flambda
9.0.1-ocaml-4.14.2-flambda, 9.0-ocaml-4.14-flambda, 9.0.1, 9.0
9.0.1-ocaml-4.13.1-flambda, 9.0-ocaml-4.13-flambda
9.0.1-ocaml-4.12.1-flambda, 9.0-ocaml-4.12-flambda
9.0.1-ocaml-4.09.1-flambda, 9.0-ocaml-4.09-flambda
9.0.1-native-ocaml-4.14.2, 9.0-native-ocaml-4.14, 9.0.1-native, 9.0-native
9.0.1-native-ocaml-4.14.2-flambda, 9.0-native-ocaml-4.14-flambda, 9.0.1-native-flambda, 9.0-native-flambda

镜像拉取方式

您可以使用以下命令拉取该镜像。请将 <标签> 替换为具体的标签版本。如需查看所有可用标签版本，请访问标签列表页面。

轩辕镜像加速拉取命令点我查看更多 rocq-prover 镜像标签

docker pull docker.xuanyuan.run/rocq/rocq-prover:<标签>

使用方法：

DockerHub 原生拉取命令

docker pull rocq/rocq-prover:<标签>

轩辕镜像配置手册

按平台快速找到配置文档

Docker

登录仓库拉取

登录认证 · 私有仓库

专属域名拉取

免登录 · 高速拉取

Linux

Docker 镜像配置

Windows / Mac

Docker Desktop 配置

MacOS OrbStack

OrbStack 容器

Docker Compose

Compose 项目配置

NAS

群晖

Synology 配置

飞牛

fnOS 镜像配置

绿联

绿联 NAS

威联通

QNAP 配置

极空间

极空间 NAS

企业仓库

其他仓库

ghcr · Quay · nvcr

Harbor 镜像源

Proxy Repository 对接

Portainer 镜像源

Registries 配置

Nexus 镜像源

Docker Proxy 缓存

开发工具

Dev Containers

VS Code 开发容器

Podman

Podman 配置指南

Singularity / Apptainer

HPC 科学计算容器

Kubernetes

K8s Containerd

Kubernetes · Containerd

K3s

轻量级集群

面板 / 网络

爱快路由

iKuai 镜像加速

宝塔面板

一键配置镜像源

AI

用 AI 使用轩辕镜像

agents.md · AI 对话 · 提示词

一键安装

一键安装 Docker

Linux Docker 一键安装

需要其他帮助？请查看我们的常见问题 Docker 镜像访问常见问题解答或提交工单

镜像拉取常见问题

功能

免费版与专业版区别

功能对比 · 版本选择

支持的镜像仓库

Docker Hub · GCR · GHCR

新手拉取配置

docker search 限制

专属域名 · Hub 搜索

不支持 push

仅支持 pull · 不支持

拉取速度原因

带宽 · 缓存 · 冷热镜像

错误码

402 与流量用尽

402 · 流量包 · 充值

401 认证失败

401 · docker login

manifest unknown

标签错误 · 镜像不存在

410 Gone 排查

410 · Docker 升级

429 限流

免费版 · 请求频率

其他报错

DNS 超时

DNS 解析 · 网络超时

TLS 证书失败

no matching manifest（架构）

账号

失败是否计费

manifest · blob · 计费

申请开发票（企业 / 个人）

企业 · 个人 · 工单

修改登录密码

网站 · 仓库 · 重置

注销账户

工单 · 数据 · 注销

原理

mirrors 不生效

daemon.json · 重启

去掉域名前缀

docker tag · 重命名

指定架构拉取

ARM64 · AMD64 · 多架构

latest 与「最新」

digest · 版本号 · 标签

查看全部问题→

用户好评

来自真实用户的反馈，见证轩辕镜像的优质服务

oldzhang

运维工程师

Linux服务器

"Docker访问体验非常流畅，大镜像也能快速完成下载。"

热门搜索:

rocq/rocq-prover

rocq

Rocq Prover的Docker镜像，基于Debian 12 Slim和opam 2.x，提供便捷的形式化证明环境，支持稳定版（如9.1、9.0）和开发版（dev）等多种标签，适用于本地开发与CI场景。

2 次收藏下载次数: 0状态：社区镜像维护者：rocq仓库类型：镜像最近更新：14 天前

让 AI 帮你使用轩辕镜像？ · 展开查看说明

只需在 AI 对话中先发送下面这句话即可：

请先完整阅读并严格遵守以下文档中的全部规则与要求：

https://xuanyuan.cloud/agents.md

在未充分阅读并理解该文档前，不要生成任何命令、配置、修改建议、故障排查方案或技术回答。后续所有输出都必须严格以该文档中的规范为最高优先级执行。

镜像标签列表与下载命令

rocq/rocq-prover

该仓库提供Rocq Prover的Docker镜像。

	GitHub仓库	类型	Docker Hub
	https://github.com/coq-community/docker-coq-action	GitHub Action	N/A
⊙	https://github.com/coq-community/docker-rocq	Dockerfile	https://hub.docker.com/r/rocq/rocq-prover/
↳	https://github.com/coq-community/docker-base	Dockerfile	https://hub.docker.com/r/rocq/base/
↳	Debian	Linux发行版	https://hub.docker.com/_/debian/

有关如何在本地或CI环境中使用此类镜像的详细信息，另请参阅https://github.com/coq-community/docker-coq/wiki%E3%80%82

[!NOTE]

请注意，本仓库仅包含Rocq Prover ≥9.0的Docker镜像。
对于Coq Proof Assistant ≤8.20.1的早期版本，请使用https://hub.docker.com/r/coqorg/coq%E9%95%9C%E5%83%8F%E3%80%82

[!TIP]

对于大多数使用场景，标签9.1（稳定版）和dev（开发版）最为常用。
建议在CI中省略补丁版本号（使用9.1而非9.1-rc1或9.1.0），这样当Rocq Prover发布新的补丁版本时，无需更改所选的Docker标签。

核心功能与特性

基础架构

底层依赖：基于rocq/base镜像，该镜像构建于Debian 12 Slim之上，确保轻量级且稳定的运行环境
包管理：集成opam 2.x，提供OCaml生态系统的包管理支持，便于依赖管理和环境配置

版本支持

最低版本：仅支持Rocq Prover ≥9.0，早期版本需使用coqorg/coq镜像
多版本覆盖：提供稳定版本（如9.1、9.0系列）和开发版本（dev系列），满足不同阶段的使用需求

标签多样性

版本标识：标签包含Rocq Prover版本（如9.1.0、9.0）、OCaml版本（如4.14.2、4.13.1）、编译特性（如native、flambda）等信息
简化标签：提供省略次要版本或补丁版本的标签（如9.1、latest），便于自动适配更新

使用场景

本地开发

为形式化证明开发提供隔离、一致的环境，避免本地环境配置冲突。

CI/CD集成

可无缝集成到GitHub Actions、GitLab CI等持续集成流程中，实现证明脚本的自动化验证。

版本测试

通过切换不同标签（如稳定版与开发版），便捷测试不同版本Rocq Prover的兼容性。

使用方法

拉取镜像

从Docker Hub拉取指定标签的镜像：

bash
# 拉取稳定版9.1
docker pull rocq/rocq-prover:9.1

# 拉取开发版
docker pull rocq/rocq-prover:dev

运行容器

基本交互式运行

启动容器并进入交互式shell：

bash
docker run -it --rm rocq/rocq-prover:9.1 bash

挂载本地项目

将本地项目目录挂载到容器中，进行证明开发：

bash
docker run -it --rm -v $(pwd):/home/coq/project rocq/rocq-prover:9.1 bash

进入容器后，可在/home/coq/project目录下执行Rocq Prover命令（如rocqtop、rocqc）。

支持的标签及对应Dockerfile链接

dev-ocaml-4.14.2-flambda, dev-ocaml-4.14-flambda, dev
dev-native-ocaml-4.14.2, dev-native-ocaml-4.14, dev-native
dev-native-ocaml-4.14.2-flambda, dev-native-ocaml-4.14-flambda, dev-native-flambda
9.1.0-ocaml-4.14.2-flambda, 9.1-ocaml-4.14-flambda, 9.1.0, 9.1, latest-ocaml-4.14-flambda, latest
9.1.0-native-ocaml-4.14.2, 9.1-native-ocaml-4.14, 9.1.0-native, 9.1-native, latest-native-ocaml-4.14, latest-native
9.1.0-native-ocaml-4.14.2-flambda, 9.1-native-ocaml-4.14-flambda, 9.1.0-native-flambda, 9.1-native-flambda, latest-native-ocaml-4.14-flambda, latest-native-flambda
9.0.1-ocaml-4.14.2-flambda, 9.0-ocaml-4.14-flambda, 9.0.1, 9.0
9.0.1-ocaml-4.13.1-flambda, 9.0-ocaml-4.13-flambda
9.0.1-ocaml-4.12.1-flambda, 9.0-ocaml-4.12-flambda
9.0.1-ocaml-4.09.1-flambda, 9.0-ocaml-4.09-flambda
9.0.1-native-ocaml-4.14.2, 9.0-native-ocaml-4.14, 9.0.1-native, 9.0-native
9.0.1-native-ocaml-4.14.2-flambda, 9.0-native-ocaml-4.14-flambda, 9.0.1-native-flambda, 9.0-native-flambda

镜像拉取方式

您可以使用以下命令拉取该镜像。请将 <标签> 替换为具体的标签版本。如需查看所有可用标签版本，请访问标签列表页面。

轩辕镜像加速拉取命令点我查看更多 rocq-prover 镜像标签

docker pull docker.xuanyuan.run/rocq/rocq-prover:<标签>

使用方法：

DockerHub 原生拉取命令

docker pull rocq/rocq-prover:<标签>

轩辕镜像配置手册

按平台快速找到配置文档

Docker

登录仓库拉取

登录认证 · 私有仓库

专属域名拉取

免登录 · 高速拉取

Linux

Docker 镜像配置

Windows / Mac

Docker Desktop 配置

MacOS OrbStack

OrbStack 容器

Docker Compose

Compose 项目配置

NAS

群晖

Synology 配置

飞牛

fnOS 镜像配置

绿联

绿联 NAS

威联通

QNAP 配置

极空间

极空间 NAS

企业仓库

其他仓库

ghcr · Quay · nvcr

Harbor 镜像源

Proxy Repository 对接

Portainer 镜像源

Registries 配置

Nexus 镜像源

Docker Proxy 缓存

开发工具

Dev Containers

VS Code 开发容器

Podman

Podman 配置指南

Singularity / Apptainer

HPC 科学计算容器

Kubernetes

K8s Containerd

Kubernetes · Containerd

K3s

轻量级集群

面板 / 网络

爱快路由

iKuai 镜像加速

宝塔面板

一键配置镜像源

AI

用 AI 使用轩辕镜像

agents.md · AI 对话 · 提示词

一键安装

一键安装 Docker

Linux Docker 一键安装

需要其他帮助？请查看我们的常见问题 Docker 镜像访问常见问题解答或提交工单

镜像拉取常见问题

功能

免费版与专业版区别

功能对比 · 版本选择

支持的镜像仓库

Docker Hub · GCR · GHCR

新手拉取配置

docker search 限制

专属域名 · Hub 搜索

不支持 push

仅支持 pull · 不支持

拉取速度原因

带宽 · 缓存 · 冷热镜像

错误码

402 与流量用尽

402 · 流量包 · 充值

401 认证失败

401 · docker login

manifest unknown

标签错误 · 镜像不存在

410 Gone 排查

410 · Docker 升级

429 限流

免费版 · 请求频率

其他报错

DNS 超时

DNS 解析 · 网络超时

TLS 证书失败

no matching manifest（架构）

账号

失败是否计费

manifest · blob · 计费

申请开发票（企业 / 个人）

企业 · 个人 · 工单

修改登录密码

网站 · 仓库 · 重置

注销账户

工单 · 数据 · 注销

原理

mirrors 不生效

daemon.json · 重启

去掉域名前缀

docker tag · 重命名

指定架构拉取

ARM64 · AMD64 · 多架构

latest 与「最新」

digest · 版本号 · 标签

查看全部问题→

用户好评

来自真实用户的反馈，见证轩辕镜像的优质服务

oldzhang

运维工程师

Linux服务器

"Docker访问体验非常流畅，大镜像也能快速完成下载。"

rocq/rocq-prover

Rocq Prover的Docker镜像，基于Debian 12 Slim和opam 2.x，提供便捷的形式化证明环境，支持稳定版（如9.1、9.0）和开发版（dev）等多种标签，适用于本地开发与CI场景。

rocq/rocq-prover

核心功能与特性

基础架构

版本支持

标签多样性

使用场景

本地开发

CI/CD集成

版本测试

使用方法

拉取镜像

运行容器

支持的标签及对应Dockerfile链接

镜像拉取方式

轩辕镜像加速拉取命令点我查看更多 rocq-prover 镜像标签

DockerHub 原生拉取命令

更多 rocq-prover 镜像推荐

caprover/caprover

caprover/cli-caprover

caprover/caprover-placeholder-app

caprover/caprover-edge

caprover/certbot-sleeping

caprover/nginx-reverse-proxy

查看更多 rocq-prover 相关镜像

轩辕镜像配置手册

Docker

登录仓库拉取

专属域名拉取

Linux

Windows / Mac

MacOS OrbStack

Docker Compose

NAS

群晖

飞牛

绿联

威联通

极空间

企业仓库

其他仓库

Harbor 镜像源

Portainer 镜像源

Nexus 镜像源

开发工具

Dev Containers

Podman

Singularity / Apptainer

Kubernetes

K8s Containerd

K3s

面板 / 网络

爱快路由

宝塔面板

AI

用 AI 使用轩辕镜像

一键安装

一键安装 Docker

镜像拉取常见问题

功能

免费版与专业版区别

支持的镜像仓库

新手拉取配置

docker search 限制

不支持 push

拉取速度原因

错误码

402 与流量用尽

401 认证失败

manifest unknown

410 Gone 排查

429 限流

其他报错

DNS 超时

TLS 证书失败

no matching manifest（架构）

账号

失败是否计费

申请开发票（企业 / 个人）