Dockerfile执行eval $(opam env)后 进容器为何仍需重跑才能用coqc

eval $(opam env)的生效范围仅限执行该命令的当前shell进程，它的本质是在当前shell内临时修改PATH、OCaml相关环境变量，进程退出后所有修改都会直接丢弃，不会持久化。

Docker构建时的每一条RUN指令都会启动一个独立的临时shell进程，执行完成后该进程立刻销毁，进程内设置的所有环境变量都不会保留到后续构建层，更不会自动注入到容器启动后的新shell进程中：

• 你在Dockerfile中写的单独RUN eval $(opam env)执行完就随临时进程销毁，没有任何持久化效果
• 后续执行opam pin add coq 8.15.2是在另一个全新的独立shell进程中运行，本身也没有继承上一层RUN设置的环境
• 你通过docker exec进入容器启动的bash是全新进程，没有加载opam的环境配置，自然找不到coqc命令，手动执行eval $(opam env)本质是给当前这个新shell重新注入一遍环境变量，之后才能正常找到命令。

选任意一种即可，不需要重复操作：

• 把opam环境配置写入全局bash启动脚本，所有新启动的bash会自动加载配置，无需手动执行eval。在Dockerfile安装完coq后新增一行：

  RUN echo 'eval $(opam env)' >> /etc/bash.bashrc
  

• 直接将opam的可执行文件目录加入全局PATH，这是最轻量的方案，coqc找不到的核心原因就是opam的bin目录不在默认PATH中。一般opam默认安装的bin路径为/root/.opam/default/bin，在Dockerfile中新增ENV指令即可：

  ENV PATH="/root/.opam/default/bin:${PATH}"
  

  如果coq运行依赖其他opam设置的环境变量，可以直接把opam env输出的所有变量导出为全局镜像环境变量。
• 注意：如果构建阶段就需要用到opam环境下的命令，不要把eval $(opam env)拆成单独的RUN指令，要和后续命令放在同一个RUN层执行，保证同属一个shell进程：

  RUN eval $(opam env) && opam pin add coq 8.15.2 -y
  

  这个修改仅能保证构建阶段的命令能找到opam环境，容器启动后的环境问题还是需要配合前两种方案解决。

原Dockerfile #

##############
#            #
# 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

原复现现象 #

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

内容的提问来源于stack exchange，提问作者OrenIshShalom