ci(lean,#2874): plomberie build-jobs (LEAN_NUM_THREADS) — unité infra du split de PR 14821

.github/actions/lean-axiom/action.yml

@@ -29,6 +29,10 @@ inputs:
     description: 'Whether a transitive sorryAx fails the run. false = report has_sorry without gating (honesty knob, not leniency).'
     required: false
     default: 'true'
+  build-jobs:
+    description: 'Optional lake job-parallelism cap, applied as LEAN_NUM_THREADS. Empty = default (all cores). Lake 5.0.0 (Lean 4.32.1) has NO -j/--jobs CLI flag (`-J` is JSON output; jobs are BaseIO.asTask tasks on the Lean runtime pool, sized by LEAN_NUM_THREADS). `1` serialises elaboration when sibling modules peak together inside ONE job (knot_lean Conway/Conway_en, #14821).'
+    required: false
+    default: ''
 
 runs:
   using: composite
@@ -82,9 +86,17 @@ runs:
     - name: Lake build
       shell: bash
       working-directory: ${{ inputs.project-path }}
+      env:
+        # See the build-jobs input description: the cap goes through
+        # LEAN_NUM_THREADS (Lake 5.0 task pool), NOT a CLI flag — `lake -R
+        # build -j 1` dies with "unknown short option '-j'" (#14821 run
+        # 34037681207). Empty input = no export = default behavior, so
+        # callers that do not pass build-jobs are unaffected.
+        LAKE_BUILD_JOBS: ${{ inputs.build-jobs }}
       run: |
         set -o pipefail   # propagate lake's exit code through the pipeline (FAILED must
                           # exit != 0; See incident conway_lean HashlifeCorrectness L1058, 2026-06-14).
+        if [ -n "$LAKE_BUILD_JOBS" ]; then export LEAN_NUM_THREADS="$LAKE_BUILD_JOBS"; fi
         lake exe cache get || true
         # On failure, surface the error lines the `tail` window loses (See #8915).
         if lake -R build 2>&1 | tee "$RUNNER_TEMP/lake.log" | tail -10; then

.github/actions/lean-build/action.yml

@@ -19,6 +19,10 @@ inputs:
   sorry-filter-mode:
     description: 'How to count sorry: raw | prose-header | standalone-tactic | real'
     required: true
+  build-jobs:
+    description: 'Optional lake job-parallelism cap, applied as LEAN_NUM_THREADS. Empty = default (all cores). Lake 5.0.0 (Lean 4.32.1) has NO -j/--jobs CLI flag (`-J` is JSON output; jobs are BaseIO.asTask tasks on the Lean runtime pool, sized by LEAN_NUM_THREADS). `1` serialises elaboration when sibling modules peak together inside ONE job (knot_lean Conway/Conway_en, #14821).'
+    required: false
+    default: ''
 
 runs:
   using: composite
@@ -168,11 +172,19 @@ runs:
     - name: Lake build
       shell: bash
       working-directory: ${{ inputs.project-path }}
+      env:
+        # See the build-jobs input description: the cap goes through
+        # LEAN_NUM_THREADS (Lake 5.0 task pool), NOT a CLI flag — `lake -R
+        # build -j 1` dies with "unknown short option '-j'" (#14821 run
+        # 34037681207). Empty input = no export = default behavior, so
+        # callers that do not pass build-jobs are unaffected.
+        LAKE_BUILD_JOBS: ${{ inputs.build-jobs }}
       run: |
         set -o pipefail   # propagate lake's exit code through the pipeline — without this a
                           # FAILED lake build reports exit 0 (tail always succeeds), and the
                           # CI step passes regardless. See incident conway_lean HashlifeCorrectness
                           # L1058 (rfl fail masked as CI PASS, 2026-06-14).
+        if [ -n "$LAKE_BUILD_JOBS" ]; then export LEAN_NUM_THREADS="$LAKE_BUILD_JOBS"; fi
         lake exe cache get || true
         # `tail` keeps the SUCCESS path terse, but on FAILURE it also truncates the
         # `File.lean:L:C: error:` line — lake builds in parallel and pushes an early

.github/workflows/lean-knot.yml

@@ -140,6 +140,16 @@ jobs:
           display-name: knot_lean
           sorry-baseline: "10"
           sorry-filter-mode: real
+          # #14821 : le pool coursia-lean OOM-kill (exit 137) sur le pic
+          # d'elaboration des siblings Conway/Conway_en DANS le meme job —
+          # la contention entre jobs est REFUTEE (Proof integrity mort seul,
+          # 18 min apres liberation de l'autre job, DM ai-01 2026-09-06).
+          # Serialisation d'abord comme INSTRUMENT DE MESURE (reco ai-01,
+          # msg-20260906T133912-j6rlew) : si ca passe, c'est aussi le remede
+          # court terme ; si ca OOM, le pic d'un Conway seul depasse la boite.
+          # NB: Lake 5.0 n'a pas de -j (tentative 1 = run 34037681207, mort
+          # a l'option parsing) — le cap passe par LEAN_NUM_THREADS.
+          build-jobs: "1"
 
   # Level 3 proof-integrity gate (criterion B.3 of pr-review-discipline).
   # Closes #8677: catches forbidden axioms (incl. transitive `sorryAx`)
@@ -178,6 +188,10 @@ jobs:
           # The per-module enumeration now lives in the gate's runtime derivation
           # (issue #10889) -- flip to `true` when the baseline reaches 0.
           fail-on-sorry: false
+          # #14821 : meme instrument que le job ci (voir le commentaire du
+          # job ci) — ce job REBUILD le lake avec sa propre cle de cache,
+          # donc le pic des siblings se rejoue ici aussi.
+          build-jobs: "1"
 
   # Advisory proof-integrity coverage (See #8782). Same pattern as conway_lean
   # (#8787): the `target-modules` list above is hand-maintained while the