diff --git a/.github/workflows/missions-comparator.yml b/.github/workflows/missions-comparator.yml index 6a305e2ba..1e9687c05 100644 --- a/.github/workflows/missions-comparator.yml +++ b/.github/workflows/missions-comparator.yml @@ -206,6 +206,14 @@ jobs: run: | set -uo pipefail echo "lean4export = $COMPARATOR_LEAN4EXPORT ; nanoda = $COMPARATOR_NANODA" + # Stack (2026-09-24, #615 run 36055910789): nanoda's kernel is recursive and the KWin + # artifacts carry large `decide +kernel` LDL^T certificates; replaying them overflowed + # the 8 MB MAIN-thread stack ("thread 'main' has overflowed its stack", exit 134). + # RUST_MIN_STACK only sizes spawned threads, so raise the process limit here; the + # comparator's children (lean4export, nanoda) inherit it. Fall back to 4 GB if the + # runner's hard limit refuses unlimited; never let the fallback itself fail the job. + ulimit -s unlimited 2>/dev/null || ulimit -s 4194304 2>/dev/null || echo "::warning::could not raise the stack limit (ulimit -s); large certificates may overflow nanoda" + echo "stack limit (KB): $(ulimit -s)" fail=0; pass=0 { echo "## missions-comparator: ${{ matrix.island }} shard ${{ matrix.shard }} (run ${{ github.run_id }})" diff --git a/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md b/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md index 747f45846..94cf43db0 100644 --- a/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md +++ b/telperion/docs/AUDIT_INDEPENDENCE_2026-09-23.md @@ -90,7 +90,11 @@ on a GitHub-hosted runner from a clean checkout. It is **not** independent of th vocabulary: the registered statement is elaborated in the artifact's own namespace and `open` context on the island, not against the campaign's vocabulary mirror (`Statements.RHDefs`, `MMDefs`), because the Comparator needs both sides in one Lake -workspace. Whether the mirror still matches the island is `missions/mirrors.py` and the +workspace. The judge step raises the process stack limit (`ulimit -s unlimited`, 4 GB +fallback) before invoking the Comparator: nanoda replays proofs recursively and the large +`decide +kernel` certificates of the KWin artifacts overflowed the 8 MB main-thread stack +(#615, run 36055910789); a stack overflow is a runner limit, not a verdict, and the job +says so. Whether the mirror still matches the island is `missions/mirrors.py` and the islands' `generate.py --check` jobs. Whether the island's `DBN.H` is the de Bruijn-Newman `H` is the read-back's job. The judge closes the gap between the two: given the vocabulary, the artifact proves this proposition and nothing weaker.