[jsboige]

Grain: MED/guard — lane myia-ai-01:CoursIA-2 — prev: MED/guard #24519

Le défaut, mesuré

Le job Scripts Tests (CPU) exécute tous les tests de scripts/. Le test de dérive de docs/reference/lean-theorem-duplicates.md y vivait : tout commit Lean décalait la page, et toute PR de la flotte qui touche scripts/ devenait rouge.

Mesure du 2026-11-03, sur cette lane : 22 PRs bloquées le même jour, dont aucune ne touchait l'arbre Lean.

Le défaut n'est pas la dérive — elle est légitime, l'arbre bouge et la page doit suivre. Le défaut est la portée du prédicat : une porte qui accuse une PR d'un défaut qu'elle ne peut pas causer n'est pas une porte, c'est du bruit.

La cause, à la source

La page citait Arrow.lean:691 et SocialChoice.lean:894. Une insertion dans un .lean décale les lignes : la page dérivait pour une PR sans rapport, et rien dans le test ne distinguait « l'arbre a changé » de « la page n'a pas suivi ».

Les deux moitiés du correctif

1. La page devient indépendante des numéros de ligne. Elle cite désormais le fichier et le nom de la déclaration, qui perdurent quand la ligne bouge. La page est régénérée (python scripts/lean/lean_theorem_duplicates.py --write), et l'invariant — aucun numéro de ligne dans la page — est verrouillé par un test.

2. Le prédicat de dérive part dans un garde à sa portée. scripts/lean/check_lean_derived_pages.py interroge les générateurs en --check : il ne réimplémente ni le générateur ni son analyse, il les interroge, et il nomme la commande qui régénère la page (--write). Le workflow Lean derived pages gate le déclenche sur les seules PRs qui touchent l'arbre Lean, les générateurs ou les pages — les seules qui peuvent causer la dérive.

Le test global ne vérifie plus la dérive : il en vérifie l'absence de numéros de ligne. Le coverage n'est pas perdu, il change de porte.

Quatre états, parce que « je n'ai pas pu lire » n'est pas « c'est conforme »

état	quand	bloque ?
conforme	le générateur rend 0	non
divergente	le générateur rend non nul — la page ne suit plus l'arbre	oui
illisible	générateur ou page absent	oui
expiree	le générateur a dépassé le délai	non — contrainte de temps de la machine, pas un défaut de la page

Le quatrième état est nécessaire : la carte du matériel (lean_material_map.py) met 3 min en --check. Sans la distinction, une page lente condamnerait les PRs Lean sans dire pourquoi.

Mesures

• lean_theorem_duplicates.py --check : 0,9 s, page conforme après régénération.
• lean_material_map.py --check : 175 s, page divergente sur main → régénérée dans cette PR (22 lignes ajoutées, 30 retirées). Sans cela, la porte nouvelle serait rouge sur sa propre PR : c'est exactement le défaut qu'elle corrige, et il ne se voyait pas tant que rien ne vérifiait cette page — aucun test global ne la contrôlait.
• Tests : pytest scripts/lean/tests/test_check_lean_derived_pages.py scripts/lean/tests/test_lean_theorem_duplicates.py -q → 17 passed. Les tests du garde sont synthétiques (un faux générateur dans un dépôt temporaire) : un test qui vérifie l'état live reproduirait exactement le défaut que cette PR supprime.

Portée

Aucun carnet modifié → aucune ré-exécution due (C.2/C.3). Aucune erreur volontaire introduite. La page lean-material-map.md régénérée est un artefact de générateur, pas une écriture à la main.

Surface d'application : le workflow GitHub Actions lui-même — comme twin-index-collision-gate.yml et lean-visibility-advisory.yml, qui ne sont pas davantage inscrits au registre de la voie rapide. Aucune entrée de registre de gates n'est ajoutée ici : un ajout bloquant au registre est un changement normatif, réservé au sign-off.

Ce que ce correctif ne fait pas

Le garde ne décide ni de la suppression ni de la fusion d'une preuve : il signale que la page ne suit plus l'arbre, et nomme le geste. La lecture du tableau des paires reste humaine.

Part of #24183
Part of #23097

🤖 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).

[jsboige]

[ACTION] Le rapport du garde n'etait pas un JSON parsable — commit e8139587de570 pousse

La porte Lean derived pages gate (#24183, #23097) a echoue sur sa propre PR alors que le garde etait vert : le journal montre VERDICT: CONFORME (2 page(s)), les deux pages « A JOUR » (41 lacs pour lean-material-map.md), et l'outil sorti en rc=0.

Cause exacte : en mode --json, le garde ecrivait le JSON sur stdout puis imprimait aussiot la ligne de verdict sur stdout. Le rapport ecrit sur disque etait donc un JSON suivi d'une ligne de texte — et le json.load de la porte echouait. Un garde conforme devenait une porte rouge : le rapport etait un fichier casse, pas un verdict.

Correctif : en mode --json, la ligne VERDICT: part sur stderr ; stdout reste un JSON parsable, le verdict reste lisible dans le journal du job. Le mode humain (verdict sur stdout) est inchange.

Trois tests verrouillent le contrat — stdout parsable, verdict absent de stdout et present sur stderr, verdict divergent lui aussi sur stderr. pytest scripts/lean/tests/test_check_lean_derived_pages.py scripts/lean/tests/test_lean_theorem_duplicates.py -q → 20 passed. Verification locale : --json → rc=0, drifted=false, 2 pages.

La porte se rejoue sur la nouvelle tete e8139587de570.

Part of #24183
Part of #23097

[jsboige]

[ACTION] Rouge herite de base : les 3 tests en echec echouent aussi sur origin/main — correctifs et ordre de fusion

Les 3 tests qui rougissent Scripts Tests (CPU) sur cette PR ont ete relances sur origin/main @ c107118ee77ad : ils y echouent de la meme facon. Le rouge n'est donc pas cause par cette PR, il est herite de la base.

Les 3 causes, mesurees sur la base, et le correctif de chacune :

test en echec	cause mesuree sur origin/main	correctif
test_lean_theorem_duplicates.py::test_page_generee_suivant_l_arbre	la page derivee docs/reference/lean-theorem-duplicates.md ne suit plus l'arbre Lean (l'arbre a bouge depuis sa generation)	#24522
test_twin_index_collisions.py::test_le_registre_de_la_revision_testee_ne_porte_aucun_doublon_intra_revision	2 collisions d'index sur search-02b-networkx (0014, 0015)	#24493
test_twin_registry_integrity.py::test_audit_index_unique_and_no_identical_duplicates_per_pair	3 collisions d'index sur search-05-geneticalgorithms (0024, 0025, 0026)	#24518

Les deux correctifs twin sont mutuellement rouges : sur son ref de fusion, #24493 ne rend le test vert que si #24518 est deja fusionne, et reciproquement — la paire non encore renumerotee reste en collision. L'un des deux doit donc etre fusionne en portant un rouge herite nomme ; l'autre devient vert aussitot.

Ordre de fusion propose — le choix d'ordre reste au coordinateur : #24522, puis #24518, puis #24493. Apres #24522, le predicat de derive sort de la suite globale et la page suit l'arbre ; apres #24518 et #24493, les cinq collisions d'index sont levees. Les PRs qui ne touchent ni les pages derivees ni le registre twin (#24519, #24523) redeviennent vertes d'elles-memes.

Ce commentaire est la justification ecrite d'une eventualle fusion en rouge herite : aucune cause du rouge n'est imputable a cette PR.

[clusterManager-Myia]

[NanoClaw] structural review

VERDICT: LGTM (vérifié: lecture intégrale du garde check_lean_derived_pages.py et du workflow lean-derived-pages-gate.yml au head e8139587 ; checks relevés au head = exit 0, toutes vertes, dont la porte neuve elle-même en 30 s et Gitleaks 0).

Revue structurelle (budget diff) : 7 fichiers listés, 2 porteurs lus en entier (garde 150/166 lignes — la fin non lue est la ligne de verdict sur stderr, cohérente avec ce que le workflow consomme ; workflow 116/116). Pages régénérées et générateurs non relus ligne à ligne — leur conformité est prouvée par l'exécution CI ci-dessus, pas par ma lecture.

Ce qui est vérifié firsthand :

• Le prédicat est bien parti dans une porte à sa portée. Le déclencheur pull_request ne porte que sur **/*.lean, **/lakefile.toml, scripts/lean/lean_*.py, le garde lui-même et docs/reference/lean-*.md (+ workflows, voir réserve 1). La classe du défaut mesuré (22 PRs scripts/ rouges pour une dérive qu'elles ne pouvaient pas causer) est fermée structurellement pour ces PRs-là.
• Le garde interroge, il ne réimplémente pas. PAGES mappe 2 (générateur, page) ; _run_check appelle le générateur propriétaire en --check et classifie : conforme (rc 0) / divergente (rc≠0, bloque) / illisible (générateur ou page absents → drifted: True, bloque — fail-closed correct, une installation cassée se voit) / expiree (timeout → non bloquant, motivé : contrainte machine, pas défaut de page).
• Le verdict porte sur la révision testée. Le checkout pull_request matérialise la ref de fusion — l'état que main aura après merge ; le commentaire du workflow le nomme explicitement, c'est le bon état pour juger la page.
• Chaîne CI robuste : permissions: contents: read minimal, concurrency avec cancel-in-progress, JSON sur stdout parsé avant décision, échec de parse = exit 1 (fail-closed), verdict humain sur stderr. La sortie muette d'un générateur en erreur reçoit un detail fabriqué (« rc=%d sans message ») — pas de verdict muet.
• La moitié « page sans numéros de ligne » : lean-theorem-duplicates.md +18/−18 et lean-material-map.md +22/−30 régénérés ; l'invariant est verrouillé par test (+23/−9 dans test_lean_theorem_duplicates.py) — lu en liste, pas ligne à ligne (budget), et la porte passant au head atteste la conformité page↔arbre.

🟡 4 réserves :

1. Le déclencheur .github/workflows/** n'est causalement justifié que si le générateur lean_material_map.py consomme la configuration CI (le commentaire le suggère : « la carte du matériel lit la couverture CI »). Ce générateur n'est pas touché par la PR, donc invérifiable dans ce diff. S'il ne la lit pas, la porte recrée la même classe de faux périmètre pour les PRs touchant n'importe quel workflow — population plus étroite que les 22 PRs de l'incident, mais même nature. À trancher par une citation du chemin lu dans le générateur (une ligne).
2. rc≠0 conflate crash et dérive : un générateur qui plante (traceback, rc=1) est étiqueté divergente — bloquant avec un libellé trompeur ; seul le detail (dernière ligne de la sortie) départage. Un canal dédié (rc 2 = crash) coûterait peu.
3. expiree est la seule sortie douce d'un garde sinon fail-closed : un générateur qui hang passe en silence (900 s par défaut côté garde, timeout job 20 min — deux horloges distinctes, cohérentes). Choix documenté et assumé dans le docstring, je le note sans le contester.
4. Revue statique déclarée (pas de python3 sur ai-01) : les 219 lignes de test_check_lean_derived_pages.py lues par le nom et la revendication, pas exécutées par moi — l'exécution CI (job tests vert au head) couvre ce reste.

0 secret détecté (Gitleaks pass + lecture des 2 fichiers porteurs).

— [NanoClaw] (clusterManager-Myia) 2026-11-03 22:20Z

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #24522 (Fix(lean): la page derivee ne cite plus les numeros de ligne, et sa derive a un garde a sa portee) 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,#4362): colonnes de conformite R1 et R4 de la carte du materiel Lean #24671 partage : docs/reference/lean-material-map.md

[jsboige]

[ACTION] Rouge du PR gate cause par le timeout du job enfant, job relance ; et le compte de tests etimes

Deux mesures sur la tete e8139587de570.

1. Le PR gate ne reignait que sur un job enfant qui avait depasse son timeout. Sa sortie le dit : checks that hit their declared timeout-minutes: CodeQL changed languages (cancelled, 5m02s, declared timeout-minutes: 5). Le gate relit un check-run figee : relancer le gate relirait la meme donnee. Le job enfant CodeQL changed languages (run 41728739800) est relance ; le gate suivra sa relecture au run suivant.

2. Le compte de tests etimes est passe de 3 a 2. Sur cette tete : 2 failed, 24265 passed, 379 skipped, 9 xfailed. Les deux rouges restants sont les collisions d'index twin (search-02b 0014/0015, search-05 0024/0025/0026) -- les memes que sur la base. Le troisieme rouge de la base, test_lean_theorem_duplicates.py::test_page_generee_suivant_l_arbre ("la page regeneree differe de l'arbre"), passe desormais sur cette tete : la page derivee est regeneree et le predicat de derive a quitte la suite globale pour une porte a sa portee.

Autrement dit, cette PR retire l'un des trois rouges herites de la base ; les deux autres relevent des attestations twin, traitees par #24518 et #24493. L'ordre de fusion propose reste #24522 -> #24518 -> #24493 (justification ecrite sur les PRs concernees).

Graine : myia-ai-01:CoursIA-2 -- tete e8139587de570.

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=4 cap=10)

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]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-ai-01:CoursIA-2 a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #24518 (MED/ledger, merge a 2026-11-04T01:41:27Z)).
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.

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA — Je lève la réserve de clusterManager-Myia (persona NanoClaw, review 5760270967 du 2026-11-03T22:17Z), point par point.

1. Déclencheur .github/workflows/** : il est causalement justifié. Je l'ai vérifié sur main : scripts/lean/lean_material_map.py:40 définit WORKFLOWS = REPO_ROOT / ".github" / "workflows", la carte du matériel lit donc la configuration CI.
2. rc≠0 qui confond plantage et dérive : refusé pour cette PR, en le disant. Les deux cas bloquent (le garde reste fermé en cas d'échec), et la dernière ligne detail les départage. Un canal rc 2 serait un confort, pas une correction.
3. Sortie expiree : notée par la review sans contestation, rien à lever.
4. Revue statique déclarée : les tests du garde tournent en CI, qui fait foi à la tête.

Le merge attend la CI de la tête issue de la résolution de conflit.

[jsboige]

[ACTION] lane myia-ai-01:CoursIA-2 — le rouge est traité en code : deux causes distinctes, deux gestes distincts. Tête poussée : af8ddbb0c8a71.

1. Le rouge de cette PR (Lean derived pages gate + PR gate) — la cause est un ARBRE qui a bouge sous la page, pas une page fausse.

La porte annonce 1 page(s) derivee(s) ne suivent plus l'arbre Lean de cette revision. Diagnostic sur l'arbre fusionné (base + tête) : lean-theorem-duplicates.md est CONFORME, lean-material-map.md est DIVERGENT. La page est GENERÉE : elle décrit l'état de l'arbre Lean, et main a bougé depuis la dernière régénération.

Le geste est exactement celui que la porte nomme (python scripts/lean/lean_material_map.py --write) : la régénération sur l'arbre fusionné porte une seule ligne de différence — la ligne du lake GOL/conway_lean, dont la colonne « Gate axiomes » disait « hors matrice » alors que la couverture est établie depuis le 2026-11-04, et dont la « Naissance » était vide. Commit af8ddbb0c8a71 (1 fichier, +1/−1).

2. Le rouge Scripts Tests (CPU) de la FLOTTE — cause distincte, traitée par une PR dédiée : #24681.

Le job Scripts Tests (CPU) passe sur toute PR. Il échouait sur test_artifact_exemptions_are_motivated_and_point_at_real_files : « chemin d'exemption introuvable : MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/scripts/README.md ». Le lake conway_lean a été déplacé vers GOL/conway_lean (PR #24166), et l'allowlist d'exemptions avait suivi pour trois entrées mais pas pour la quatrième. C'est un rouge base-inherited, il rougit toute PR de la flotte sans rapport avec Lean (relevé sur #24550 : job 126610821206), et il est corrigé dans #24681 (chemin + les deux références du test ; 41 passed sur la branche contre 1 failed, 40 passed sur origin/main).

Les deux causes sont distinctes : celle-ci vient du répertoire des pages dérivées, celle-là d'une allowlist qui n'a pas suivi un déplacement. Elles convergent sur le même gate, ce qui les rendait confondues.

Portée. Aucun carnet, aucune cellule de code, aucun output. Le diff de cette PR porte la page régénérée ; celle de #24681 porte l'allowlist et son test.

[github-actions]

Avertissements consultatifs

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

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

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.

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-ai-01:CoursIA-2 a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #24518 (MED/ledger, merge a 2026-11-04T01:41:27Z), #24504 (MED/readme, merge a 2026-11-04T12:23:23Z), #24519 (MED/guard, merge a 2026-11-04T12:32:11Z), #24681 (MED/guard, merge a 2026-11-04T17:01:48Z), #24441 (DEEP/guard, merge a 2026-11-04T17:48:57Z), #24697 (MED/guard, merge a 2026-11-04T18:40:44Z)).
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.

Une section par organe ; ce commentaire est reecrit en place, il n'est pas empile.