Diff
patch 70c4f5cd26f8af3818354ea83e7bb742cb99ac82
Author: fritjof@alokat.org
Date: Wed Apr 15 13:50:11 UTC 2026
* Speed up Docker rebuilds on Pi 5 with BuildKit cache mounts.
hunk ./.dockerignore 4
-*.vo
-*.vok
-*.vos
-*.glob
-.*.aux
+**/dist-newstyle/
+**/*.vo
+**/*.vok
+**/*.vos
+**/*.glob
+**/.*.aux
hunk ./Dockerfile 1
+# syntax=docker/dockerfile:1.7
hunk ./Dockerfile 8
+#
+# BuildKit cache mounts are used below so that apt packages, the opam
+# switch (OCaml + Rocq), the stack resolver, and .stack-work survive
+# between builds. BuildKit is the default builder since Docker 23; older
+# hosts need `DOCKER_BUILDKIT=1 docker build ...`.
hunk ./Dockerfile 16
-# Install Rocq (needed for verified extraction) and build tools
-RUN apt-get update && \
+# TARGETARCH is populated by BuildKit from the target platform and is used
+# below to namespace cache mounts so arm64 and amd64 builds do not share
+# arch-specific binaries (notably the opam switch, which is native code).
+ARG TARGETARCH
+
+# Build parallelism. Defaults to 2 because the Raspberry Pi 5 hangs under
+# -j4 (GHC linking and the opam Rocq build exhaust RAM on a 4 GB Pi).
+# Raise it on bigger hosts via `--build-arg JOBS=$(nproc)`.
+ARG JOBS=2
+
+# Install Rocq build dependencies. /var/cache/apt and /var/lib/apt are
+# cache-mounted so repeated builds do not redownload .deb files; the
+# default docker-clean hook is removed so apt keeps its cache.
+RUN --mount=type=cache,id=darcsweb-apt-cache-${TARGETARCH},target=/var/cache/apt,sharing=locked \
+ --mount=type=cache,id=darcsweb-apt-lib-${TARGETARCH},target=/var/lib/apt,sharing=locked \
+ rm -f /etc/apt/apt.conf.d/docker-clean && \
+ apt-get update && \
hunk ./Dockerfile 35
- libgmp-dev linux-libc-dev pkg-config && \
- rm -rf /var/lib/apt/lists/*
-
-# Pin OCaml compiler and Rocq versions for reproducible builds
-RUN opam init --disable-sandboxing --bare -y && \
- opam switch create default ocaml-base-compiler.4.14.2 && \
- eval $(opam env --switch=default) && \
+ libgmp-dev linux-libc-dev pkg-config
+
+# Pin OCaml + Rocq. /root/.opam is cache-mounted, so the multi-minute
+# OCaml and Rocq compilation runs once, not on every rebuild. The mount
+# must be re-declared on every subsequent RUN that invokes `rocq` (the
+# stack build triggers extraction through Setup.hs). A stale cache can
+# leave the switch half-built; verify the compiler runs with the pinned
+# version and rebuild from scratch on mismatch.
+RUN --mount=type=cache,id=darcsweb-opam-${TARGETARCH},target=/root/.opam,sharing=locked \
+ if [ ! -f /root/.opam/config ]; then \
+ opam init --disable-sandboxing --bare -y; \
+ fi && \
+ if ! opam exec --switch=default -- ocaml -version 2>/dev/null | grep -q '4\.14\.2'; then \
+ opam switch remove default -y 2>/dev/null || true; \
+ opam switch create default ocaml-base-compiler.4.14.2 -j"${JOBS}"; \
+ fi && \
+ eval "$(opam env --switch=default)" && \
hunk ./Dockerfile 54
- opam install rocq-core.9.0.0 rocq-stdlib.9.0.0 -y
+ opam install rocq-core.9.0.0 rocq-stdlib.9.0.0 -y -j"${JOBS}"
+
+# Make rocq available to later RUN steps that mount /root/.opam.
+ENV PATH=/root/.opam/default/bin:$PATH
hunk ./Dockerfile 61
-# Copy dependency manifests first to cache the resolver/GHC download
+# Copy dependency manifests first so the snapshot/GHC layer is cached
+# independent of source changes.
hunk ./Dockerfile 64
-RUN eval $(opam env --switch=default) && \
+
+# Stack's resolver, GHC tarball, and global package DB live in ~/.stack;
+# cache-mount it so `stack setup` is a no-op on the second build.
+RUN --mount=type=cache,id=darcsweb-stack-${TARGETARCH},target=/root/.stack,sharing=locked \
hunk ./Dockerfile 70
-# Copy sources and build
+# Copy sources and build. .stack-work is cache-mounted so Haskell
+# modules are only recompiled when their sources actually change.
hunk ./Dockerfile 78
-RUN eval $(opam env --switch=default) && \
- stack build --install-ghc --no-terminal --copy-bins --local-bin-path /usr/local/bin
+RUN --mount=type=cache,id=darcsweb-opam-${TARGETARCH},target=/root/.opam,sharing=locked \
+ --mount=type=cache,id=darcsweb-stack-${TARGETARCH},target=/root/.stack,sharing=locked \
+ --mount=type=cache,id=darcsweb-stackwork-${TARGETARCH},target=/src/.stack-work,sharing=locked \
+ stack build --no-terminal --copy-bins \
+ --local-bin-path /usr/local/bin \
+ -j"${JOBS}"
hunk ./Dockerfile 88
-RUN apt-get update && \
+ARG TARGETARCH
+
+RUN --mount=type=cache,id=darcsweb-apt-cache-runtime-${TARGETARCH},target=/var/cache/apt,sharing=locked \
+ --mount=type=cache,id=darcsweb-apt-lib-runtime-${TARGETARCH},target=/var/lib/apt,sharing=locked \
+ rm -f /etc/apt/apt.conf.d/docker-clean && \
+ apt-get update && \
hunk ./Dockerfile 95
- rm -rf /var/lib/apt/lists/* && \
hunk ./README.md 171
+The Dockerfile uses BuildKit cache mounts for apt, the opam switch
+(OCaml + Rocq), and the stack artifacts, so the expensive first build is
+reused on subsequent rebuilds. BuildKit is the default builder in Docker
+23+; on older hosts prefix the command with `DOCKER_BUILDKIT=1`.
+
+Build parallelism defaults to `JOBS=2`, which is what a 4 GB Raspberry
+Pi 5 can sustain without hanging during GHC linking or the Rocq compile.
+On a host with more RAM and cores, raise it:
+
+```
+docker build --build-arg JOBS=$(nproc) -t darcsweb .
+```
+
