From 2dcabb17ef7490e51425b2b2448e4cc7d4d2177e Mon Sep 17 00:00:00 2001 From: bryan Date: Sun, 26 Jul 2026 12:07:46 -0700 Subject: [PATCH 1/2] zola, tamarin-prover: fix reproducibility MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both were flagged `unknown` by a build-twice audit of the 87 packages added since the last fleet run. They turned out to be completely different problems. zola — the reproducibility guide was applied halfway. The recipe already cites minimal-repro's guide and strips build paths, but never pinned codegen. rustc's default release build shards codegen across parallel units that finish in thread-completion order, so functions are EMITTED in a different order each build. Measured on 0.22.1: 16.89% of bytes differed while the total size stayed identical, and 69% of differing windows had a byte-exact twin elsewhere in the other build — a size-preserving permutation, i.e. ordering, not codegen variance. Adds `-C codegen-units=1` (ordering) and `-C symbol-mangling-version=v0` (legacy mangling embeds a per-session hash). Same fix as nushell and difftastic. tamarin-prover — not GHC, and not the toolchain. Its version banner embeds the wall-clock compile time via a TemplateHaskell splice that calls getCurrentTime while compiling; it asks the clock directly, so SOURCE_DATE_EPOCH never reaches it. Exactly 26 bytes of a 135 MB binary differ, and the Haskell codegen is otherwise bit-identical — the GHC determinism work is holding fine. Rewrites the splice to a fixed instant derived from SOURCE_DATE_EPOCH, locating the source file by content so an upstream file move fails loudly instead of silently reverting to a wall clock. Co-Authored-By: Claude Opus 4.8 --- packages/tamarin-prover/build.sh | 30 ++++++++++++++++++++++++++++++ packages/zola/build.sh | 17 ++++++++++++++--- 2 files changed, 44 insertions(+), 3 deletions(-) diff --git a/packages/tamarin-prover/build.sh b/packages/tamarin-prover/build.sh index a484a1ba..8ed2df0f 100755 --- a/packages/tamarin-prover/build.sh +++ b/packages/tamarin-prover/build.sh @@ -67,6 +67,36 @@ grep -v '^with-compiler:' stackage-lts-24.50.cabal.config > lts-pinned.config # so the field is reachable via the type. (pkgmgr-rs#528) sed -i 's/defaultTheoryLoadOptions, maudePath, TheoryLoadError/defaultTheoryLoadOptions, TheoryLoadOptions(maudePath), TheoryLoadError/' src/Main/REPL.hs +# Reproducibility: tamarin's version banner embeds the WALL-CLOCK compile time +# +# Git revision: UNKNOWN, branch: UNKNOWN +# Compiled at: 2026-07-25 03:47:54.541898723 UTC +# +# via a TemplateHaskell splice that calls getCurrentTime while COMPILING. It +# asks the clock directly, so the sandbox's SOURCE_DATE_EPOCH never reaches it, +# and two builds differ by exactly that string — measured: 26 bytes out of +# 135 MB, with the Haskell codegen itself bit-identical. (The git fields are +# already deterministic: no repo here, so both builds say UNKNOWN.) +# +# Rewrite the splice to a fixed instant derived from SOURCE_DATE_EPOCH. Located +# by content rather than by path so an upstream file move fails loudly here +# instead of silently reverting to a wall clock. +STAMP="$(date -u -d "@${SOURCE_DATE_EPOCH:-0}" '+%Y-%m-%d %H:%M:%S UTC' 2>/dev/null \ + || date -u -r "${SOURCE_DATE_EPOCH:-0}" '+%Y-%m-%d %H:%M:%S UTC')" +stamp_file="$(grep -rl 'Compiled at' --include='*.hs' src lib 2>/dev/null | head -1)" +if [ -z "$stamp_file" ]; then + echo "ERROR: no source file embeds 'Compiled at' — tamarin's version banner moved; revisit this patch." >&2 + exit 1 +fi +# Replace the runIO getCurrentTime splice with the pinned literal. +sed -i "s|runIO Data\.Time\.getCurrentTime|pure (\"$STAMP\")|g; \ + s|runIO getCurrentTime|pure (\"$STAMP\")|g" "$stamp_file" +if grep -q 'getCurrentTime' "$stamp_file"; then + echo "ERROR: tamarin compile-time-clock patch did not apply in $stamp_file (splice shape changed)." >&2 + grep -n 'getCurrentTime' "$stamp_file" >&2 + exit 1 +fi + # Build + install the executable (STATIC — a normal Haskell static link; the link # was never the problem). The sandbox hides build detail, so on failure dump the # real error (compile OR link) rather than a silent "Failed to build". diff --git a/packages/zola/build.sh b/packages/zola/build.sh index c20b192c..9453acf1 100755 --- a/packages/zola/build.sh +++ b/packages/zola/build.sh @@ -3,9 +3,20 @@ set -eu export CC=gcc export LD=gcc -# Reproducibility (per minimal-repro's guide): strip absolute build -# paths (source dir + cargo registry) and disable incremental builds. -export RUSTFLAGS="-C linker=gcc --remap-path-prefix=$(pwd)=/builddir --remap-path-prefix=$HOME/.cargo=/cargo" +# Reproducibility (per minimal-repro's guide): strip absolute build paths +# (source dir + cargo registry), disable incremental builds, and pin codegen. +# +# codegen-units=1 is the load-bearing one here. rustc's default release build +# shards codegen across parallel units, and the units finish in whatever order +# the thread pool happens to produce, so functions are EMITTED in a different +# order each build. The result is a binary of identical size whose contents are +# a permutation of themselves — measured on 0.22.1: 16.89% of bytes differed +# with the total size unchanged, and 69% of the differing windows had a +# byte-exact twin elsewhere in the other build. Not codegen variance; ordering. +# +# symbol-mangling-version=v0 removes the other half: the legacy mangling scheme +# embeds a compilation-session hash in symbol names, which varies run to run. +export RUSTFLAGS="-C linker=gcc --remap-path-prefix=$(pwd)=/builddir --remap-path-prefix=$HOME/.cargo=/cargo -C codegen-units=1 -C symbol-mangling-version=v0" export CARGO_INCREMENTAL=0 cargo build --release mkdir -p "$OUTPUT_DIR/usr/bin" From 7d7556ade83a261ae8dabde88f3547940e002bfe Mon Sep 17 00:00:00 2001 From: bryan Date: Sun, 26 Jul 2026 12:31:40 -0700 Subject: [PATCH 2/2] tamarin-prover: match the composed compile-time-clock splice The reproducibility patch only matched a BARE call: s|runIO Data\.Time\.getCurrentTime|...| s|runIO getCurrentTime|...| but upstream composes the action rather than naming it: $(stringE =<< runIO (show `fmap` Data.Time.getCurrentTime)) `runIO` is followed by `(show ` fmap ` ...`, so neither pattern matched, getCurrentTime survived, and the guard correctly refused the build on both arches rather than shipping a wall-clock binary: ERROR: tamarin compile-time-clock patch did not apply in src/Main/Console.hs Add a pattern for the whole parenthesised argument; keep the two bare forms in case upstream simplifies back to them. Verified by running the patched block verbatim against the real line: compileTime = "Compiled at: " ++ $(stringE =<< pure ("1970-01-01 00:00:00 UTC")) which type-checks (`pure :: String -> Q String` feeding `stringE`) and leaves no getCurrentTime for the guard to catch. Co-Authored-By: Claude Opus 5 (1M context) --- packages/tamarin-prover/build.sh | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/packages/tamarin-prover/build.sh b/packages/tamarin-prover/build.sh index 8ed2df0f..4ba93a89 100755 --- a/packages/tamarin-prover/build.sh +++ b/packages/tamarin-prover/build.sh @@ -88,8 +88,13 @@ if [ -z "$stamp_file" ]; then echo "ERROR: no source file embeds 'Compiled at' — tamarin's version banner moved; revisit this patch." >&2 exit 1 fi -# Replace the runIO getCurrentTime splice with the pinned literal. -sed -i "s|runIO Data\.Time\.getCurrentTime|pure (\"$STAMP\")|g; \ +# Replace the compile-time-clock splice with the pinned literal. Upstream +# COMPOSES the action rather than naming it bare: +# $(stringE =<< runIO (show `fmap` Data.Time.getCurrentTime)) +# so the first pattern matches the whole parenthesised argument. The two bare +# forms are kept in case upstream simplifies back to them. +sed -i "s|runIO ([^)]*getCurrentTime[^)]*)|pure (\"$STAMP\")|g; \ + s|runIO Data\.Time\.getCurrentTime|pure (\"$STAMP\")|g; \ s|runIO getCurrentTime|pure (\"$STAMP\")|g" "$stamp_file" if grep -q 'getCurrentTime' "$stamp_file"; then echo "ERROR: tamarin compile-time-clock patch did not apply in $stamp_file (splice shape changed)." >&2