Dockerfile中需要的冗余评估$（OPAM ENV）

Question

我成功安装了 coqc dockerfile 。当我执行Docker时，为什么我需要运行 evary $（opam env） 再次？

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

Answer 1

”

如上所述， docker-coq repository coq的储存库，例如

docker pull coqorg/coq:8.15.2

：所有标签都可以在此URL上找到：

https：// https：///hub.dub.dub.dub.dhub.com/ r/coqorg/coq＃support-tags

和相关的文档在此Wiki中：

https://github.com/coq-community/docker-coq/wiki

for ubuntu供ubuntu进行自我控制的dockerfile作为“安装教程”，

以地址问题中提到的问题（当我执行Docker 时，我为什么需要再次运行 evar> evar> evar>（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的两个dockerfiles /相关备注之间的变化摘要

，已应用以下修复程序：

• Merge conterge incore Run < / code> commands命令使用＆amp;＆amp; 避免在此问题中提出的问题：。
• 添加CLI标志 -Q 和 - no-install-recommends apt-get 命令，以便输出较少的冗长，并且仅安装软件包包括指定的软件包（和强制性依赖项）。
• 按字母顺序将APT软件包放置，以简化审核和更新。
• 在此处添加一个非root用户（在此处添加 coq ），以便 opam 不再向常规 [警告]作为root运行的情况不推荐。
  当然，可以在非偶数安装中跳过此步骤，因为我们始终在标准工作站上安装了一些常规 $ user ……
• 用以下方式替换 opam init 命令：
  在
  ＆amp;＆amp; OPAM开关创建系统OCAML-System

  因此，〜/.profile 脚本是自动更新的（感谢 - 自动设置）和Switch的名称（ System ）和它的内容（ OCAML-SYSTEM ）是明确的。

• 添加 OPAM回购添加 - all-switches -set-default coq-Real https://coq.inria.fr/opam/released ，这样就可以在需要时安装社区软件包，例如，例如：

    opam install-y -v -j“ $（nproc）” coq-mathcomp-sreflect
   

• 通过 -J“ $（NPROC）” 选项，取决于安装并加速安装，具体取决于环境系统的内核数。
• 添加可选的， docker特定命令 apt-get clean＆amp;＆amp; rm -rf/var/lib/apt/lists/*和 opam清洁-a -c -s -logs 以减小码头层的大小。

中提出的主要问题

• 每次启动新的shell（或 Run 命令等）中提出的主要问题

  ，命令是更新 path 等。

• 有两种方法可以确保此命令 eval $（opam env）是自动完成的：：

  • 用 opam exec将命令包裹 - …
  • 或运行/bin/bash - -login ，以便〜/.profile init脚本是源源（实际上，感谢 opam init- Auto-Setup ，负责使用适当的环境变量初始化环境外壳等的线，此脚本中的 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