ci(missions-comparator): raise the stack limit before the judge (nanoda overflow on KWin certificates) - #625
Merged
Merged
Conversation
…da overflowed on KWin certs On #615 (run 36055910789, judge rvm_bridge 2/4) the bridge for MM_weil_positivity_prime_free_window built and exported, then nanoda died with "thread 'main' has overflowed its stack" (exit 134) replaying the KWin `decide +kernel` LDL^T certificate: nanoda's kernel is recursive and the main thread has an 8 MB stack that RUST_MIN_STACK does not size. `ulimit -s unlimited` (4 GB fallback, warning if neither is allowed) before invoking the comparator; lean4export and nanoda inherit it. Documented in the workflow and in AUDIT_INDEPENDENCE section 4. #619 (KWin2) and #622 carry larger certificates and would hit the same wall. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
This was referenced Sep 25, 2026
DrMurphyIsIn
pushed a commit
that referenced
this pull request
Sep 25, 2026
…-only) `MM_weil_positivity_prime_free_window` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The KWin window certificates need ~16-19 GB per decide, which exhausted the 16 GB runner and killed the whole shard after five nodes (run 36076883673); with the flag, the shard's single heavy node is judged by the Lean kernel alone and the other twelve keep both kernels. Merged main in for the machinery this depends on: #632 (the flag, the swap step for shards containing a heavy node, the dispatch filter, and `comparator-record --lean-kernel-only`) and #625 (`ulimit -s unlimited`). Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (53 challenges) and the node's config row now reads `lean-kernel-only`. `mission verify` is OK on all four campaigns. The record itself follows once the restricted shard dispatch passes, as `comparator-record --lean-kernel-only`, which stores `second_kernel = "none: heavy_certificates"` so provenance-report prints "Lean kernel only" rather than staying silent. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
DrMurphyIsIn
pushed a commit
that referenced
this pull request
Sep 25, 2026
…l-only) `MM_weil_positivity_window_two_fifths` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The L = 1/2 window certificates are the heaviest in the registry (~1100 s and ~16 GB per decide in the local rebuild), well past what a 16 GB runner survives with two kernels. Merged cl/kwin in, which carries main (#632's flag, swap step and dispatch filter, #625's `ulimit -s unlimited`) and the same flag on the prime-free-window node. The two heavy nodes land in different shards -- prime-free in rvm_bridge 2/4, two-fifths in 3/4 -- so each shard has at most one heavy node and gets the swap step only where it is needed. Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (54 challenges) and both heavy nodes' config rows read `lean-kernel-only`. `mission verify` is OK on all four campaigns. The records follow once the shards pass, as `comparator-record --lean-kernel-only`. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
On #615 (run 36055910789, shard
judge rvm_bridge 2/4) the bridge forMM_weil_positivity_prime_free_windowbuilt and exported, then nanoda died withthread 'main' has overflowed its stack(exit 134) while replaying the KWindecide +kernelLDL^T certificate. nanoda's kernel is recursive and the Rust main thread has an 8 MB stack thatRUST_MIN_STACKdoes not size.Fix (workflow only):
ulimit -s unlimited(fallbackulimit -s 4194304, and a::warning::if neither is allowed) in the judge step before invoking the comparator, so lean4export and nanoda inherit it. The limit in effect is printed. Documented in the workflow comment and inAUDIT_INDEPENDENCE_2026-09-23.mdsection 4. #619 (KWin2) and #622 carry larger certificates and would hit the same wall.After this lands, #615 merges main and reruns its shard; the same change is carried on
missions/judge-li-qc. No registry change.conjecture1_proved = False.🤖 Generated with Claude Code
https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU