Skip to content
Snippets Groups Projects
Commit af6d3928 authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[port] Support both 32- and 64-bit builds.

Use gosu to allow running commands with local user permissions
in bind directories (for sdk).
parent efdf67ec
Branches
No related tags found
No related merge requests found
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,21 @@ 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"]
ENTRYPOINT ["/root/sdk-startup.sh"]
RUN if [ ${WORDSIZE} = 32 ] ; then \
dpkg --add-architecture i386 && apt-get update && \
apt-get install --no-install-recommends -y \
libgmp10:i386 libc6-i386 ; \
fi
RUN apt-get install gosu && apt-get clean
ENV PATH /usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/jscoq/bin
# ----------------------------------------------------------
......@@ -180,7 +203,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
......
......@@ -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
......
#!/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}
echo "Starting with UID : $USER_ID, GID: $GROUP_ID"
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
#!/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,14 @@ function mounts() {
return (mnt ? [mnt] : []).map(d => `-v${d}:${d}`);
}
function user() {
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'});
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment