Upon commit 51e2c88557a84ae8a0e9f9a32037af977a8b8768, the Everest Docker image fails to build, because Z3 could not be found in PATH.
Indeed, the abovementioned commit pulls Z3 from FStarLang/binaries and makes PATH point there. This change to PATH is then made in .bashrc , which is not loaded when building the Docker image because .bashrc is only loaded in interactive shells, whereas the shell in which the Docker image is built cannot be interactive.
By contrast, opam init --auto-setup writes its changes to .profile, which is always loaded by login shells, whether interactive or not; thus, the Docker image has been built in such a way that all commands always run in a login shell. This way, OCaml is in the PATH when building the Docker image.
Given all of these, it means that whatever changes to the environment ./everest check is doing should happen in .profile instead of .bashrc for the purpose of building the Docker image.
This pull request offers the user a way to override the destination file into which the variable environment changes are recorded, through the EVEREST_ENV_DEST_FILE environment variable. This new feature is then used when building the everest-chomolungma Docker image, so that the environment variables are changed in .profile instead of .bashrc.
msprotz
commented
7 years ago
Upon commit 51e2c88557a84ae8a0e9f9a32037af977a8b8768, the Everest Docker image fails to build, because Z3 could not be found in PATH. Indeed, the abovementioned commit pulls Z3 from FStarLang/binaries and makes PATH point there. This change to PATH is then made in
.bashrc, which is not loaded when building the Docker image because.bashrcis only loaded in interactive shells, whereas the shell in which the Docker image is built cannot be interactive. By contrast,opam init --auto-setupwrites its changes to.profile, which is always loaded by login shells, whether interactive or not; thus, the Docker image has been built in such a way that all commands always run in a login shell. This way, OCaml is in the PATH when building the Docker image.Given all of these, it means that whatever changes to the environment
./everest checkis doing should happen in.profileinstead of.bashrcfor the purpose of building the Docker image.This pull request offers the user a way to override the destination file into which the variable environment changes are recorded, through the
EVEREST_ENV_DEST_FILEenvironment variable. This new feature is then used when building the everest-chomolungma Docker image, so that the environment variables are changed in.profileinstead of.bashrc.