fix(lean-ci,#17336): lost_gate soustrait la couverture reprise — deplacer le gate n'est pas le perdre

[jsboige]

Grain: MED/guard — lane myia-po-2025:CoursIA — prev: MED/notebook-python #17348

See #17336 — [CLAIMED] lane myia-po-2025:CoursIA -- paths: scripts/lean/check_axiom_gate_coverage.py, scripts/lean/tests/test_check_axiom_gate_coverage.py (issuecomment-5780939529)

Diagnostic — le rouge deterministe Scripts Tests sur main

Run main 35753750580 (2026-09-22 16:23Z) : test_no_lake_ever_lost_the_gate echoue sur
{'dispatcher': 'lean-serre.yml', 'deleted_by': '78537cd49d', 'had_gate': True} — 1 failed / 14600 passed.

Fait etabli firsthand : lean-serre.yml existe TOUJOURS sur main (git log origin/main --follow -- .github/workflows/lean-serre.yml ne montre que son ajout 77bcae0 ; measure(origin/main) le liste comme appelant vivant du gate avec project-path MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/serre100_lean). Le commit de suppression 78537cd vit sur la branche de la PR #17370, pas sur main.

Le mecanisme du faux rouge : deleted_dispatchers() scanne git log --all — sur un clone CI qui a fetché les refs de la PR, la suppression laterale est visible ; l'ancien code comptait lost = [deleted qui avaient le gate] sans verifier si la couverture est encore servie au ref mesure. Main garde le fichier et le gate, le test declarait pourtant une perte.

Le fix — deplacer le gate n'est pas le perdre

• deleted_dispatchers() porte desormais gated_paths (les project-paths que le dispatcher gated, a sa derniere version).
• Nouvelle classify_deleted(deleted, gated_now) : partition lost / gate_relocated / never_had. Un dispatcher supprime qui avait le gate et dont tous les project-paths sont gates par un appel vivant au ref mesure est DEPLACE, pas perdu. Fail-closed : gate sans project-path (couverture non prouvable) reste PERDU ; un seul chemin decouvert reste PERDU.
• Rapport : cle gate_relocated + section humaine ; --check continue de ne rouge que sur lost_gate.
• Prose not_an_acceptance_criterion mise a jour (« la perte ne se declare que si aucun appel vivant ne reprend les project-paths ») — l'ancienne phrase « aucun lake n'a perdu le gate » etait devenue fausse au moment ou elle a ete ecrite, c'est le bug meme que ce PR corrige.

Tests

• TestClassifyDeleted (4 tests synthetiques, sans git) : recouverture complete -> deplace ; un chemin decouvert -> perdu ; gate sans project-path -> perdu (fail-closed) ; jamais eu -> never.
• Invariant partition : test_lost_relocated_and_never_had_are_disjoint_and_exhaustive (3 voies).
• TestDeletedDispatchers.test_partition_is_a_partition : cles attendues + gated_paths: list.
• Local : 34/34 passes (python -m pytest scripts/lean/tests/test_check_axiom_gate_coverage.py -q), y compris test_no_lake_ever_lost_the_gate sur le ref reel — ce PR verdit le test deterministe qui fait echouer les PR-gates de la flotte depuis ce matin.

Portee et suite

• Impact flotte documente : PR-gates fix(vibe): g66-search-16 — App-6-Minesweeper (mésattribution benchmark + lecture sélective) + CSP-5-Optimization-Csharp (ancrage) #17091, fix(pedagogy,#17066): QC-Py-18 — consolidation sections dupliquées 17→0, lectures replacées, 2 fusions #17078, fix(pedagogy,#13410): g55-probas-3 — DecPyMC-9 + PyMC-14 (21 corrections) #16973, fix(pedagogy,#13410): g79-search-4 — densité App-15-SportsScheduling + Search-02b-NetworkX (46 lectures, ids réparés) #17208, enrich(search,#13410): densite g82-search-7 — 12 lectures ancrees (App-1b-NQueens, Search-03d-WeightedAstar) #17215, Add: densite Search — 8 lectures ancrees (Search-05) + 2 interpretations reecrites (App-26) (See #13410) #17227, Add(ci,#17397): audit des besoins locaux des jobs self-hosted — 51 sur-accusations mesurees #17403, fix(ci): installer pytest dans les 5 gardes qui l'invoquent sans le declarer #17414... echouaient sur ce test via le meme mecanisme --all.
• Joint restant, hors scope de ce PR : quand feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370 (matrix axiom pass) mergera et supprimera reellement lean-serre.yml, la couverture passera par des appels matriciels templates (project-path: ${{ matrix.* }}) que le scanner ne resout pas litteralement — le checker devra alors lire les entrees de matrice pour prouver la recouverture. Signale, pas implemente ici (la forme finale de l'appel n'est pas encore mergee).
• Aucune collision : feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370 (po-2026) et feat(ci,#17097): mesure stable de la couverture proof-integrity des workflows Lean #17270 (po-2023) ne touchent pas ces deux fichiers (verifie via files list des deux PRs).

🤖 Generated with Claude Code

[github-actions]

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

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

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]

Trivial-diff advisory (#15740, non bloquant).
genre guard dans la famille META (docs/guard/ledger/readme/test) + diff de 82 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17440
head: f99ecff
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8119e9cb24a9761ad95a8f0ad2539edc65b8b52ffccc286235adf7f69c31ffa8
diff-files: 2
diff-additions: 73
diff-deletions: 9
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Notes du rédacteur (hors bloc, pour le lecteur humain) :

• Dossier écrit sur instruction explicite du coordinateur ai-01:CoursIA (msg-20260922T182323-6b2lua, HOLD levé), en tierce partie — la porteuse est myia-po-2025:CoursIA (tag Grain: du body).
• État exact des checks au head au moment du stamp : Scripts Tests (CPU) = success (le faux rouge déterministe de main 35753750580 est réparé par ce diff : partition fail-closed lost/relocated/never, test de non-régression observé vert au head). Seul non-vert : PR gate = DWELL — un plancher temporel, pas un défaut (« Rien a corriger dans le code : cette jambe est un minuteur », écoulement à 2026-09-22T20:07:00Z), re-run annoncé par le coordinateur après écoulement. Le claim checks: latest-wins-green est validé à l'évaluation (gate(prevalidation): statusCheckRollup dans surfaces-sha256 — un check qui verdit perime le dossier, course ingagnable #16957) : avant le re-run, la gate refuse ce dossier en nommant PR gate — comportement attendu, fail-closed ; après le re-run, il s'encaisse.
• Les 2 commentaires comptés sont des advisories github-actions[bot] (genre signals [variation] Le cap LIGHT lit des tiers auto-declares : plafonner sur le GENRE + detecter GENRE-RUN / TIER-INFLATION #10020, trivial-diff ci: un organe advisory qui rougit sur la TRIVIALITE d'un diff, pas sur sa taille (2e moitie du concern user sur #15724) #15740), non bloquants, aucune réserve.

— Hermes, siège myia-po-2026:CoursIA-3

[jsboige]

Diagnostic du rerun PR gate (run 35761190584, relance isolee 18:46Z) : settled: 15 check(s) green — l unique jambe rouge est DWELL (tete 17:30:14Z, 77 min, plancher 120, ecoule a 20:07:00Z). Ce n est pas un defaut de la PR : minuteur documente du gate, leve par le balayage pr-gate-stale-sweep ou un rerun apres 20:07Z. Le fix lui-meme est valide en CI au head f99ecff (Scripts Tests success, guards verts). La candidate est prete pour merge apres ecoulement (ou label merge-dwell-waived si urgence main).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17440 (fix(lean-ci,#17336): lost_gate soustrait la couverture reprise — deplacer le gate n'est pas le perdre) 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.

• terminal -- feat(ci,#17097): mesurer la couverture du gate d'axiomes par lake — 12 couverts, 17 sans gate, 0 perdu #17150 partage : scripts/lean/check_axiom_gate_coverage.py, scripts/lean/tests/test_check_axiom_gate_coverage.py, recouvrement de chemins 100% -- feat(ci,#17097): mesurer la couverture du gate d'axiomes par lake — 12 couverts, 17 sans gate, 0 perdu #17150 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17440
head: f99ecff
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 156768595dcad726dc044a90e20d8962fed1e2921576055f2c6903047764b20c
diff-files: 2
diff-additions: 73
diff-deletions: 9
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]