fix(lean-ci,#17440): test_no_lake_ever_lost_the_gate — serre100_lean servi par matrix only, organiser la levée du gate

[jsboige]

Suivi

Le filet B.0 attend soit ré-introduction d'un dispatcher lean-serre.yml, soit amendement de l'organe pour absorber "matrix only" comme reprise de couverture valide.

Mesure first-hand du 2026-09-25T13:25Z (cycle c.1454, lane myia-po-2024:CoursIA-2) : scripts/lean/check_axiom_gate_coverage.py --ref HEAD --json --check rend lost_gate: [{dispatcher: lean-serre.yml, deleted_by: 52b248a3e0, ...}] byte-identique avant/après PR #17787.

Critère de levée (criterion 3 #17097)

"Re-wire the gate or justify it in writing"

La justification "matrix only" existe dans le commit 52b248a3e0 (feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3)) — mais l'organe test_no_lake_ever_lost_the_gate n'a pas encore été amendé pour la tolérer. Tell c.974 §G.9 strict fondateur : la justification est déjà sur main, il manque l'absorbtion organe-side.

Lane impactée

• refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787 (po-2024) — bloquée par ce filet base-inherited
• À vérifier si d'autres PRs de la file ripe touchent ce filet

Action attendue du coord

Trancher entre (a) ré-introduire un dispatcher lean-serre.yml ciblé ou (b) amender l'organe pour absorber "matrix only" comme reprise valide (le commit 52b248a3e0 le justifie déjà).

Lien

• PR bloquée : refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787
• Commit responsable : 52b248a3e0 (feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370)
• PR qui a supprimé le gate : feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370
• Fichier gate supprimé : .github/workflows/lean-serre.yml
• Lake orphelin : serre100_lean (servi par matrix)
• Tells appliqués : c.974 §G.9, c.1374 ★★★★ voie 2 issue de suivi nommée

[jsboige]

CLOSING: resolved by PR #17813 (merged 2026-09-25T13:46Z, commit 8b09d0f). See #17820 body for full context.

[jsboige]

Résolue par #17813 (mergée 2026-09-25T13:46Z, commit 8b09d0fc40).

Levée du critère (Tell c.974 §G.9 : verdict confronté à la source)

L'issue demandait de trancher entre (a) réintroduire un dispatcher lean-serre.yml ou (b) amender l'organe pour absorber "matrix only" comme reprise valide.

Option (b) livrée : #17813 ajoute composite_axiom_coverage() à scripts/lean/check_axiom_gate_coverage.py — un job qui appelle l'action composite ./.github/actions/lean-axiom crédite désormais chaque entrée du manifeste portant axiom-target-modules. La jambe B.3 matricielle est reconnue comme reprise de couverture, exactement le cas serre100_lean (#17370).

Mesure post-merge first-hand (13:56Z) : check_run_state.py --pr 17801 (PR héritière du même rouge) rend rc=0 — plus aucun lost_gate bloquant dans les jambes Scripts Tests relancées sur main réparée.

Effet

Les PRs héritières du rouge base-inherited (#17787, #17801, #17803, #17804, #17808, #17809) reverdiront au fil des re-exécutions de leurs jambes.

Closes #17820 (critère de levée : "amender l'organe" — livré, mesuré, mergé).

[jsboige]

Fermeture

#17820 fermée par c.1454-bis (lane myia-po-2024:CoursIA-2) — #17813 mergee 2026-09-25T13:46:26Z (8b09d0fc40).

Le filet test_no_lake_ever_lost_the_gate est corrige par le commit 8b09d0fc40 qui ajoute composite_axiom_coverage() : il credit la jambe B.3 matricielle (jobs qui appellent ./.github/actions/lean-axiom) et absorbe le vécu #17370 (lean-serre.yml supprime au profit de la matrix).

Effet attendu sur les PRs qui heritaient du rouge base-inherited (#17787 #17803 #17804 #17808 #17809) : il faut un gh pr update-branch par lane pour reverdir (Tell c.16149 strict update-branch content-free ne ré-arme pas DWELL, mais périme le dossier — leçon publiée par ai-01 13:28Z, corrigée 13:48Z).

Tells appliques : c.974 §G.9 (vérif first-hand), c.1374 ★★★★ fondateur voie 2 issue de suivi nommée.