Skip to content

Commit

Permalink
user.sh: put env settings in /etc/bash.bashrc
Browse files Browse the repository at this point in the history
The user home is a docker volume, which is persistent between container
runs and cannot be mounted during image building.

Store env settings like PATH and other variables in container-global
/etc/bash.bashrc instead of user ~/.bashrc so that changes to these
variables during image build become visible without deleting the volume.

Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
lsf37 committed May 22, 2024
1 parent 361e0e2 commit cb742b5
Showing 1 changed file with 15 additions and 18 deletions.
33 changes: 15 additions & 18 deletions scripts/utils/user.sh
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,8 @@ EOF

mkdir "/home/${UNAME}"

# Put in some branding
# Put in some branding. This is in the volume, so it can be edited/removed by
# the user.
# shellcheck disable=SC2129
cat << EOF >> "/home/${UNAME}/.bashrc"
echo '___ '
Expand All @@ -97,29 +98,25 @@ echo ' / '
echo 'Hello, welcome to the seL4/CAmkES/L4v docker build environment'
EOF

# This is a small hack. When the dockerfiles are building, many of
# the env things are set into the .bashrc of root (since they're
# building as the root user). Here we just copy all those declarations
# and put them in this user's .bashrc.
# This can be an issue with regard to the NOTE above, about docker
# volumes.
grep "export" /root/.bashrc >> "/home/${UNAME}/.bashrc"

# Note that this block does not do parameter expansion, so will be
# copied verbatim into the user's .bashrc.
# We use this to ensure they have the repo program in their path,
# that they pick up any potentially present Haskell installation,
# and to ensure they start in the /host dir (aka, their own file
# path)
cat << 'EOF' >> "/home/${UNAME}/.bashrc"
# Since the user home is mounted as a volume, we do not write to ~/.bashrc, but
# modify the system-wide bashrc instead. /etc/profile.d/ does not work, because
# it's not a login shell.
#
# When the dockerfiles are building, many of the env settings are written into
# /root/.bashrc by various install tools. We copy all those declarations.
RC_FILE="/etc/bash.bashrc"
grep "export" /root/.bashrc >> "${RC_FILE}"

# The following are in addition to the declarations in /root/.bashrc. Note that
# this block does not do parameter expansion, so will be copied verbatim.
cat << 'EOF' >> "${RC_FILE}"
export PATH=/scripts/repo:$PATH
export GHCUP_INSTALL_BASE_PREFIX=/opt/ghcup
[ -r /opt/ghcup/.ghcup/env ] && source /opt/ghcup/.ghcup/env
cd /host
EOF

# Set an appropriate chown setting, based on if the group setup
# went OK
# Set an appropriate chown setting, based on if the group setup went OK
chown_setting="${UNAME}"
if [ "$GROUP_OK" = true ]; then
chown_setting="${UNAME}:${GROUP}"
Expand Down

0 comments on commit cb742b5

Please sign in to comment.