redundant eval $(opam env) needed in Dockerfile

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

Solution

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