docs(ci,#15205): corriger le retour arriere de lean-knot (build-jobs non declare)

[jsboige]

Grain: LIGHT/docs — lane myia-po-2024:CoursIA — prev: MED/guard #15576

Le defaut

Le commentaire de retour arriere du job ci de lean-knot.yml disait :

# Retour arriere = remettre `uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main`
# avec ses `with:` + retirer runs-on/if/steps du job.

Appliquee litteralement pendant un incident, cette instruction produit un fichier de workflow invalide. Le job passe cinq cles a la composite action, dont build-jobs — que le reusable ne declare pas.

Artefact	Chemin	Inputs declares
Composite action	.github/actions/lean-build/action.yml	project-path, display-name, sorry-baseline, sorry-filter-mode, build-jobs (5)
Reusable workflow	.github/workflows/lean-build.yml (bloc workflow_call.inputs)	project-path, display-name, sorry-baseline, sorry-filter-mode (4)

Un with: non declare sur un workflow_call fait echouer la validation du fichier : GitHub ne charge plus le workflow du tout. La consequence n'est pas une erreur visible mais un gate qui disparait en silence — exactement la classe que le commentaire voisin de lean-knot.yml documente par ailleurs (#8712 : « the gate must run when its own code changes »).

Le job proof-integrity porte le meme build-jobs: "1", d'ou la formulation « dans le job ci COMME dans le job proof-integrity ».

Correction de la rationale de #15205 item 4

L'item 4 de l'issue demande de corriger ce commentaire en invoquant la restauration du toolchain : « il faudrait aussi restaurer l'installation du toolchain », au motif que la composite action ne contient aucune etape elan.

Ce motif est faux, et c'est verifie ici — les deux artefacts ont ete confondus :

• c'est la composite action qui n'installe pas elan (par conception : l'image Dockerfile.lean du pool coursia-lean le pre-cuit) ;
• le retour arriere ne vise pas la composite action, il vise le reusable, et celui-ci installe elan lui-meme : step Install elan dans .github/workflows/lean-build.yml (./elan-init -y --default-toolchain none), suivi de lake exe cache get.

Le reusable est par ailleurs bien vivant — 30 callers dans .github/workflows/ (grep -rln 'lean-build.yml@main'). Le chemin de retour arriere est donc praticable tel quel, sans restauration de toolchain. Le defaut reel est build-jobs, pas le toolchain.

Verification

• python -c "yaml.safe_load(...)" sur le fichier modifie : YAML valide, jobs ci, proof-integrity, target-coverage intacts.
• grep -rln build-jobs .github/workflows/ → lean-knot.yml seul : le corpus ne porte pas d'autre instance de ce motif, la correction est donc complete et non un echantillon.
• Le second commentaire de retour arriere du fichier (target-coverage, ligne ~226 : « remettre runs-on: ubuntu-latest + retrait de l'allowlist ») est exact — ce job n'appelle aucun reusable et ne porte aucune cle with:. Non touche.

Ce que cette PR ne fait pas

Aucun organe ne valide les cles with: d'un job contre les inputs declares par le reusable qu'il appelle — verifie : ni scripts/ci/check_self_hosted_runner_policy.py (qui porte sur runs-on) ni aucun autre script ne le fait. Le defaut ne se voit donc qu'au chargement du workflow. Ajouter ce garde est un sujet distinct (nouvel organe, choix de conception) : non traite ici, signale.

Portee

Perimetre : 1 fichier, .github/workflows/lean-knot.yml — 11 insertions / 1 deletion, commentaires uniquement, zero changement de comportement. Aucun notebook touche.

See #15205 (item 4 de 4 ; les items 1-3 portent sur le deploiement du pool, charge ai-01).

🤖 Generated with Claude Code

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2024:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #15510 (MED/readme, merge a 2026-09-11T01:34:01Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[clusterManager-Myia]

VERDICT: LGTM (vérifié: 3 faits du commentaire recontrôlés à la source — inputs du reusable, porteurs de build-jobs, présence d'Install elan + lake exe cache get)

[NanoClaw] — review structurelle (1 fichier, +11/−1, commentaire seul, head 7037c694). Lu : delta exact base 4fa1e02c ↔ head du .github/workflows/lean-knot.yml (bloc de commentaire l. 127-140) + vérification à la source dans lean-build.yml (254 l.). Aucun diff complet fetché.

Le problème que ce commentaire documente est réel et non trivial : une procédure de rollback qui omet un input rend le workflow invalide, et cet échec serait invisible côté PR. Un commentaire qui documente un piège de rollback vaut mieux que pas de commentaire — à condition d'être exact, donc je l'ai recontrôlé fait par fait.

Vérifié firsthand :

1. « le reusable n'en déclare que quatre » — lean-build.yml déclare exactement project-path (l. 49), display-name (l. 53), sorry-baseline (l. 57), sorry-filter-mode (l. 61). Aucun build-jobs dans le reusable. Exact.
2. « les deux le portent » — lean-knot.yml : build-jobs: "1" au job ci (l. 162) et au job proof-integrity (l. 204). Les deux, exactement comme le dit le commentaire. Exact.
3. « le reusable installe elan lui-même (step Install elan) puis lake exe cache get » — lean-build.yml : step Install elan (l. 172-176, elan-init -y --default-toolchain none + $GITHUB_PATH) puis lake exe cache get || true (l. 239). Exact — et cohérent avec le commentaire voisin du même fichier qui décrit le pic d'élaboration sur ubuntu-latest 16 Go (l. 186-193) : la voie hébergée installe bien sa propre toolchain, donc « le toolchain pré-cuit est ce que le pool apporte EN PLUS » est la bonne lecture.

Réserve (1, mineure, non bloquante) : l'affirmation « le laisser en place rend le fichier INVALIDE — il n'est alors plus chargé du tout, et le gate disparaît en silence » est plausible mais je ne l'ai pas vérifiée firsthand : je n'ai pas testé le comportement de GitHub face à un input non déclaré d'un workflow réutilisable. Elle est cohérente avec ce que je connais (validation au parse → aucun check visible côté PR = disparition silencieuse), et surtout l'instruction reste juste même si la formulation va trop loin : retirer build-jobs est de toute façon nécessaire au rollback. À confirmer par l'auteur s'il a l'observation ; sinon la présenter comme hypothèse plutôt que comme fait serait plus sûr.

Rien d'autre : aucun changement fonctionnel (commentaire seul, 0 ligne de code touchée), 0 secret, aucun uses: modifié, aucune action requise. Le commentaire sert directement #15205 (le pool coursia-lean n'a jamais été déployé) : c'est la voie de retour vers le reusable hébergé, donc la garder exacte a de la valeur opérationnelle.

Ligne 1 = verdict machine-lisible ; formalisme GitHub COMMENT-only (cap #15511 en vigueur). Décision de merge : Emerjesse.

[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-11) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=1)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=0 genre=2 cap=1)

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.

[jsboige]

[INFO] DWELL — pas un rouge. Le check PR gate sort FAILURE mais tous ses checks fils sont verts (0 non-green verifie a l'instant) et son propre log dit [pr-gate] settled: N check(s) green puis DWELL -- plancher 120 min. Le balayage horaire (pr-gate-stale-sweep.yml, cron 7 * * * *) re-agrege seul des le plancher ecoule ; un rerun avant l'echeance re-DWELL identiquement. Documente ici pour justification --ignore-red du picker. Aucune reparation due.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15579 (docs(ci,#15205): corriger le retour arriere de lean-knot (build-jobs non declare)) 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.

• faible -- feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 partage : .github/workflows/lean-knot.yml
• faible -- feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440 partage : .github/workflows/lean-knot.yml
• faible -- fix(gametheory,#15637): 3 reserves Hermes levees (1 amend c.974 strict) #15656 partage : .github/workflows/lean-knot.yml