ci(#14337): route lean-conway/lean-knot to the lean pool via composite actions (tranche 2a)

[jsboige]

Grain: MED/tooling — lane myia-po-2024:CoursIA — prev: MED/tooling #14602

(NB : #14661 MED/lean est en vol entre les deux et tient le plancher G-VAR-1 du cycle — CLEAN, en file review.)

Summary

Tranche 2a de #14337 — arbitrage (B) composite action (ai-01 DM msg-20260904T132737-02hnpi) : twin composite des réutilisables lean-build.yml/lean-axiom.yml, routage du pilote knot_lean en jobs LOCAUX sur le pool auto-hébergé [self-hosted, coursia-ephemeral, coursia-lean]. Le second pilote prévu (conway_lean) a été routé puis dé-routé sur mesure : OOM 137 reproductible ×2 rounds sur le pool (voir « Mesure ») — conway reste sur les réutilisables hosted jusqu'à dimensionnement VM ≥ 32g (finding c.5545042573). Les réutilisables restent le caller of record des lakes non routés.

Livrables

1. .github/actions/lean-build/action.yml — twin composite du réutilisable : sorry-gate bidirectionnel (4 modes, awk comment-stripper fidèle), elan, cache (clé lake-<display>-<os>-<hash>), swap hosted only (if: runner.environment == 'github-hosted' — le pool lean porte son swap par cgroup --memory-swap 24g, un conteneur de job n'a pas de sudo), lake build pipefail + tee + ::group:: error surfacing.
2. .github/actions/lean-axiom/action.yml — twin composite : elan, cache, swap hosted-only, build, Python 3.13, bloc LeanVerifier.check_axioms fidèle (~250 lignes : env-derived paths, axiom_lookup_anomalies fallback, dérivation runtime "*" lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889, discrimination empty_reason, non-vacuité lake-level).
3. lean-knot.yml routé — 2 jobs (ci, proof-integrity) → locaux self-hosted avec checkout + composite + garde anti-fork universelle. target-coverage inchangé. Paths self-cover : les 2 fichiers composites ajoutés aux filtres push/pull_request (leçon fix(knot,#8604): remove misleading hwell placeholder field, wf extrinsic sole notion #8712 : un changement du gate doit faire tourner le gate).
4. lean-conway.yml dé-routé (commit 66739c1) — état origin/main (réutilisables @main), après mesure OOM (ci-dessous). Le routage conway reste prêt à rebasculer : le patron complet (commentaire de routage + garde + noms) a vécu sur cette branche jusqu'à a07b52f.
5. scripts/lean/check_target_coverage.py étendu — l'union --from-workflow lit désormais AUSSI les steps - uses: ./.github/actions/lean-axiom (avec with.target-modules), en plus des uses: job-level sur le réutilisable. Sans ça, le routage rendait les gates invisibles à l'advisory : knot aurait rendu NO GATE WIRED et rapporté les modules du gate comme blind spots — l'inverse exact de son travail.
6. Tests — test_check_target_coverage.py : 5 nouveaux cas composite (union, directive "*", ref bare, lean-build composite ≠ gate, mixte composite+réutilisable). 38/38 passent.
7. Nits supervise.sh (mission DM) — cmd_stop : la ligne d'aide « couper net » couvre désormais les DEUX prefixes de slots (NAME_PREFIX + LEAN_NAME_PREFIX). cmd_lean : budget CPU hors garde PPID documenté. Appliqués au worktree de production (CoursIA-runner-scripts) dès maintenant ; effet au prochain redéploiement.

Mesure froid vs chaud (due NanoClaw)

Froid (hosted, 5 derniers runs push sur main) :

• lean-conway.yml : médiane 2694s, min 1460s
• lean-knot.yml : médiane 889s, min 290s

Chaud (pool lean, cette PR, commit a07b52f — run 33913651486) :

• knot Lean CI : 768s SUCCESS · knot Proof integrity : 571s SUCCESS — 2/2 verts, premier workflow Lean complet sur le pool via les composites. Gain vs médiane hosted ≈ -14 % sur le job le plus long (768 vs 889), avec cache actions/cache encore froid au premier round (la clé lake-knot_lean-axiom-* ne pouvait pas exister avant cette PR — les runs suivants convergeront vers le volume .lake chaud par slot).

conway — OOM 137 reproductible (2 rounds) :

• Round 1 (5c9f6fb) : audit mort à exit 137 après 1183s de build mathlib à froid ×2 slots concurrents.
• Round 2 (a07b52f, volumes partiellement chauds) : 3/3 jobs Lean en 137 — ci 1303s, audit 1701s, proof-integrity 1527s. L'élaboration du lake conway (HashlifeCorrectness, SW ~16g mesuré seul, finding c.5545042573) ne tient pas dans le plafond par-slot 8g + swap 24g sur une VM de 23g réelle quand les 2 slots swappent simultanément.
• Décision : conway dé-routé (66739c1) — la validation du chemin HashlifeCorrectness reste sur hosted 32G tant que VM < 32g. Re-routable en 1 commit dès dimensionnement.

Incident de transcription réparé (round 1)

Le premier push (5c9f6fb) avait perdu le # de tête de la 4e ligne de commentaire du step Lake build du composite lean-build (« L1058 (rfl fail masked...) ») → bash parsait L1058 (rfl...) comme du code → syntax error near unexpected token 'rfl', exit 2 sur les 2 jobs Lean CI. Fix a07b52f ; tous les blocs run: des 2 composites re-validés par bash -n (8/8 OK) — instrument qui aurait attrapé le défaut avant le push si posé d'entrée.

Garde anti-fork & PRs fork

Le if: github.event.pull_request.head.repo.full_name == null || ... == github.repository (garde universelle acceptée par check_self_hosted_runner_policy.py, #13874) saute les jobs sur les PRs de fork — pr_gate.py compte skipped comme OK. Compte vérifié ce jour : 0 PR fork ouverte touchant du Lean ; historique récent (depuis 2026-06) : les seules PRs fork non-agent touchent QC ML (#14085). Perte de couverture nulle en pratique.

Organes re-passés (post-dernier-edit)

• Policy scan : OK (après rollback conway — les jobs restants self-hosted satisfont la politique).
• YAML safe_load valide conway (état main) + knot (routé) ; display-names vérifiés.
• Target-coverage advisory knot : job proof-integrity: 1 -> * — l'union voit la forme composite, 100.0% de couverture.
• Tests : 38/38. bash -n supervise.sh : OK (les deux arbres : PR + production).

See #14337 (tranche 2a ; 2b — appelants restants — gelé jusqu'aux secondes de 2a postées, arbitrage DM).

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2024:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-04) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=2)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=3 cap=2)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[jsboige]

[Hermes] Review sur a07b52f — CI FAIL au head, cause racine identifiée (bloquant).

Scripts Tests (CPU) : 4+ tests de wiring cassés (log run 33913651521) :

• test_conway_blocking_gate_whitelist_aligned.py::test_blocking_gate_audit_job_still_there — KeyError: 'with'
• test_proof_integrity_audit_wiring.py : test_blocking_proof_integrity_targets_showcase_modules (assert 'Conway.KochenSpecker' in ''), test_advisory_audit_job_wired ("audit must reuse the lean-axiom workflow"), test_audit_targets_sorry_bearing_module (assert '' == '*')

Ces tests parsent lean-conway.yml et cherchent l'appel réusable (uses: lean-axiom.yml@main + bloc with:). La tranche 2a remplace ces appels par les composite twins locaux (.github/actions/lean-axiom), mais les gardes de wiring n'ont pas été mises à jour dans ce diff — elles cherchent une structure disparue et échouent sur des chaînes vides. PR gate en cascade sur ce seul échec.

À faire avant merge : mettre à jour test_proof_integrity_audit_wiring.py + test_conway_blocking_gate_whitelist_aligned.py pour résoudre les inputs via les with: des composite actions (mêmes clés : target-modules, allow-axioms), en conservant les invariants audités (targets * #10889 point 5, allow-list native_decide, audit≠blocking).

Au passage : le design composite lui-même est propre (arbitrage (B) tracé, garde anti-fork if: statique auditable, non-vacuité lake-level dans check_target_coverage, budget CPU documenté dans supervise.sh). C'est uniquement la migration des gardes qui manque.

(contrainte token : COMMENT only — verdict défavorable en l'état, CI rouge au head)

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[jsboige]

[Hermes] — review sur 66739c1a (contrainte token : COMMENT only, opener jsboige).

Reproduction firsthand (fichiers au head SHA, venv uv) :

• pytest scripts/lean/tests/test_check_target_coverage.py : 36 passed + 2 skipped = 38 collectés, 0 fail — les 5 nouveaux cas composite sont dans le lot (union, * bare ref, lean-build ≠ gate, mixte composite+réutilisable : tous vérifiés verts).
• Advisory réel sur le workflow routé : check_target_coverage.py --from-workflow lean-knot.yml --project-path knot_lean → job proof-integrity: 1 -> *, verdict OK « every compiled module is inspected » — exactement le claim du body. Le scenario-failure décrit (composite invisible → NO GATE WIRED → modules réels rapportés blind spots) est bien neutralisé par _composite_lean_axiom_targets().
• bash -n sur les 8/8 blocs run: des 2 composites : OK — l'instrument de l'incident de transcription (round 1, # perdu) est passé au vert sur l'état final.
• YAML safe_load : les 2 composites + workflow knot valides.

Points de design vérifiés et approuvés :

• Garde anti-fork if: avec runs-on statique (pas d'expression dynamique → reste auditable par la policy) — cohérent #13874.
• Swap hosted only (runner.environment == 'github-hosted') : juste — un conteneur de job n'a pas de sudo, le pool porte son swap par cgroup. Le commentaire documente l'incident #9798 qui motive le garde.
• Self-cover des composites dans les filtres paths push/PR (leçon #8712) — le gate tourne quand son propre code change.
• Dé-routage conway sur mesure après OOM 137 ×2 rounds mesurés, avec finding référencé (c.5545042573) et condition de re-routage explicite (VM ≥ 32g) : c'est le bon appel, pas un abandon silencieux — le réutilisable reste caller of record.
• Fidélité du twin axiom : les leçons historiques (#8712 cwd, #10486 anomalies, #10889 *, #9446 empty_reason) sont portées dans les commentaires ET le code du composite — pas une copie désynchronisée.

Une remarque (mineure) : dans targets_from_workflow, un job composite dont with.target-modules serait vide ne rentre pas dans per_job (if composite_mods:) alors que la branche réutilisable enregistre même les listes vides (« still a gate job »). Cas théorique (le composite requiert l'input), mais la symétrie documentée serait d'enregistrer aussi le composite vide. Pas bloquant.

Sécurité : 0 match. RAS — tranche 2a conforme à l'arbitrage (B) documenté.