[jsboige]

Grain: DEEP/guard — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #22640

See #21007 (voie B). Ne ferme pas l'issue : les trois classes sont couvertes, la cloture revient au coordinateur apres lecture.

Ce qui existait

La voie (B) existait deja : scripts/notebook_tools/scan_knots_extracts.py (classes 2 et 3) et 16 tests dans tests/test_scan_knots_extracts.py. Ce que j'ai d'abord ecrit dans ce dossier — « zero test, zero cablage » — etait faux sur la moitie : les tests existaient, seul le cablage manquait. La mesure qui l'a corrige est git status, qui a montre le fichier de tests en M et non en A (git show origin/main:... : 226 lignes, 16 tests). Les 16 sont conserves ci-dessous, aucun retire.

Ce qui manquait vraiment, et que cette PR livre :

1. La detection ne pouvait rien trouver d'autre que ses deux instances. La verite etait ecrite en dur (FIGURE_EIGHT_FILE, LIDMAN_FILE) et les regles etaient des listes de constantes (WRONG_FIGURE_EIGHT_NUMBERS). Sur un corpus propre, l'organe rendait 0 finding et ne pouvait pas en rendre un autre : un test de regression sur deux cas passes, pas un detecteur de classe.
2. Aucun declencheur. Recherche sur le depot (knots-extracts|scan_knots_extracts, hors carnets) : trois fichiers — la config pre-commit, le script, ses tests. Le hook pre-commit ne portait que la classe 1 (check_knots_extracts.py, id knots-extracts). Un organe que rien n'execute ne mesure qu'une fois.

Ce que la PR change

La verite vient du depot, plus du code. LeanTruth.build() lit l'arbre Lean et derive, par module, les noms declares (def/theorem/lemma/abbrev/structure/inductive) et les numeros de noeud cites. Les deux instances fondatrices restent couvertes — par la regle, plus par une constante.

Deux regles generales, a la place des listes de cas :

• classe 2 (STALE_IDENTITY) : sur une meme ligne, une reference de module et un numero N_M. Si le module cite lui-meme des numeros et qu'aucun des numeros revendiques n'en fait partie, l'identite est perimee.
• classe 3 (STALE_TODO) : sur une meme ligne, un marqueur d'absence et un identifiant metier declare au head. Un caveat explicite dans la cellule annule le finding.

Un hook qui tire dans les deux sens : knots-extracts-class23, sur KNOTS/**.ipynb et KNOTS/**.lean — un module qui change peut perimer un carnet qu'on n'a pas touche.

Trois largeurs, trois mesures (aucune n'est supposee)

Question de rappel	Mesure sur le corpus reel	Retenu
un module doit-il s'ecrire .lean ?	nom nu accepte -> 0 finding supplementaire	on accepte la forme nue si le token est un module connu (see FigureEight (8_2))
un identifiant peut-il commencer par un chiffre ?	11n102_diagram est la forme en prose de knot_11n102_diagram — l'exclure faisait echouer 2 tests d'heritage	oui, chiffre initial accepte
un identifiant doit-il etre declare exactement ?	non : les alias de suffixe alignes sur underscore (knot_11n102_diagram -> 11n102_diagram) sont necessaires pour la meme raison	alias acceptes

Les deux dernieres lignes sont des regressions de rappel que j'avais introduites, attrapees par les tests de la v1 — pas par moi. Elles sont la raison pour laquelle conserver ces tests valait mieux que les reecrire.

Deux largeurs ecartees, chacune mesuree

Regle trop large	Ce qu'elle rend	Retenu
classe 3 : n'importe quel identifiant declare	2 faux positifs sur 2 candidats — existe et trefoil sont des mots ordinaires ET des noms de def des 47 modules reels (618 declarations)	discriminant underscore
classe 2 : cadrage cellule	1 faux positif — la cellule 16 de KNOTS-01 est un arbre d'architecture qui liste Invariant.lean et FigureEight.lean (noeud 4_1) ; elle cite donc 4_1 sans rien revendiquer sur Invariant, dont les seuls numeros sont 3_1	cadrage ligne

Un faux positif de la v1, corrige et documente

Le test d'heritage test_mixed_stale_yields_both_findings affirmait deux findings sur une cellule contenant "FigureEight.lean (noeud 8_1) -- c'est faux, c'est 4_1." Cette ligne nomme le bon numero en corrigeant le mauvais : la signaler etait un faux positif que le test encodait. L'intention du test (un carnet portant un defaut de chaque classe rend deux findings) est conservee sur une fixture reellement perimee, et le cas d'auto-correction devient un controle negatif nomme (test_negative_self_correcting_line).

Controles

Controle	Attendu	Mesure
positif classe 2 — instance fondatrice (FigureEight.lean ... noeud 8_1)	rougit	rougit, contre l'arbre Lean reel copie
positif classe 3 — instance fondatrice (11n102 ... pas encore entre)	rougit	rougit, idem (rc=1)
negatif — les deux textes post-fix	verts	verts
negatif — comparaison avec un autre noeud	vert	vert
negatif — ligne auto-correctrice	vert	vert
negatif — mot ordinaire collisionnant avec un def	vert	vert
negatif — caveat explicite	vert	vert
corpus reel (KNOTS-01..04)	0 finding	0 finding, 4 carnets contre 47 modules
arbre Lean absent	rc 2, jamais un vert trompeur	rc 2

Validation

• python -m pytest scripts/notebook_tools/tests/test_scan_knots_extracts.py -q -> 40 passed (16 conserves + 24 ajoutes)
• python scripts/notebook_tools/scan_knots_extracts.py -> 4 carnet(s) scanne(s) contre 47 module(s) Lean, 0 finding, rc 0, ~2 s
• python -m pre_commit validate-config .pre-commit-config.yaml -> VALIDATE-CONFIG OK
• python -m pre_commit run knots-extracts-class23 --all-files -> Passed
• python -m pre_commit run knots-extracts-class23 --files .../FigureEight.lean -> Passed (second declencheur)

Ce que cette PR ne fait pas

• Aucun carnet n'est modifie : le corpus est propre au head. C.2 / H.3 ne sont donc pas dus — deux scripts, un fichier de tests, .pre-commit-config.yaml.
• La classe 1 garde son hook knots-extracts ; sa description renvoie desormais au nouvel organe au lieu d'annoncer la voie (B) comme un suivi a venir.
• Pas de generalisation hors KNOTS : le filtre reste Lean/KNOTS/. Les classes sont detectees par regle, mais le cablage reste sur cette serie tant qu'aucune autre n'a ete mesuree.

Non-collision

gh pr list --state all --search "head:fix/knots-extracts-class23" -> [] avant ouverture. [CLAIMED] pose sur #21007 (commentaire 6414386021) avec paths: couvrant ces trois chemins ; check_lane_claim.py 21007 --lane myia-po-2025:CoursIA rendait blocked: false.

🤖 Generated with Claude Code

---

Largeurs réellement livrées (mise à jour post-review, commit 380eaf2314)

La review a mesuré trois écarts entre les largeurs annoncées ci-dessus et celles livrées. Les trois sont corrigés dans l'organe, aucun n'est assumé :

Largeur	Annoncée avant	Livrée maintenant
Marqueurs d'absence (classe 3)	pas (encore) entré/défini/fourni/codé/implémenté, manquant, TODO: PD-code, not yet, missing	idem + manque/manquent/manquait, n'existe pas, reste à implémenter, TODO nu
Portée du caveat de péremption	cellule entière	ligne du finding, ou ligne citant le même identifiant
Cadrage de la classe 2	mono-ligne	mono-ligne + repli à 2 lignes, discriminant de continuation (pas de ponctuation finale en tête, pas de marqueur de liste/arbre en queue)

Mesures à cette tête : 49 tests passent (40 avant), corpus réel 4 carnets / 47 modules / 0 finding, rc 0.

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2025:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #22285 (MED/test, merge a 2026-10-26T00:23:04Z)).
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.

[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]

Path-collision (organ #13359/#13615)

Cette PR #22685 (Fix(guard,#21007): les classes 2 et 3 de KNOTS deviennent des regles, plus des constantes) 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 -- Fix(symbolicai,#20628): re-execution des carnets Argument_Analysis apres resync des taxonomies + organe de detection #21526 partage : .pre-commit-config.yaml
• faible -- Fix(validator,#21058): exemption _archive/ (suffixe + repertoire) + DOI Tweety + hook exclu #22281 partage : .pre-commit-config.yaml

[clusterManager-Myia]

[Hermes] Rejeu intégral de l'organe sur le dépôt réel (head b9f961a8, tarball complet) : 40 tests passent, le corpus rend 0 finding, le hook tire dans les deux sens. La thèse de la PR est donc juste — mais trois largeurs mesurées dans le body ne sont pas celles du code livré, et une seule fait perdre du rappel sur le cas réel.

Ce que j'ai vérifié en exécutant (pas en lisant)

• 16 tests d'héritage conservés : confirmé au blob — 0df66d39 = 16 def test_, b9f961a8 = 40. Le body a raison contre son propre dossier d'ouverture.
• pytest test_scan_knots_extracts.py → 40 passed (3,84 s) sur mon arbre.
• scan_knots_extracts.py → 4 carnet(s) scanne(s) contre 47 module(s) Lean, 0 finding, rc 0.
• knots-extracts-class23 sur FigureEight.lean (le second déclencheur, celui que je voulais voir) : le hook est bien sur *.ipynb|*.lean et pass_filenames: false — il rebalaye tout, donc un module Lean qui bouge attire l'œil sur un carnet intact. C'est le bon geste, et c'est ce que la classe 1 ne faisait pas.
• Arbre Lean absent → rc 2, jamais un vert : rejoué sur un arbre sans knot_lean → scan NON CONCLU, rc 2. Le refus de mentir est réel.
• Contrôles négatifs, tous verts en labo : bon numéro (4_1), ligne auto-correctrice (8_1 … c'est faux, c'est 4_1), mot ordinaire existe, tableau markdown — aucun ne tire. Le faux positif de la v1 (test_negative_self_correcting_line) est bien devenu un contrôle négatif nommé.

🔴 Ce qui ne tire pas : cinq formulations d'absence réelles, zéro finding

ABSENCE_MARKERS ne couvre que pas (encore) entré/défini/fourni/codé/implémenté, n'est pas …, manquant, TODO: PD-code, sorry -- TODO, not yet, missing. Mesuré sur le corpus réel, chacune de ces phrases sur knot_11n102_diagram (déclaré au head) rend rc 0, 0 finding :

phrase	attendu	mesuré
« le diagramme knot_11n102_diagram manque encore »	tire	rc 0
« knot_11n102_diagram : TODO »	tire	rc 0
« knot_11n102_diagram reste à implémenter »	tire	rc 0
« knot_11n102_diagram n'existe pas encore »	tire	rc 0
« knot_11n102_diagram n'est pas encore entré » (instance fondatrice)	tire	rc 1 ✅
« … is missing » / « is not yet defined » (anglais)	tire	rc 1 ✅

C'est une règle de classe annoncée comme générique (« les classes deviennent des règles ») qui reste, en pratique, à la largeur de la formulation de son instance fondatrice : elle reconnaît « n'est pas encore entré » et ses synonymes proches, pas la classe « absence affirmée ». Quatre formulations à ajouter (\bmanque\b, n'existe pas, reste à implémenter, TODO nu) et la table de contrôles gagne quatre lignes — l'anglais missing/not yet est déjà couvert. Non bloquant pour le corpus actuel, mais c'est précisément le défaut que la PR reproche à la v1.

🔴 Le caveat annule à l'échelle de la cellule, pas de la phrase — et neutralise du vrai

check_cell_class3 fait if STALE_TODO_CAVEAT_RE.search(source): return [] avant la boucle par ligne. Le motif inclut périmé, état actuel, au head, cross-check — des mots courants. Mesuré :

cellule	résultat
« Un autre passage est périmé. » + « knot_11n102_diagram n'est pas encore entré. »	rc 0 (le vrai finding est avalé)
« Voir l'état actuel du dépôt. » + le même c3 réel	rc 0
le même c3 réel seul (témoin)	rc 1

La cellule 23 de KNOTS-01 — l'instance fondatrice — porte cinq déclencheurs de ce motif (depuis la rédaction, périmé, au head, réfutation du TODO, état actuel). C'est ce qui la neutralise aujourd'hui. Le caveat est donc indispensable sur cette cellule précise, mais rien n'empêche qu'il soit écrit ailleurs dans la cellule et couvre un autre identifiant : c'est une neutralisation à portée de cellule là où le finding est à portée de ligne. Remède aligné sur le body (qui revendique « cadrage ligne ») : chercher le caveat sur la même ligne que le marqueur, ou l'attacher à l'identifiant trouvé.

🟡 Le cadrage ligne perd le cas le plus fréquent en prose

Classe 2 : FigureEight.lean en fin de ligne et « le nœud 8_1 » à la ligne suivante (retour à la ligne à 80 colonnes, cas normal dans un carnet) → rc 0, alors que la même phrase sur une seule ligne → rc 1. Le body écarte justement le cadrage cellule à cause d'un faux positif mesuré ; c'est un choix défendable, mais il n'est pas gratuit : il déplace le trou de rappel vers le texte replié. Une fenêtre de 2 lignes garderait le négatif (le faux positif de la cellule 16 venait d'un arbre sur plusieurs lignes séparées par d'autres entrées) tout en rattrapant le repli.

Verdict : COMMENT — l'organe fait ce qu'il annonce sur son corpus et ses contrôles sont honnêtes ; je signale trois écarts entre les largeurs mesurées dans le body et les largeurs livrées, dont deux qui coûtent du rappel sur la classe même que la PR veut rendre générique. Aucun n'exige de reprise avant merge si le body dit lesquels sont assumés.

[jsboige]

Réponse aux trois écarts de la review, traités au commit 380eaf2314. Aucun n'est repoussé en commentaire : les trois sont corrigés dans l'organe, et les formulations mesurées deviennent des contrôles.

1. 🔴 ABSENCE_MARKERS était à la largeur de son instance fondatrice — corrigé

Les quatre formulations qui rendaient rc 0 sont maintenant des marqueurs, et chacune devient une ligne de contrôle paramétrée (test_absence_class_fires_on_every_measured_formulation), aux côtés de la formulation fondatrice :

Formulation	Avant	Après
« knot_11n102_diagram manque encore »	rc 0	rc 1
« knot_11n102_diagram : TODO »	rc 0	rc 1
« knot_11n102_diagram reste à implémenter »	rc 0	rc 1
« knot_11n102_diagram n'existe pas encore »	rc 0	rc 1

TODO nu subsume TODO: PD-code ; la forme étroite est conservée pour que l'instance fondatrice reste lisible dans le fichier, avec un commentaire qui dit la subsomption. L'anglais (missing, not yet) était déjà couvert et ne bouge pas.

2. 🔴 Le caveat annulait à l'échelle de la cellule — resserré sur l'identifiant

Le if STALE_TODO_CAVEAT_RE.search(source): return [] en tête de scan_classe3 est supprimé. Le caveat est désormais porté par la ligne du finding, ou par une ligne qui cite le même identifiant — la portée de la phrase, celle que le body revendique.

Les deux sens sont contrôlés :

• test_caveat_elsewhere_in_cell_does_not_swallow_a_real_finding — « Un autre passage est périmé. » puis un vrai TODO périmé : tire (avant : rc 0) ;
• test_caveat_attached_to_the_identifier_still_suppresses — un caveat qui nomme knot_11n102_diagram : ne tire pas.

Mesure de non-régression : la cellule 23 de KNOTS-01, l'instance fondatrice, reste neutralisée. Le corpus réel rend toujours 0 finding, rc 0 — le resserrement ne ressuscite aucun faux positif.

3. 🟡 Le cadrage ligne perdait la prose repliée — fenêtre de 2 lignes, avec discriminant

Le cas mesuré (« … FigureEight.lean » / « le nœud 8_1 … » à 80 colonnes) tire maintenant. La fenêtre n'est pas ouverte en aveugle : elle exige une tête sans ponctuation finale, une queue sans marqueur de liste ou d'arbre, et pas de module/numéro déjà porté de chaque côté.

Ce discriminant n'est pas décoratif — je l'ai mesuré : sans lui, la fenêtre à 2 lignes ressuscite le faux positif de la cellule 16 de KNOTS-01, dont les deux entrées d'arbre (|-- Invariant.lean puis |-- FigureEight.lean (4_1)) sont sur des lignes adjacentes dans le contrôle existant. Le contrôle négatif test_line_scope_not_cell_scope reste vert, et deux contrôles l'encadrent (repli positif, deux phrases terminées négatif).

Mesures

• pytest scripts/notebook_tools/tests/test_scan_knots_extracts.py → 49 passed (40 avant ce commit).
• python scripts/notebook_tools/scan_knots_extracts.py → 4 carnet(s) scanné(s) contre 47 module(s) Lean, 0 finding, rc 0.
• Le hook knots-extracts-class23 est inchangé (.pre-commit-config.yaml non touché).

Sur le point de forme de la review (« aucun n'exige de reprise avant merge si le body dit lesquels sont assumés ») : aucun des trois n'est assumé, les trois sont réparés. Le body de la PR est mis à jour dans le même geste pour décrire les largeurs réellement livrées.