热门搜索:
rocq/rocq-prover
rocq
Rocq Prover的Docker镜像，基于Debian 12 Slim和opam 2.x，提供便捷的形式化证明环境，支持稳定版（如9.1、9.0）和开发版（dev）等多种标签，适用于本地开发与CI场景。
2 次收藏下载次数: 0状态：社区镜像维护者：rocq仓库类型：镜像最近更新：14 天前
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：
bashdocker run -it --rm rocq/rocq-prover:9.1 bash
挂载本地项目
将本地项目目录挂载到容器中，进行证明开发：
bashdocker 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,devdev-native-ocaml-4.14.2,dev-native-ocaml-4.14,dev-nativedev-native-ocaml-4.14.2-flambda,dev-native-ocaml-4.14-flambda,dev-native-flambda9.1.0-ocaml-4.14.2-flambda,9.1-ocaml-4.14-flambda,9.1.0,9.1,latest-ocaml-4.14-flambda,latest9.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-native9.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-flambda9.0.1-ocaml-4.14.2-flambda,9.0-ocaml-4.14-flambda,9.0.1,9.09.0.1-ocaml-4.13.1-flambda,9.0-ocaml-4.13-flambda9.0.1-ocaml-4.12.1-flambda,9.0-ocaml-4.12-flambda9.0.1-ocaml-4.09.1-flambda,9.0-ocaml-4.09-flambda9.0.1-native-ocaml-4.14.2,9.0-native-ocaml-4.14,9.0.1-native,9.0-native9.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:<标签>
更多 rocq-prover 镜像推荐
caprover/caprover
caprover
CapRover是一款极易使用的应用/数据库部署与Web服务器管理工具，支持NodeJS、Python、PHP等多种应用及MySQL、MongoDB等数据库，基于Docker、nginx等技术，通过简洁界面提供快速、稳定的服务器管理功能。
30 次收藏1亿+ 次下载
5 个月前更新
apache/skywalking-rover
Apache 软件基金会镜像
Apache SkyWalking Rover是一款指标收集器和基于eBPF的性能分析器，支持C、C++、Golang和Rust语言。
1 次收藏100万+ 次下载
1 年前更新
caprover/cli-caprover
caprover
CapRover CLI工具的Docker镜像，用于自动化部署和管理应用，支持服务器配置、应用部署等操作。
10万+ 次下载
2 个月前更新
caprover/caprover-edge
caprover
该镜像是推送时自动构建的版本，主要用于测试，同时作为简易的应用/数据库部署平台，支持NodeJS、Python、PHP、Ruby、Go等应用，无需Docker和nginx知识即可快速部署。
2 次收藏10万+ 次下载
2 个月前更新
caprover/certbot-sleeping
caprover
修改自certbot/certbot的Docker镜像，通过调整启动配置解决原镜像立即退出问题，支持作为Docker服务持续运行，便于在容器环境中管理SSL证书。
1亿+ 次下载
1 年前更新
caprover/nginx-reverse-proxy
caprover
使用nginx和Docker的非常简单的反向代理
1000万+ 次下载
9 个月前更新
轩辕镜像配置手册
探索更多轩辕镜像的使用方法，找到最适合您系统的配置方式
Docker 配置
登录仓库拉取
通过 Docker 登录认证访问私有仓库
专属域名拉取
无需登录使用专属域名
K8s Containerd
Kubernetes 集群配置 Containerd
K3s
K3s 轻量级 Kubernetes 镜像加速
Dev Containers
VS Code Dev Containers 配置
Podman
Podman 容器引擎配置
Singularity/Apptainer
HPC 科学计算容器配置
其他仓库配置
ghcr、Quay、nvcr 等镜像仓库
Harbor 镜像源配置
Harbor Proxy Repository 对接专属域名
Portainer 镜像源配置
Portainer Registries 加速拉取
Nexus 镜像源配置
Nexus3 Docker Proxy 内网缓存
系统配置
需要其他帮助？请查看我们的 常见问题Docker 镜像访问常见问题解答 或 提交工单
镜像拉取常见问题
使用与功能问题
配置了专属域名后，docker search 为什么会报错？
docker search 限制
Docker Hub 上有的镜像，为什么在轩辕镜像网站搜不到？
站内搜不到镜像
机器不能直连外网时，怎么用 docker save / load 迁镜像？
离线 save/load
docker pull 拉插件报错（plugin v1+json）怎么办？
插件要用 plugin install
WSL 里 Docker 拉镜像特别慢，怎么排查和优化？
WSL 拉取慢
轩辕镜像安全吗？如何用 digest 校验镜像没被篡改？
安全与 digest
第一次用轩辕镜像拉 Docker 镜像，要怎么登录和配置？
新手拉取配置
轩辕镜像合规吗？轩辕镜像的合规是怎么做的？
镜像合规机制
错误码与失败问题
docker pull 提示 manifest unknown 怎么办？
manifest unknown
docker pull 提示 no matching manifest 怎么办？
no matching manifest（架构）
镜像已拉取完成，却提示 invalid tar header 或 failed to register layer 怎么办？
invalid tar header（解压）
Docker pull 时 HTTPS / TLS 证书验证失败怎么办？
TLS 证书失败
Docker pull 时 DNS 解析超时或连不上仓库怎么办？
DNS 超时
docker 无法连接轩辕镜像域名怎么办？
域名连通性排查
Docker 拉取出现 410 Gone 怎么办？
410 Gone 排查
出现 402 或「流量用尽」提示怎么办？
402 与流量用尽
Docker 拉取提示 UNAUTHORIZED（401）怎么办？
401 认证失败
遇到 429 Too Many Requests（请求太频繁）怎么办？
429 限流
docker login 提示 Cannot autolaunch D-Bus，还算登录成功吗？
D-Bus 凭证提示
为什么会出现「单层超过 20GB」或 413，无法加速拉取？
413 与超大单层
账号 / 计费 / 权限
用户好评
来自真实用户的反馈，见证轩辕镜像的优质服务
oldzhang
运维工程师
Linux服务器
5
"Docker访问体验非常流畅，大镜像也能快速完成下载。"