我成功安装了coqc与 Dockerfile 。为什么我需要运行eval $(opam env) 再次当我执行docker时？
##############
# #
# image name #
# #
##############
FROM ubuntu:22.04
#################
# #
# bash > sh ... #
# #
#################
SHELL ["/bin/bash", "-c"]
##########
# #
# update #
# #
##########
RUN apt-get update -y
############################
# #
# minimal set of utilities #
# #
############################
RUN apt-get install curl -y
RUN apt-get install libgmp-dev -y
###########################################
# #
# opam is the easiest way to install coqc #
# #
###########################################
RUN apt-get install opam -y
RUN opam init --disable-sandboxing
RUN eval $(opam env)
#########################################
# #
# install coqc, takes around 10 minutes #
# #
#########################################
RUN opam pin add coq 8.15.2 -y
这是我的使用方法:
$ docker build --tag host --file .\Dockerfile.txt .
$ docker run -d -t --name my_lovely_docker host
$ docker exec -it my_lovely_docker bash
当我在 docker 内时:
root@3055f16a1d78:/# coqc --version
bash: coqc: command not found
root@3055f16a1d78:/# eval $(opam env)
[WARNING] Running as root is not recommended
root@3055f16a1d78:/# coqc --version
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1
最佳答案
Coq 的预构建版本(Debian 内)
如上所述in the comments ，Docker-Coq存储库收集 Coq 的预构建版本，例如:
docker pull coqorg/coq:8.15.2
所有标签的列表可在以下 URL 中找到:
https://hub.docker.com/r/coqorg/coq#supported-tags
相关文档位于此 Wiki 中:
https://github.com/coq-community/docker-coq/wiki
一个独立的 Dockerfile 作为 Ubuntu 的“安装教程”
发送至地址the specific use case OP提到的，这里是一个全面的Dockerfile，它解决了问题中提到的主要问题(为什么当我执行docker时需要再次运行eval $(opam env))，以及遵守标准 Dockerfile 和 opam 指南所必需的几个修复(尽管不会妨碍所涉及的用例):
##############
# #
# image name #
# #
##############
FROM ubuntu:22.04
#################
# #
# bash > sh ... #
# #
#################
SHELL ["/bin/bash", "--login", "-c"]
############################
# #
# minimal set of utilities #
# #
############################
# Run the following as root:
RUN apt-get update -y -q \
&& apt-get install -y -q --no-install-recommends \
# alphabetical order advised for long package lists to ease review & update
ca-certificates \
curl \
libgmp-dev \
m4 \
ocaml \
opam \
rsync \
sudo \
#########################################
# #
# Docker-specific cleanup to earn space #
# #
#########################################
&& apt-get clean \
&& rm -rf /var/lib/apt/lists/*
#####################
# #
# add non-root user #
# (with sudo perms) #
# #
#####################
ARG coq_uid=1000
ARG coq_gid=${coq_uid}
RUN groupadd -g ${coq_gid} coq \
&& useradd --no-log-init -m -s /bin/bash -g coq -G sudo -p '' -u ${coq_uid} coq \
&& mkdir -p -v /home/coq/bin /home/coq/.local/bin \
&& chown coq:coq /home/coq/bin /home/coq/.local /home/coq/.local/bin
###########################################
# #
# opam is the easiest way to install coqc #
# #
###########################################
USER coq
WORKDIR /home/coq
RUN opam init --auto-setup --yes --bare --disable-sandboxing \
&& opam switch create system ocaml-system \
&& eval $(opam env) \
&& opam repo add --all-switches --set-default coq-released https://coq.inria.fr/opam/released \
#########################################
# #
# install coqc, takes around 10 minutes #
# #
#########################################
&& opam pin add -y -k version -j "$(nproc)" coq 8.15.2 \
#########################################
# #
# Docker-specific cleanup to earn space #
# #
#########################################
&& opam clean -a -c -s --logs
###################################
# #
# Automate the 'eval $(opam env)' #
# #
###################################
ENTRYPOINT ["opam", "exec", "--"]
CMD ["/bin/bash", "--login"]
两个 Dockerfile 之间的变化摘要/相关备注
在上面的 Dockerfile 中，已应用以下修复:
- 将连续的
RUN命令与&&合并，以避免此 SO 问题中提出的问题:Purpose of specifying several UNIX commands in a single RUN instruction in Dockerfile . - 将 CLI 标志
-q和--no-install-recommends添加到apt-get命令，以便输出更加简洁，并且安装的软件包仅包含那些指定的(和强制依赖项)。 - 将 APT 软件包按字母顺序排列，以便于审核和更新。
- 添加一个非 root 用户(此处名为
coq)，以便opam不再提示通常的情况[警告] 不建议以 root 身份运行。
当然，在非 Docker 安装中可以跳过此步骤，因为我们总是在标准工作站上安装一些常规的$USER... - 将
opam init命令替换为:
因此opam init --auto-setup --yes --bare --disable-sandboxing \ && opam switch create system ocaml-system~/.profile脚本会自动更新(感谢--auto-setup)以及交换机的名称 (system) 和其内容 (ocaml-system) 是明确的。 - 添加
opam repo add --all-switches --set-default coq-released https://coq.inria.fr/opam/released以便在需要时可以安装社区软件包是，例如:opam install -y -v -j "$(nproc)" coq-mathcomp-ssreflect - 传递
-j "$(nproc)"选项以并行化并加速安装，具体取决于环境系统的核心数量。 - 添加可选的、Docker 特定命令
apt-get clean && rm -rf/var/lib/apt/lists/*和opam clean -a -c -s --logs减少 Docker 层的大小。
回答问题中提出的主要问题
每次启动新的 shell(或
RUN命令等)时，都需要使用eval $(opam env)命令来更新路径等有两种方法可以确保此命令
eval $(opam env)自动完成:- 用
opam exec -- ... 包装命令 - 或者运行
/bin/bash --login，以便获取~/.profile初始化脚本(事实上，这要归功于opam init -- auto-setup是负责使用适当的环境变量等初始化环境 shell 的行，在此脚本中由opam附加)。
- 用
为了完整起见，这两种解决方案都已在这个提议的 Dockerfile 中实现(我们可以保留这两种解决方案，而没有任何特定的缺点)。
测试这一切
$ docker build -t coq-image .
# or better $ docker build -t coq-image --build-arg=coq_uid="$(id -u)" --build-arg=coq_gid="$(id -g)" .
$ docker run --name=coq -it coq-image
# or to mount the current directory
# $ docker run --name=coq -it -v "$PWD:$PWD" -w "$PWD" coq-image
# Ctrl+D
$ docker start -ai coq # to restart the container
# Ctrl+D
$ docker rm coq # to remove the container
关于bash - Dockerfile 中需要冗余 eval $(opam env)，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/72583938/