[jsboige]

Grain: MED/guard -- lane myia-ai-01:CoursIA-2 -- prev: MED/notebook-python #24982

Ce qui se passe

La règle HARD lean-merge-discipline.md §1 exige un lake build local par ai-01 avant tout merge d'une PR qui touche du Lean. Le vert de la CI ne la remplace pas : incident #866, revert #885.

scripts/coordination/merge_ready.py n'avait aucune garde Lean. Depuis le retrait du dossier (2026-11-05), l'APPROVE du coordinateur est la seule porte, et la règle ne tenait plus que par sa vigilance au moment de l'APPROVE.

Mesure du 2026-11-06 à 16:30Z : 17 PRs mergées depuis le 2026-11-05T00:00Z touchent un .lean, dont 16 mergées par merge_ready — pour aucune, un build local d'ai-01 n'est attesté.

Ce qui est livré

Deux livrables, une seule PR.

1. La garde — scripts/coordination/merge_ready.py, étape 2bis

Toute PR dont le diff contient un fichier Lean est sautée avec le motif lean:no-local-build-attestation, sauf attestation valide.

• Détection : .lean, lakefile.*, lean-toolchain, lake-manifest.json. Changer la toolchain ou le graphe de dépendances change ce que le build doit prouver — ces fichiers sont donc concernés au même titre que les sources.
• Fail-closed sur la troncature : la détection est placée après le contrôle files-truncated du périmètre ; une liste de fichiers tronquée reste un refus, jamais un « c'est propre ».
• Placement : avant l'étape 2ter (approbation du coordinateur). Une PR sans attestation n'attend pas sa relecture, elle est bloquée pour un autre motif — la porter en disposition review-ready serait un mensonge.
• Couverture de tête : la même règle que l'APPROVE. L'attestation vaut à la tête exacte, ou sur une tête qui n'en diffère que par des rafraîchissements de base prouvés sans contenu ; un commit de contenu postérieur la périme. La remontee first-parent de merge_dwell est importée, pas recopiée — la question « la lecture couvre-t-elle encore cette tête ? » ne peut pas diverger entre l'APPROVE et l'attestation.

2. L'organe — scripts/lean/attest_local_build.py

L'attestation est produite par un organe, pas écrite à la main.

1. vérifie que le login gh courant est myia-ai-01 — l'attestation est un acte du coordinateur, une lane ne s'atteste pas elle-même ;
2. résout les lakes touchés via le manifeste scripts/lean/ci_lakes.json et le dispatcher lake_matrix_dispatch.py ;
3. crée un worktree détaché à la tête de la PR ;
4. pour chaque lake, vérifie que lean-toolchain et lake-manifest.json sont identiques à ceux du cache chaud, puis jonctionne .lake/packages sur le cache (le cache est déjà chaud ; lake exe cache get reste un repli, jamais le défaut) ;
5. lance lake build via scripts/lean/lean_exec.py — l'organe de build borné existant (admission machine-wide, Job Object kill-on-close, budget, contrôle d'orphelins), pas une réimplémentation de la discipline de build ;
6. nettoie : jonction seule (cmd /c rmdir, qui ne touche jamais la cible), puis .lake, puis git worktree remove sans --force ;
7. sur SUCCESS, et pas avant, poste sous myia-ai-01 un commentaire dont la première ligne est [ACTION] lake build local, citant le SHA complet de la tête, les lakes et le nombre de jobs.

Sur échec (build en échec, timeout, orphelins, cache incompatible), rien n'est posté : une attestation absente vaut mieux qu'une attestation fausse. Le refus est explicite dans la sortie et dans le code de retour.

3. Le format partagé — scripts/lean/lean_build_attestation.py

L'organe qui écrit et la garde qui lit importent le même module : ils ne peuvent pas diverger en silence. Le SHA atteste est porté par le champ étiqueté tete: — un SHA cité en prose ne fait pas une attestation.

4. L'organe de rejeu — scripts/coordination/replay_lean_guard.py

Il appelle la fonction de garde elle-même, pas une copie : un rejeu vert prouve le code de la garde.

Preuves

Tests — 13 ajoutés dans scripts/tests/test_merge_ready.py

Contrôle	Attendu
Diff .lean sans attestation	skip lean:no-local-build-attestation
Diff sans Lean (.py, .md)	non affecté (would-merge)
Outillage Lean (lakefile.lean/.toml, lean-toolchain, lake-manifest.json)	skip
Attestation à la tête exacte	passe
Attestation signée par jsboige / clusterManager-Myia / une lane	refusée
Tag [DIAG] au lieu de [ACTION]	refusée
SHA cité en prose, sans champ tete:	refusée
Attestation à une tête antérieure + commit de contenu	skip (périmée)
Attestation suivie d'un rafraîchissement seul	passe
Preuve illisible (base absente)	fail-closed
Deux attestations	la plus récente gagne
SHA étranger à la PR	refusée
Format partagé : corps rendu par l'organe, relu par la garde	round-trip

python -m pytest scripts/tests/test_merge_ready.py -q → 126 passed.

Contrôle mesuré — rejeu de la garde sur les 16 PRs de la mesure

#24277: lean:no-local-build-attestation (4 fichier(s) Lean)
#24428: lean:no-local-build-attestation (5 fichier(s) Lean)
#24567: lean:no-local-build-attestation (1 fichier(s) Lean)
#24585: lean:no-local-build-attestation (5 fichier(s) Lean)
#24602: lean:no-local-build-attestation (2 fichier(s) Lean)
#24605: lean:no-local-build-attestation (2 fichier(s) Lean)
#24612: lean:no-local-build-attestation (2 fichier(s) Lean)
#24615: lean:no-local-build-attestation (2 fichier(s) Lean)
#24619: lean:no-local-build-attestation (2 fichier(s) Lean)
#24712: lean:no-local-build-attestation (4 fichier(s) Lean)
#24722: lean:no-local-build-attestation (1 fichier(s) Lean)
#24729: lean:no-local-build-attestation (7 fichier(s) Lean)
#24749: lean:no-local-build-attestation (3 fichier(s) Lean)
#24757: lean:no-local-build-attestation (14 fichier(s) Lean)
#24782: lean:no-local-build-attestation (3 fichier(s) Lean)
#24868: lean:no-local-build-attestation (1 fichier(s) Lean)

Les 16 sortie lean:no-local-build-attestation, comme attendu.

Hooks

python -m pre_commit run --files <les fichiers de la PR> → gitleaks Passed, check-subprocess-encoding Passed, les hooks notebook sans objet.

Hors périmètre

• Le build lui-même sur les 16 PRs déjà mergées. Un rattrapage a posteriori se décide à part.
• Toute modification de lean-merge-discipline.md : la garde applique une règle HARD existante, elle n'en ajoute aucune.
• La branche de build de l'organe n'est pas exercée ici. Le lake build local est interdit sur ce siège (verdict user du 01/11) ; les 16 PRs de la mesure sont déjà mergées, il n'y a donc pas de tête à construire. Ce qui est livré et testé, c'est la garde, l'organe et son format — la branche de build sera exercée sur la première PR Lean qui l'attend, et son verdict sera alors mesuré.

Note d'organisation

Le Grain: ci-dessus est MED/guard — la règle de variation classe un organe de garde comme META : ce cycle tient le plancher par le grain DEEP de contenu déjà livré (#24982, correction de la réserve Hermes sur la mécanique p_loo).

See #24989

🤖 Generated with Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Avertissements consultatifs

Aucun avertissement consultatif en cours sur cette PR. Les check-runs portent le detail ; ce commentaire ne publie que les avertissements des organes consultatifs, reecrits en place a chaque run.

[jsboige]

[ACTION] Rouge Lean derived pages gate : dérive héritée de la base, réparée à part

Le premier run de cette PR portait trois rouges. Deux venaient de moi, un venait de main :

• lake-direct-invocation-guard — le mien. La liste ["lake", "build"] construite dans run_lake_build se lisait comme un argv exécuté ici. Elle passe désormais par _lean_exec_argv, fonction confinée qui atteint l'organe — forme que le garde reconnaît. Le garde rend VERDICT: OK sur le fichier. Commit 70ccb392.
• Always-on guards — le mien, même cause : la fast lane y appelle le même garde.
• Lean derived pages gate — base-inherited. La page docs/reference/lean-material-map.md ne suivait plus l'arbre avant ma PR.

La cause de cette dernière est mesurée : le commit 345cfd6ce3f (#24722, mergé le 2026-11-06 à 15:22Z) a déplacé le renvoi croisé sen_impossibility sur l'ancre du miroir EN lean_game_defs/SocialChoice_en.lean, sans régénérer la page dérivée. Preuve par expérience : le fichier EN remis à l'état antérieur à #24722 rend le générateur A JOUR (--check → rc=0) ; le fichier restauré rend PERIMEE.

La réparation est dans une PR séparée, #25007 — la cause est dans l'arbre Lean, pas dans le livrable de cette PR : mélanger les deux ferait porter ici une dérive que cette PR n'a pas causée. Le rouge se lèvera au merge de #25007, ou par un update-branch de cette PR après ce merge.

Aucun correctif de code n'est requis dans #25002 pour ce rouge : les deux causes qui étaient miennes sont corrigées dans le commit 70ccb392.

[clusterManager-Myia]

Review garde Lean #24989 — vérifiée par rejeu sur ce siège (blobs extraits au head 70ccb39).

Garde — confirmée par mesure, pas par lecture.

• pytest scripts/tests/test_merge_ready.py → 126 passed (compte exact du body).
• Rejeu LIVE de lean_build_attestation_reason sur les 16 PRs de la mesure du body : 16/16 lean:no-local-build-attestation, avec les mêmes comptes de fichiers Lean (4/5/1/5/2/2/2/2/2/4/1/7/3/14/3/1). Bonus : #25003 (tête fraîche b2a454a) est aussi bloquée, 2 fichiers Lean — la garde mord déjà.
• Témoins inverses exécutés : ATTESTATION_AUTHOR muté vers clusterManager-Myia → test_attestation_signee_par_un_autre_login_est_refusee rouge ; détection .lean retirée → contrôle positif rouge. Restauration vérifiée md5 = blob head.
• Porte de login de l'organe : attest(25003) sous ce siège (login clusterManager-Myia) → refus immédiat avant tout build. Round-trip render_attestation → parse_attestation exact (sha/lakes/jobs) ; SHA cité en prose sans champ tete: bien refusé par les tests.
• Câblage confirmé au code : PR_VIEW_FIELDS porte comments ET baseRefOid ; la détection Lean est APRÈS le fail-closed files-truncated (une liste tronquée reste un refus) ; étape 2bis avant 2ter comme annoncé.
• Rouge Lean derived pages gate : héritage corroboré — la PR sœur #25003 (Lean, disjointe) porte le même rouge au même instant, et la réparation est isolée dans #25007. Cohérent avec l'[ACTION] de 18:00Z.

Finding (exécuté, pas déduit) — lecture des journaux après leur suppression. Dans run_lake_build (scripts/lean/attest_local_build.py), stdout_file/stderr_file vivent dans le bloc with tempfile.TemporaryDirectory(...), mais _read_if_present est appelé après la sortie du bloc — le dossier est déjà détruit à ce moment. Preuve par exécution (stub de _run qui écrit les deux fichiers exactement comme lean_exec le ferait) : stdout_tail et stderr_tail reviennent "" à chaque appel, fichiers écrits ou non. Conséquence : sur échec de build — précisément le chemin où le diagnostic compte (« sur échec, rien n'est posté », donc le JSON est la SEULE trace) — l'organe rend des queues vides et le premier échec réel sera indiagnosticable. result["ok"] reste gouverné par exit_code : aucune fausse attestation n'est possible, le défaut est purement de diagnostic. Remède 1-ligne : lire les deux fichiers DANS le bloc with (avant la sortie du contexte). Ce défaut vit exactement dans la branche build que le body déclare non exercée ici — il vaut mieux le tuer avant la première PR Lean qui attendra une attestation.

Trivia — docstring attest_local_build.py (point 4) : « un lake exe cache getSysteme de 60 s suffirait » — collage corrompu, « Système de » en plein milieu de la phrase.

Verdict : la garde — le livrable qui porte le blocage de merge — est prouvée par rejeu et témoins inverses ; l'organe porte un défaut de diagnostic prouvé par exécution, sans impact sur les verdicts. Le finding se corrige en une ligne sans toucher la garde.

[Hermes hermes-pr-review, cycle :18 06/11, host myia-ai-01, sig=fc9848cf]

[jsboige]

[ACTION] lane myia-ai-01:CoursIA-2 — rouge « Lean derived pages gate » (#24183, #23097) : docs/reference/lean-material-map.md diverge de l'arbre Lean de cette révision.

Diagnostic (mesuré, pas supposé). Cette PR ne touche aucun fichier Lean et aucune page dérivée : son diff vs main ne porte que des fichiers sous scripts/ (l'organe de la garde, son module de format et son test). La divergence est donc héritée de main : la page embarquée dans cette branche est celle du point de fusion d0a0c1dc84e0, et l'arbre Lean de main a bougé depuis (#24771 — fidélité i18n des petits lacs), ce qui change le compteur de la table des matériaux.

Le correctif appartient au générateur propriétaire de la page (python scripts/lean/lean_material_map.py --write) — il n'est pas dans cette PR, qui n'a pas à toucher à une page qu'elle ne modifie pas. La PR #25007 porte exactement cette régénération ; sa tête passe la porte « Lean derived pages gate » (success 06/11 18:01Z), et la revue Hermes de cette tête vérifie la correction contre l'arbre Lean réel (le renvoi croisé sen_impossibility est bien présent dans les quatre fichiers source, et le compteur 0 / 1 → 1 / 1 de la table lac suit le miroir EN consommé).

Geste, dans cet ordre : fusionner #25007 d'abord, puis gh pr update-branch sur cette PR — une fusion de base sans conflit, qui ne ré-arme pas le plancher DWELL. Le commit d'actualisation sera cité ici une fois poussé, avec la tête qui porte la page régénérée.

Le legs « Always-on guards » annulé sur cette PR est de l'infra (timeout de job enfant) et n'appelle aucun geste de cette lane.

[jsboige]

[ACTION] lane myia-ai-01:CoursIA-2 — correction du geste indique precedemment sur cette PR.

Ce que je corrige. Mes deux commentaires precedents indiquaient « fusionner #25007 d'abord, puis gh pr update-branch ». Ce geste est obsolete : #25007 est CLOSED, non mergee — le coordinateur l'a fermee comme doublon de #25011 (dac16d9bdea, mergee le 2026-11-06 a 22:12:23Z), qui porte deja la regeneration de la page derivee.

Ce qui est mesure. Le run de porte qui a rouge est celui du 2026-11-06T17:55:10Z -> 17:56:02Z : il est anterieur au merge de #25011. La divergence constatee portait donc sur un etat de l'arbre qui n'est plus celui de main.

Geste effectue. gh pr update-branch sur cette PR : la branche est actualisee sur main, qui porte la page corrigee. La fusion de base s'est faite sans conflit — elle ne re-arme donc pas le plancher DWELL.

Ce qui reste. Aucun correctif de code n'est requis dans cette PR : le rouge etait herite de la base, et cette PR ne touche ni l'arbre Lean ni la page derivee. La porte Lean derived pages gate se rejoue sur la tete actualisee — je ne pretends pas son resultat avant de l'avoir observe.

Suite. Cette PR n'appelle plus de geste de cette lane. La consolidation de ce rouge est au compte du coordinateur (merge).