Add a script to build the Docker image

We need the user in the container and the user on the host to share
the same user id, in order to allow sharing a directory without any
access permissions problems.

Adding a script to enable each user to built her/his own container
and another to run an image from that container.

Dockerfile

 FROM ubuntu:18.04
 
-RUN useradd -m pintos && echo pintos:pintos | chpasswd && \
-	usermod -aG sudo pintos
+ARG HOST_USER_ID
+
+RUN useradd -m edaf35 -u $HOST_USER_ID && echo edaf35:edaf35 | chpasswd && \
+	usermod -aG sudo edaf35
 
 # General-purpose utilities
 RUN apt-get update && apt-get -y install \
@@ -17,12 +19,17 @@ RUN apt-get update && apt-get -y install \
         qemu
 
 # Switch user
-USER pintos
-WORKDIR /home/pintos
+USER edaf35
+
+WORKDIR /edaf35
+
+COPY ./chuid.sh /home/edaf35/chuid.sh
+
+RUN /bin/bash -c 'echo ". /home/edaf35/chuid.sh" >> /home/edaf35/.bashrc'
 
 # Clone pintos - needs adjustment to the right repo
-RUN git clone https://git.cs.lth.se/al7330du/pintos-public pintos
+# RUN git clone https://git.cs.lth.se/al7330du/pintos-public pintos
 
-RUN /bin/bash -c 'echo "pushd /home/pintos/pintos > /dev/null ; source setup.sh ; popd > /dev/null" >> /home/pintos/.bashrc'
+# RUN /bin/bash -c 'echo "pushd /home/pintos/pintos > /dev/null ; source setup.sh ; popd > /dev/null" >> /home/pintos/.bashrc'
 
-CMD /bin/bash
+# CMD /bin/bash

build.sh

+#! /bin/bash
+
+docker build --build-arg HOST_USER_ID=`id -u` -t edaf35:2021 .

chuid.sh

+#! /bin/bash
+
+EDAF35_USER_ID=`id -u`
+
+if [ $HOST_USER_ID != $EDAF35_USER_ID ] ; then
+    echo "*********************************** WARNING ***********************************************"
+    echo "* WARNING! Your user ID ($HOST_USER_ID) differs from the edaf35 user ID ($EDAF35_USER_ID). "
+    echo "* The directory /edaf35 is probably read-only.                                             "
+    echo "*******************************************************************************************"
+fi
+
+export PINTOS_HOME=/edaf35/pintos
+export PATH=$PATH:$PINTOS_HOME/src/utils

runme.sh

+#! /bin/bash
+
+THIS_SCRIPT=`realpath "$0"`
+EDAF35_DIR=`dirname $THIS_SCRIPT`
+
+docker run --env HOST_USER_ID=`id -u` -it --mount type=bind,source="$EDAF35_DIR",target=/edaf35 edaf35:2021