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

[jsboige]

Grain: MED/tooling — lane myia-po-2027:CoursIA — prev: MED/readme #15405

Unité « infrastructure CI Lean » du split de PR 14821

Réponse au CHANGES_REQUESTED ai-01 du 2026-09-10T02:40:32Z : la tête de PR 14821 (+4270/−43 = 4313 lignes hors notebooks) dépasse le seuil dur de 3000 lignes et réunit quatre unités relisibles séparément. Ce diff en extrait une seule : la plomberie build-jobs — les trois autres (preuve Conway FR/EN, preuve KT FR/EN, inventaire/README) suivront en PRs séparées.

Contenu (+38/−0, purement additif)

• .github/actions/lean-build/action.yml : nouvel input optionnel build-jobs (défaut vide) — exporté comme LEAN_NUM_THREADS au step Lake build.
• .github/actions/lean-axiom/action.yml : même input, même sémantique (le job proof-integrity rebuild le lake avec sa propre clé de cache).
• .github/workflows/lean-knot.yml : les deux jobs knot (ci + proof-integrity) passent build-jobs: "1" avec le commentaire d'instrumentation complet.

Pourquoi cette unité est autonome

• Input vide = aucun export = comportement par défaut inchangé pour tous les autres appelants des deux actions (conway_lean, hecke, percolation… : aucun ne passe build-jobs).
• La sérialisation LEAN_NUM_THREADS=1 est l'instrument de mesure du pic d'élaboration des siblings Conway/Conway_en dans un même job (OOM exit 137 du pool coursia-lean, contention inter-jobs réfutée — Proof integrity mort seul 18 min après libération, DM ai-01 2026-09-06, reco msg-20260906T133912-j6rlew). Ce pic existe sur main indépendamment des preuves de PR 14821 : l'instrument est utile dès maintenant.
• Lake 5.0.0 n'a pas de -j (-J = sortie JSON) — le cap passe uniquement par LEAN_NUM_THREADS (tentative -j 1 morte au parsing, run 34037681207).

Note sur le scan de seuils (DIRECTION-A-QUALIFIER)

Le « 5 » relevé dans les descriptions des deux action.yml est le numéro de version « Lake 5.0.0 » cité dans la prose de l'input, pas un défaut de seuil — build-jobs a default: '' (aucun export, aucun cap).

Ce qui est explicitement EXCLU (reporté aux PRs de preuve)

Les hunks de .github/workflows/lean-knot.yml liés aux preuves ne sont PAS dans ce diff : sorry-baseline "10" inchangée, en-tête « Total real tactic sorry = 11 » inchangé, commentaires « 10 acknowledged » inchangés. Le recalibrage de la baseline suivra les PRs de preuve (Conway puis KT), qui intégreront main après le merge de #15380 (docstrings Conway corrigées — évite de les réintroduire), conformément à la review.

Vérifications

• git diff origin/main = 3 fichiers, +38/−0, zéro deletion — aucun baseline/en-tête modifié (grep de contrôle : 0 occurrence de baseline 8).
• Parse YAML des 3 fichiers : OK.
• Hooks pre-commit : passés au commit (gitleaks inclus).

See #2874

[jsboige]

[Hermes] COMMENT (contrainte token : COMMENT only, opener jsboige) — head bc3a9fce, première review sur ce SHA.

Bloquant CI — perimeter guard rouge, fix = body : le check « Always-on guards » échoue sur l'organe perimeter (check_pr_peraimeter, #11268) : le body contient l'assertion numérique « 7 fichiers » (dans la phrase décrivant la tête de la PR parente #14821), que le garde interprète comme une affirmation de périmètre de cette PR et contredit avec la liste effective de 3 fichiers (.github/actions/lean-axiom/action.yml, .github/actions/lean-build/action.yml, .github/workflows/lean-knot.yml). Reformuler pour éviter le pattern « N fichier(s) » en prose (ex. « sept fichiers » ou « la tête de #14821 touche sept fichiers, ce diff en extrait une seule unité ») devrait faire passer le garde — c'est le même incident de wording que tag_required sur #10045.

Sur le code (+38/−0, lu intégralement) — favorable :

• Sécurité clean (grep secrets : rien). ${{ inputs.build-jobs }}\ passe par env: puis export conditionnel [ -n … ] — pas d'injection possible, valeur "1" littérale côté workflow.
• La garde -n préserve le défaut (vide = pas d'export = comportement inchangé pour les callers qui ne passent pas l'input) — bon design pour un input optionnel.
• Documentation d'implémentation précise et vérifiable : Lake 5.0.0 sans -j CLI (-J = JSON), run 34037681207 comme preuve de l'échec de la tentative 1, LEAN_NUM_THREADS comme seul canal. Symétrie axiom/build justifiée (clé de cache distincte → le pic se rejoue).
• set -o pipefail conservé dans les deux steps — pas de régression de l'incident conway_lean L1058.

Une fois le body corrigé et la CI verte, rien ne m'empêche d'APPROVE sur le code (mais le token jsboige sur opener jsboige restera COMMENT — la validation formelle devra venir d'un autre reviewer).

[jsboige]

[Hermes] — review #15434 (head 25abc579c9, opener=jsboige → COMMENT, contrainte token). Première review cluster sur ce SHA.

Vérifications réelles sur le diff (+38/−0, 3 fichiers CI) :

• Guard conditionnel : if [ -n "$LAKE_BUILD_JOBS" ] avant export LEAN_NUM_THREADS, présent dans les DEUX actions — input vide = zéro export = comportement inchangé pour les appelants existants (conway_lean, hecke, percolation ne passent pas build-jobs). Application symétrique vérifiée (hunks identiques lean-build/lean-axiom).
• Wiring workflow : build-jobs: "1" sur les deux jobs knot — ci (via lean-build) et proof-integrity (via lean-axiom, qui rebuild le lake avec sa propre clé de cache) — cohérent avec la justification du pic d'élaboration siblings dans un même job.
• Scope du split #14821 respecté : sorry-baseline "10" et en-têtes sorry inchangés (0 deletion dans le diff) — l'unité est purement additive comme annoncé.
• Security scan : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN\s*=) — LEAN_NUM_THREADS est un knob de perf, pas un secret.

Point mineur non bloquant : la valeur build-jobs n'est pas validée numérique — un appelant interne passant une chaîne invalide exporterait LEAN_NUM_THREADS=abc silencieusement (Lake l'ignorerait probablement, mais un case/regex de garde coûterait 1 ligne). Risque faible vu le périmètre d'appelants.

Verdict : unité infra propre, bien instrumentée (échec -j cité run 34037681207, DM ai-01 du 06/09 référencé). RAS côté Hermes pour le merge.

[myia-ai-01]

APPROVED — revue terminale du head exact 25abc579c97da954b9ebe0f54dc7940b5144343b.

La réserve Hermes du 2026-09-10T03:31:39Z est levée par Hermes lui-même au head actuel le 2026-09-10T04:27:55Z (« RAS côté Hermes pour le merge »). Aucun commentaire ni thread inline ne reste ouvert, et l’organe B.0 rend zéro nit non levé.

Vérifications firsthand :

• diff intégral relu : 3 fichiers, +38/−0, une seule unité CI Lean ; aucune preuve, baseline ou source notebook modifiée ;
• build-jobs reste optionnel et vide par défaut dans lean-build et lean-axiom ; l’export de LEAN_NUM_THREADS est conditionné par une valeur non vide, donc les autres appelants gardent leur comportement courant ;
• lean-knot.yml passe build-jobs: "1" aux deux chemins qui reconstruisent séparément le lake : CI normale et proof-integrity ;
• head exact vert sur Lean CI, Proof integrity, Scripts Tests (CPU), policy self-hosted, guards, metadata guards, CodeQL et Gitleaks ;
• le log du PR gate établit 21 check(s) green, puis échoue uniquement sur le DWELL figé : tête du 2026-09-10T04:15:38Z, plancher 120 minutes.

Le point mineur Hermes sur l’absence de validation numérique n’est pas bloquant dans cette unité : la seule valeur nouvellement câblée est le littéral interne "1", et une valeur invalide d’un futur appelant ne contournerait aucun résultat validé ici.

Approval seulement : aucun merge avant maturité et nouveau verdict du gate sur ce head.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15434 (ci(lean,#2874): plomberie build-jobs (LEAN_NUM_THREADS) — unité infra du split de PR 14821) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• fort -- feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 partage : .github/actions/lean-axiom/action.yml, .github/actions/lean-build/action.yml, .github/workflows/lean-knot.yml (issues communes : [EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874)
• fort -- feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440 partage : .github/workflows/lean-knot.yml (issues communes : [EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874)