binghelisp/hol-dev Docker 镜像 - 轩辕镜像
binghelisp/hol-devbinghelisp
HOL定理证明器(HOL4)的CI专用Docker镜像
1 收藏0 次下载
HOL4 Docker镜像文档
镜像概述
本镜像为HOL定理证明器(HOL4)的Kananaskis版本提供CI环境支持，包含完整的系统分发内容，用于自动化构建、测试与持续集成流程。相关在线资源可访问：[***]
核心功能与特性
关键文件
INSTALL：安装说明文档COPYRIGHT：版权声明文件std.prelude：HOL会话启动时默认加载的初始化文件
核心目录结构
bin/：可执行文件存放目录doc/：系统文档（含发布说明）examples/：示例程序集help/：帮助支持文件src/：系统源代码目录tools/：系统构建支持工具集sigobj/：签名与编译代码集合
使用场景
适用于HOL4开发项目的持续集成(CI)环境，支持自动化构建验证、功能测试及版本兼容性检查。
使用方法与配置说明
基础使用流程
- 基于镜像配置CI流水线，利用
tools/目录工具进行系统构建 - 通过
examples/目录示例程序验证核心功能 - 查阅
doc/目录获取系统说明及版本信息
目录挂载建议
如需自定义配置或持久化数据，可挂载以下关键目录：
- 源代码目录：
-v /本地路径/src:/hol/src - 构建产物目录：
-v /本地路径/sigobj:/hol/sigobj - 示例程序目录：
-v /本地路径/examples:/hol/examples
轩辕镜像配置手册
探索更多轩辕镜像的使用方法，找到最适合您系统的配置方式
登录仓库拉取
通过 Docker 登录认证访问私有仓库
Linux
在 Linux 系统配置镜像服务
Windows/Mac
在 Docker Desktop 配置镜像
Docker Compose
Docker Compose 项目配置
K8s Containerd
Kubernetes 集群配置 Containerd
K3s
K3s 轻量级 Kubernetes 镜像加速
Dev Containers
VS Code Dev Containers 配置
MacOS OrbStack
MacOS OrbStack 容器配置
宝塔面板
在宝塔面板一键配置镜像
群晖
Synology 群晖 NAS 配置
飞牛
飞牛 fnOS 系统配置镜像
极空间
极空间 NAS 系统配置服务
爱快路由
爱快 iKuai 路由系统配置
绿联
绿联 NAS 系统配置镜像
威联通
QNAP 威联通 NAS 配置
Podman
Podman 容器引擎配置
Singularity/Apptainer
HPC 科学计算容器配置
其他仓库配置
ghcr、Quay、nvcr 等镜像仓库
专属域名拉取
无需登录使用专属域名
需要其他帮助？请查看我们的 常见问题Docker 镜像访问常见问题解答 或 提交工单
镜像拉取常见问题
轩辕镜像免费版与专业版有什么区别？
免费版仅支持 Docker Hub 访问，不承诺可用性和速度；专业版支持更多镜像源，保证可用性和稳定速度，提供优先客服响应。
轩辕镜像支持哪些镜像仓库？
专业版支持 docker.io、gcr.io、ghcr.io、registry.k8s.io、nvcr.io、quay.io、mcr.microsoft.com、docker.elastic.co 等；免费版仅支持 docker.io。
流量耗尽错误提示
当返回 402 Payment Required 错误时，表示流量已耗尽，需要充值流量包以恢复服务。
410 错误问题
通常由 Docker 版本过低导致，需要升级到 20.x 或更高版本以支持 V2 协议。
manifest unknown 错误
先检查 Docker 版本，版本过低则升级；版本正常则验证镜像信息是否正确。
镜像拉取成功后，如何去掉轩辕镜像域名前缀？
使用 docker tag 命令为镜像打上新标签，去掉域名前缀，使镜像名称更简洁。
用户好评
来自真实用户的反馈，见证轩辕镜像的优质服务
oldzhang
运维工程师
Linux服务器
5
"Docker访问体验非常流畅，大镜像也能快速完成下载。"
咨询镜像拉取问题请 提交工单，官方技术交流群：1072982923
轩辕镜像面向开发者与科研用户，提供开源镜像的搜索和访问支持。所有镜像均来源于原始仓库，本站不存储、不修改、不传播任何镜像内容。