ci(lean): cabler le gate proof-integrity sur les 13 lakes matriciels qui n'en portent pas

Contexte mesuré

python scripts/lean/check_axiom_gate_coverage.py --json rend, à la tête de
main du 2026-10-25 :

verdict	total
`gated_lakes` (le gate d'axiomes atteint le lake)	23
`matrix_lakes` (lakes servis par `lean-ci-matrix.yml`)	27
`matrix_lakes_without_gate`	13
`lost_gate` (un gate a existé puis a disparu)	0

Les 13 lakes concernés :

MyIA.AI.Notebooks/GameTheory/SocialChoice/social_choice_lean_peters
MyIA.AI.Notebooks/GameTheory/conway_cgt_lean
MyIA.AI.Notebooks/GameTheory/lean_game_defs
MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext
MyIA.AI.Notebooks/IIT/iit_lean
MyIA.AI.Notebooks/ML/learning_theory_lean
MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean
MyIA.AI.Notebooks/Search/discrepancy_lean
MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean
MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples
MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean
MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean
MyIA.AI.Notebooks/SymbolicAI/Tweety/argumentation_lean

Mécanisme

scripts/lean/ci_lakes.json porte, par lake, une clé optionnelle
axiom-target-modules. Dans lean-build.yml, le step Proof integrity est
gardé par if: matrix.axiom-target-modules != ''. Une entrée sans la clé
s'interpole en chaîne vide et le step est sauté — sans rouge, sans
avertissement : le check-run lean-matrix / Lean CI (<lake>) peut être vert
alors qu'aucun axiome du module modifié n'a été examiné.

C'est le cas (b) de la règle B.3 de pr-review-discipline.md : un vert
hors-cible est indiscernable d'un vert sur cible. Un exemple mesuré cette
semaine : lean_game_defs_ext reçoit Bayesian/VoiBench.lean (11 nouvelles
ancres) sans que le gate voie le fichier ; la PR #22515 le déclare dans son body
plutôt que d'invoquer un vert qui ne dit rien.

Ce qui est demandé

Ce n'est pas d'ajouter la clé partout. L'organe le dit lui-même : « un lake
sans gate d'axiomes n'est pas illicite, il doit seulement être connu comme tel »
(#17097, critère 3). Ce qui manque, c'est la décision par lake, écrite.

Pour chacun des 13 :

soit la clé axiom-target-modules est ajoutée — "*" quand le lake est
petit ou sans dépendance croisée (la liste des modules est alors dérivée à
l'exécution), une énumération explicite quand le coût du pass complet est
prohibitif ou quand le lake porte des axiomes légitimes à whitelister ;
soit le lake reste sans gate, et la raison est écrite dans
docs/reference/lean-axiom-coverage.md à côté de la mesure.

Dans les deux cas, le résultat est vérifiable par l'organe : après la tranche,
un lake sans gate doit avoir une ligne de justification, pas un silence.

Acceptance

Les 13 lakes sont tranchés un par un (clé ajoutée, ou justification écrite).
python scripts/lean/check_axiom_gate_coverage.py --json ne rend plus
aucun lake dans matrix_lakes_without_gate sans justification
correspondante dans la doc de référence.
Sur au moins un lake câblé, un run de lean-ci-matrix.yml montre le step
Proof integrity exécuté (pas sauté) et vert à une tête qui touche un
module du lake.
Aucun lake ne régresse : lost_gate reste à 0.

Provenance

Part of #17097 — l'umbrella de mesure de la couverture d'axiomes, close
depuis. Ceci en est la suite opérationnelle : la mesure existe et elle est
maintenue par l'organe ; ce qui n'existait pas, c'est la décision par lake.

Signalé depuis #22515 (grain DEEP/lean, lane myia-ai-01:CoursIA-2), où la
clause 8 de l'acceptance demande explicitement de vérifier si la CI d'intégrité
atteint les nouveaux modules.

[CLAIMED] lane myia-po-2028:CoursIA-2 -- tranche par lake : cle axiom-target-modules ou justification ecrite, + verification par l'organe

paths: scripts/lean/ci_lakes.json, docs/reference/lean-axiom-coverage.md, scripts/lean/check_axiom_gate_coverage.py, .github/workflows/lean-build.yml -- 2026-10-27T22:30Z

[CLAIMED-AMEND] lane myia-po-2028:CoursIA-2 -- paths: scripts/lean/ci_lakes.json, docs/reference/lean-axiom-coverage.md, scripts/lean/check_axiom_gate_coverage.py, scripts/lean/tests/test_check_axiom_gate_coverage.py -- 2026-10-27T23:10Z

Le claim de dispatch listait trois fichiers de code et .github/workflows/lean-build.yml. Deux corrections, mesurees sur le diff reel :

ajout de scripts/lean/tests/test_check_axiom_gate_coverage.py : le cliquet --strict livré sans test serait un cliquet qu'on peut debrancher sans le voir. 8 tests ajoutes (justification par ligne, non-propagation a un lake voisin, --strict rouge sur un lake non justifie, retro-compatibilite du contrat --check seul) ;
retrait de .github/workflows/lean-build.yml : la mesure a montre que le composite y transmet deja axiom-fail-on-sorry: ${{ matrix.axiom-fail-on-sorry || 'true' }} (ligne 395) ; aucune modification du workflow n'est necessaire, la decision se porte entierement dans le manifeste.

Fix(ci,#22519): nommer l'axiome `arrow_impossibility` et retirer les …

Fix(ci,#22519): decider deux lakes SANS gate plutot que les cabler a …

Fix(lean,#22519): globber les modules racines Perceptron et PacLearning

[DELIVERED] lane myia-po-2028:CoursIA-2 -- PR #23019

Preuve par critère, mesurée à la tête a0adf91fb (28/10 ~02:40Z) :

11 lakes câblés au gate d'axiomes : la matrice lean-matrix / Lean CI (<lake>) rend 26/26 success sur la tête, dont les 5 jambes qui étaient en vol au cycle précédent (sensitivity_lean 01:24Z, social_choice_lean_peters 01:29Z, learning_theory_lean 01:24Z, sudoku_lean 01:22Z, tegmark_muh_lean 01:39Z) et argumentation_lean (01:41Z, contrôle positif du câblage). Le rouge learning_theory_lean du head précédent est résolu par le fix a0adf91fb (glob nu des racines Perceptron/PacLearning dans le lakefile — diagnostic c.6457388805) : la jambe est verte à la nouvelle tête.
2 lakes décidés SANS gate (conway_cgt_lean, mathlib_examples) : les deux jobs sont success et, mesuré au head précédent avec contrôle positif (argumentation_lean porte bien les steps), ils ne portent aucun step de gate d'axiomes — la justification écrite est au §4.1 du doc de la PR ; check_axiom_gate_coverage.py --ref HEAD --check --strict rc=0 (2 sans gate, 0 injustifié), contrôle négatif --ref origin/main rc=1 (13 injustifiés).
Rouge résiduel PR gate = agrégat périmé, rejoué : la tentative cancelled de 00:31Z avait démarré avant la relance matricielle de 00:44Z — elle a plié l'état d'alors, pas un verdict de contenu (la lecture des check-runs nominatifs montre 60 success / 5 skipped / 2 neutral advisory, 0 rouge de substance). Rerun du run porteur 40609241992 effectué (rc=0, aucun commit, plancher DWELL non ré-armé) ; le verdict d'agrégat se lit au cycle suivant.

La clôture de l'issue est un geste coordinateur/adjoint.

Fix(lean,#22519): matcher de justification delimite (anti-prefixe, an…

Merge branch 'main' into feature/22519-axiom-gate-matrix -- conflit d…

ci(lean,#22519): cabler le gate proof-integrity sur les 13 lakes matr…

Merge origin/main into feat/lean-mimo-matrix

Add(guard,#23046): armement du cliquet axiom-gate dans les gardes alw…

Fix(ci,#18038): le census distingue un lake sans declaration d'un cab…

Fix(ci,#18038): le census ne compte plus un lake sans declaration com…

Navigation Menu

Repository navigation

ci(lean): cabler le gate proof-integrity sur les 13 lakes matriciels qui n'en portent pas #22519

Contexte mesuré

Mécanisme

Ce qui est demandé

Acceptance

Provenance

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

ci(lean): cabler le gate proof-integrity sur les 13 lakes matriciels qui n'en portent pas #22519

Description

Contexte mesuré

Mécanisme

Ce qui est demandé

Acceptance

Provenance

Activity

jsboige commented on Oct 27, 2026

jsboige commented on Oct 27, 2026

jsboige commented on Oct 28, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions