Merge pull request #264 from jscoq/v8.15+docker-multiarch

Docker multiarch

CHANGES.md

-# jsCoq 0.15.0 "Go For Your Toad, or Similar"
-------------------------------
+# jsCoq 0.15.1 "Go For Your Toad, or Similar"
+---------------------------------------
 
  - Update to Coq 8.15.1 (@corwin-of-amber)
+ - Stabilized jsCoq SDK Docker image (@corwin-of-amber)
 
 # jsCoq 0.15.0 "Steady State"
 ------------------------------

etc/docker/Dockerfile

 ARG BRANCH=v8.15
 
-FROM debian:10-slim as opam
+ARG WORDSIZE=32
+ARG SWITCH=jscoq+${WORDSIZE}bit
+
+FROM debian:11-slim as opam
 
 # ------------
 #   Get OPAM
 # ------------
-RUN dpkg --add-architecture i386 && apt-get update && apt-get upgrade -y apt && \
+
+ARG WORDSIZE
+
+RUN if [ ${WORDSIZE} = 32 ] ; then dpkg --add-architecture i386 ; fi
+
+RUN apt-get update && apt-get upgrade -y apt && \
     apt-get install --no-install-recommends -y \
     wget ca-certificates \
-    m4 bubblewrap gcc gcc-multilib libc6-dev libgmp-dev:i386 binutils make patch unzip
+    m4 bubblewrap gcc libc6-dev binutils make patch unzip \
+    opam
 
-# We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.8/opam-2.0.8-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN if [ ${WORDSIZE} = 32 ] ; then \
+    apt install --no-install-recommends -y gcc-multilib libgmp-dev:i386; fi
 
 # Basic OPAM setup
 ARG NJOBS=2
@@ -32,7 +41,10 @@ RUN opam init -a --bare --disable-sandboxing
 # -----------------
 FROM opam as jscoq-preinstall
 
-RUN opam switch create jscoq+32bit --packages="ocaml-variants.4.12.0+options,ocaml-option-32bit"
+ARG SWITCH
+ARG WORDSIZE
+RUN if [ ${WORDSIZE} != 32 ] ; then opam switch create ${SWITCH} 4.12.0 ; fi
+RUN if [ ${WORDSIZE} = 32 ] ;  then opam switch create ${SWITCH} --packages="ocaml-variants.4.12.0+options,ocaml-option-32bit" ; fi
 
 # Other deps: Git, Node.js, GMP
 ENV APT_PACKAGES="git rsync bzip2 nodejs curl libgmp-dev"
@@ -46,6 +58,7 @@ RUN apt install --no-install-recommends -y $APT_PACKAGES
 FROM jscoq-preinstall as jscoq-prereq
 
 ARG BRANCH
+ARG WORDSIZE
 ARG JSCOQ_REPO=https://github.com/jscoq/jscoq
 ARG JSCOQ_BRANCH=${BRANCH}
 
@@ -53,7 +66,7 @@ WORKDIR /root
 RUN git clone --recursive -b ${JSCOQ_BRANCH} ${JSCOQ_REPO}
 
 WORKDIR jscoq
-RUN ./etc/toolchain-setup.sh --32
+RUN ./etc/toolchain-setup.sh --${WORDSIZE}
 RUN opam clean -a -c
 RUN opam list
 
@@ -64,7 +77,7 @@ FROM jscoq-prereq as jscoq
 
 ARG NJOBS=4
 
-RUN git pull
+RUN git pull --ff-only
 RUN eval $(opam env) && make coq && make jscoq
 
 # - dist tarballs
@@ -81,6 +94,8 @@ RUN eval $(opam env) && make install &&   \
     cd _build/jscoq+* && npm link
 
 ARG BRANCH
+ARG WORDSIZE
+ARG SWITCH
 ARG ADDONS_REPO=https://github.com/jscoq/addons
 ARG ADDONS_BRANCH=${BRANCH}
 
@@ -93,7 +108,7 @@ RUN git clone --recursive -b ${ADDONS_BRANCH} ${ADDONS_REPO} jscoq-addons
 
 WORKDIR jscoq-addons
 RUN make set-ver VER=`jscoq --version`
-RUN eval $(opam env) && make
+RUN eval $(opam env) && make CONTEXT=${SWITCH}
 
 # Private repos: re-enable SSH
 COPY Dockerfile _ssh* /root/_ssh/
@@ -103,7 +118,7 @@ ENV GIT_SSH_COMMAND 'ssh -i /root/_ssh/id_rsa -o StrictHostKeyChecking=no'
 RUN if [ -e /root/_ssh/id_rsa ] ; then rm ~/.gitconfig && apt-get install -y openssh-client ; fi
 RUN if [ -e /root/_ssh/id_rsa ] ; then eval $(opam env) && make privates WITH_PRIVATE=software-foundations ; fi
 
-RUN make pack
+RUN make pack CONTEXT=${SWITCH}
 
 # ---------
 # jsCoq SDK
@@ -118,13 +133,25 @@ RUN cp -rL _build/install/jscoq+*bit/ ./dist-sdk && \
 # rm dist-sdk/lib/coq/*/*.cmxs \
 # `find dist-sdk -regex '.*\.\(cm\(a\|t\|ti\)\|mli?\)'`
 
-FROM debian:10-slim as jscoq-sdk
+FROM debian:11-slim as jscoq-sdk
+
+ARG WORDSIZE
 
 COPY --from=jscoq-sdk-prepare /root/jscoq/dist-sdk /opt/jscoq
 
-COPY sdk-startup.sh /root/sdk-startup.sh
+COPY gosu-entrypoint.sh /root/gosu-entrypoint.sh
+ENTRYPOINT ["/root/gosu-entrypoint.sh"]
+
+# Needs to be squashed into a single step to facilitate cleanup
+RUN if [ ${WORDSIZE} = 32 ] ; then \
+        dpkg --add-architecture i386 && apt-get update && \
+        apt-get install --no-install-recommends -y \
+            libgmp10:i386 libc6-i386 ; \
+    else apt-get update ; \
+    fi ; \
+    apt-get install --no-install-recommends -y gosu && \
+    apt-get clean && rm -rf /var/lib/apt/lists/*
 
-ENTRYPOINT ["/root/sdk-startup.sh"]
 ENV PATH /usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/jscoq/bin
 
 # ----------------------------------------------------------
@@ -180,7 +207,7 @@ ARG JSCOQ_BRANCH=${BRANCH}
 
 ARG NJOBS=4
 
-RUN git pull
+RUN git pull --ff-only
 RUN npm install
 RUN eval $(opam env) && make coq && make
 RUN make dist-npm

etc/docker/Makefile

@@ -12,13 +12,20 @@ export WACOQ_BIN_BRANCH = $(BRANCH)
 
 export NJOBS ?= 4
 
+ifneq (${shell uname -m},x86_64)
+# 32-bit support is only available for x86 processors (esp., not arm64)
+export WORDSIZE = 64
+endif
+
 # Use BuildKit.
 # This is needed for jscoq/wacoq branching in Dockerfile
 export DOCKER_BUILDKIT = 1
 
-ARGS = --build-arg BRANCH --build-arg NJOBS \
-	   --build-arg JSCOQ_REPO --build-arg JSCOQ_BRANCH \
-	   --build-arg WACOQ_BIN_REPO --build-arg WACOQ_BIN_BRANCH
+BUILD_ARGS = BRANCH NJOBS WORDSIZE \
+             JSCOQ_REPO JSCOQ_BRANCH WACOQ_BIN_REPO WACOQ_BIN_BRANCH
+
+ARGS = $(addprefix --platform , $(firstword ${ARCH})) \
+       $(addprefix --build-arg , $(BUILD_ARGS))
 
 -include _config.mk
 

etc/docker/gosu-entrypoint.sh

+#!/bin/bash
+
+# https://gist.github.com/alexpearce/b438bc9f358ba7b333f2e15e6bd826f0
+
+# Run commands in the Docker container with a particular UID and GID.
+# The idea is to run the container like
+#   docker run -i \
+#     -v `pwd`:/work \
+#     -e LOCAL_USER_ID=`id -u $USER` \
+#     -e LOCAL_GROUP_ID=`id -g $USER` \
+#     image-name bash
+# where the -e flags pass the env vars to the container, which are read by this script.
+# By setting copying this script to the container and setting it to the
+# ENTRYPOINT, and subsequent commands run in the container will run as the user
+# who ran `docker` on the host, and so any output files will have the correct
+# permissions.
+
+USER_ID=${LOCAL_USER_ID:-9001}
+GROUP_ID=${LOCAL_GROUP_ID:-$USER_ID}
+
+if [ x"$LOCAL_USER_ID" != x ] ; then
+  echo "Starting with UID : $USER_ID, GID: $GROUP_ID"
+fi
+groupadd -g $GROUP_ID thegroup
+useradd --shell /bin/bash -u $USER_ID -g thegroup -o -c "" -m user
+export HOME=/home/user
+
+exec /usr/sbin/gosu user:thegroup "${@:-bash}"
\ No newline at end of file

examples/sdk-demo/bin/coqc

 #!/usr/bin/env node
 
-const child_process = require('child_process');
+const os = require('os'),
+      child_process = require('child_process');
 
 const ME = 'jscoq',
       DOCKER_IMAGE = `${ME}:sdk`;
@@ -16,9 +17,17 @@ function mounts() {
     return (mnt ? [mnt] : []).map(d => `-v${d}:${d}`);
 }
 
+function user() {
+    if (os.platform() === 'darwin') return [];  // seems to not work in macOS, and also unneeded
+    else {
+        var {uid, gid} = os.userInfo();
+        return ['-e', `LOCAL_USER_ID=${uid}`, '-e', `LOCAL_GROUP_ID=${gid}`];
+    }
+}
+
 function run(args) {
     var cmd = 'docker', args = [
-        'run', ...mounts(), `-w${process.cwd()}`, '--rm',
+            'run', ...mounts(), ...user(), `-w${process.cwd()}`, '--rm',
             DOCKER_IMAGE, 'coqc', ...args
         ];
     var rc = child_process.spawnSync(cmd, args, {stdio: 'inherit'});