Skip to content

Commit 8859206

Browse files
fix(ci): soundness gate must not assume bare dune on PATH (greens main) (#635)
Greens `main`, which #633 left red. ## Root cause The soundness gate's property 5 ran `dune build test/xfail/test_xfail_pins.exe`. CI reaches dune only via `opam exec -- dune`, not bare `dune` on `PATH`, so this failed with *"ERROR (property 5): cannot build test/xfail/test_xfail_pins.exe"* — and the `build` job exited there (before `@fmt`). It greened locally because my dev box has `dune` at `/usr/bin/dune`; that environment difference is exactly what a local-only run can't catch. ## Fix The harness exe is already built by the `dune build` / `dune runtest` steps that run *before* the gate, so the gate now prefers the **pre-built binary** (`_build/default/...`) and only builds — with whatever dune is available (`dune`, else `opam exec -- dune`) — if it's missing. Fail-closed if it still isn't there. ## Verified (the actual CI condition, not just locally) Built the exe, then ran the gate with `dune`/`opam` removed from `PATH`: ``` dune on restricted PATH? NO OK: soundness ledger — all 5 properties hold (...) rc=0 ``` ## Note #633's `build` died at this gate, so `@fmt` never ran on its `lib/*.ml` edits (the `return`-fence). With the gate fixed, CI here will reach `@fmt`; if it flags those lib edits I'll follow up (I can't run `ocamlformat` in my environment, so I'd apply the diff from the CI log). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa --- _Generated by [Claude Code](https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 874e36c commit 8859206

1 file changed

Lines changed: 15 additions & 2 deletions

File tree

tools/check-soundness-ledger.sh

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -253,8 +253,21 @@ check_pins() {
253253
local pins; pins="$(pinned_row_pins)"
254254
[ -n "$pins" ] || { note "ERROR (property 5): no 'residual (pinned)'/'open (tracked)' rows found (fail closed)"; return 1; }
255255
printf '%s\n' "$pins" | grep -q '^NOPIN$' && { note "ERROR (property 5): a pinned/open row names no test_* pin (fail closed)"; return 1; }
256-
dune build "$XFAIL_EXE" >/dev/null 2>&1 || { note "ERROR (property 5): cannot build ${XFAIL_EXE}"; return 1; }
257-
local report; report="$(AFFINE_FIXTURES="$PWD/test/e2e/fixtures" "_build/default/${XFAIL_EXE}" 2>&1 || true)"
256+
# Run the pin harness. CI builds it in the `dune build` / `dune runtest` steps
257+
# before this gate, so prefer the pre-built binary and do NOT assume a bare
258+
# `dune` is on PATH (in CI dune is reached via `opam exec --`, not bare). Only
259+
# build if the exe is missing (e.g. a standalone local run), with whatever dune
260+
# is available. Fail closed if it still isn't there.
261+
local exe="_build/default/${XFAIL_EXE}"
262+
if [ ! -x "$exe" ]; then
263+
if command -v dune >/dev/null 2>&1; then
264+
dune build "$XFAIL_EXE" >/dev/null 2>&1 || true
265+
elif command -v opam >/dev/null 2>&1; then
266+
opam exec -- dune build "$XFAIL_EXE" >/dev/null 2>&1 || true
267+
fi
268+
fi
269+
[ -x "$exe" ] || { note "ERROR (property 5): pin harness ${exe} not built (run dune build first)"; return 1; }
270+
local report; report="$(AFFINE_FIXTURES="$PWD/test/e2e/fixtures" "$exe" 2>&1 || true)"
258271
local pin r=0
259272
while IFS= read -r pin; do
260273
[ -z "$pin" ] && continue

0 commit comments

Comments
 (0)