Update docker_build

Makes dev,  dev-base and dev-text targets have
better helptext and error detection.

Can now run
  docker_build.sh dev-base
  docker_build.sh litmus-tests --ssh-key path/to/key
  docker_build.sh dev_text -d path/to/rmem
Or as a shorthand:
  docker_build.sh dev -d path/to/rmem --ssh-key path/to/ssh/key

docker/docker_build.sh

@@ -2,20 +2,25 @@
 
 set -o errexit
 set -o nounset
-set -o xtrace
+#set -o xtrace
 shopt -s extglob
 
 readonly SCRIPTS_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 source "$SCRIPTS_DIR/common.sh"
 
 usage() {
-  echo "Usage: docker_build.sh base|text|dev-base|dev-text"
-  echo "       docker_build.sh litmus|regression|web|dev|all --ssh-key <file>"
+  echo "Usage: docker_build.sh base|text|dev-base"
+  echo "       docker_build.sh dev-text -d <path/to/rmem> [--force]"
+  echo "       docker_build.sh litmus|regression|web|all --ssh-key <file>"
+  echo "       docker_build.sh dev -d <path/to/rmem> --ssh-key <file>"
   echo
   echo "Options:"
   echo "  --ssh-key <file>   Use <file> to access the private litmus-test"
   echo "                     repositories on github"
+  echo "  -d <path>          Use <path> as the path to a local rmem installation"
+  echo "                     to be used in docker"
+  echo "  --force            Do not check <path/to/rmem> contains an installation of rmem"
 }
 
 if [[ "$#" -lt 1 ]] ; then
@@ -24,7 +29,7 @@ if [[ "$#" -lt 1 ]] ; then
 fi
 
 case "$1" in
-  litmus|regression|web|dev|all)
+  litmus|regression|web|all)
     readonly TARGET="$1"
     shift 1
     if [[ "$#" -lt 2 || "$1" != "--ssh-key" ]] ; then
@@ -34,7 +39,37 @@ case "$1" in
     readonly SSH_KEY="$2"
     shift 2
     ;;
-  base|text|dev-base|dev-text)
+  dev-text)
+    readonly TARGET="$1"
+    shift 1
+    if [[ "$#" -lt 2 || "$1" != "-d" ]]; then
+      usage
+      exit 1
+    fi
+    readonly RMEM_DIR="$2"
+    shift 2
+    if [[ "$#" -lt 1 || "$1" != "--force" ]]; then
+      readonly RMEM_FORCE=0
+    elif [[ "$#" -lt 1 ]]; then
+      usage
+      exit 1
+    else
+      readonly RMEM_FORCE=1
+    fi
+    ;;
+  dev)
+    readonly TARGET="$1"
+    shift 1
+    if [[ "$#" -lt 4 || "$1" != "-d" || "$3" != "--ssh-key" ]]; then
+      usage
+      exit 1
+    fi
+    readonly RMEM_FORCE=0
+    readonly RMEM_DIR="$2"
+    readonly SSH_KEY="$4"
+    shift 4
+    ;;
+  base|text|dev-base)
     readonly TARGET="$1"
     shift
     ;;
@@ -103,6 +138,16 @@ build_dev_base() {
 }
 
 build_dev_text() {
+  # heuristc to check that this dir is really rmem
+  # if not give the user an opt-in way to force it.
+  if [[ $RMEM_FORCE != 1 ]] && ! grep ${RMEM_DIR}/opam -q -e 'name: "rmem"' &>/dev/null ; then
+    echo "'${RMEM_DIR}' does not appear to be a directory containing rmem."
+    echo "Run  docker_build.sh dev-text -d '${RMEM_DIR}' --force  to force using this directory"
+    echo
+    usage
+    exit 1
+  fi
+
   docker build \
     --tag "$DOCKER_LOCAL_TEXT_IMAGE_NAME" \
     --build-arg GUEST_UID="$DOCKER_UID" \
@@ -111,7 +156,7 @@ build_dev_text() {
     --build-arg GUEST_GROUP="$DOCKER_GROUP" \
     --build-arg MODE=opt \
     --build-arg ISA=PPCGEN,AArch64,RISCV \
-    -f- . < "$SCRIPTS_DIR/Dockerfile.dev.text"
+    -f- ${RMEM_DIR} < "$SCRIPTS_DIR/Dockerfile.dev.text"
 }
 
 case "$TARGET" in