redundant eval $(opam env) needed in Dockerfile

Question

I successfully installed coqc with Dockerfile. Why do I need to run eval $(opam env) again when I execute the 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

Here is how I use it:

$ docker build --tag host --file .\Dockerfile.txt .
$ docker run -d -t --name my_lovely_docker host
$ docker exec -it my_lovely_docker bash

And when I'm inside the 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

Prebuilt versions of Coq (within Debian)

As mentioned in the comments, the Docker-Coq repository gathers prebuilt versions of Coq, e.g.:

docker pull coqorg/coq:8.15.2

The list of all tags is available at this URL:

https://hub.docker.com/r/coqorg/coq#supported-tags

and the related documentation is in this Wiki:

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

A self-contained Dockerfile as an "installation tutorial" for Ubuntu

To address the specific use case mentioned by the OP, here is a comprehensive Dockerfile that solves the main issue mentioned in the question (Why do I need to run eval $(opam env) again when I execute the docker), along with several fixes that are necessary to comply with standard Dockerfile and opam guidelines (though don't hinder the use case at stake):

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

Summary of changes between both Dockerfiles / related remarks

In the Dockerfile above, the following fixes have been applied:

• Merge consecutive RUN commands with && to avoid the issue raised in this SO question: Purpose of specifying several UNIX commands in a single RUN instruction in Dockerfile.
• Add CLI flags -q and --no-install-recommends to apt-get commands, so that the output is less verbose, and the installed packages only include those specified (and mandatory dependencies).
• Put the APT packages in alphabetical order, to ease review and update.
• Add a non-root user (named coq here) so that opam does not complain anymore with the usual [WARNING] Running as root is not recommended.
  Of course, this step can be skipped in a non-Docker installation as we always have some regular $USER installed on a standard workstation…
• Replace the opam init command with:

  opam init --auto-setup --yes --bare --disable-sandboxing \
  && opam switch create system ocaml-system
  

  so the ~/.profile script is updated automatically (thanks to --auto-setup) and the name of the switch (system) and its content (ocaml-system) is explicit.
• Add opam repo add --all-switches --set-default coq-released https://coq.inria.fr/opam/released so that one can then install community packages if need be, e.g.:

  opam install -y -v -j "$(nproc)" coq-mathcomp-ssreflect
  

• Pass the -j "$(nproc)" option to parallelize and speedup the installation, depending on the number of cores of the ambient system.
• Add optional, Docker-specific commands apt-get clean && rm -rf /var/lib/apt/lists/* and opam clean -a -c -s --logs to reduce the size of the Docker layers.

Answer to the main issue raised in the question

• Each time a new shell (or a RUN command, etc.) is launched, the eval $(opam env) command is necessary to update the PATH etc.

• There are two ways to ensure that this command eval $(opam env) is done automatically:

  • either wrap the command with opam exec -- …
  • or run /bin/bash --login, so that the ~/.profile init script is sourced (indeed, thanks to opam init --auto-setup, a line in charge of initializing the ambient shell with proper environement variables and so on, was appended by opam in this script).

• For completeness, both solutions have been implemented in this proposed Dockerfile (and we can just keep both without any specific drawback).

To test all this

$ 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