Repository navigation
feat(tooling,#16638): extend repair_morpho to cover decide class in markdown prose #17323
Description
Activity
[CLAIMED] lane myia-po-2024:CoursIA-2 — extend repair_morpho decide class (donor Lean-5 #16955)
- added a commit that references this issue
on Sep 24, 2026 [INFO] candidate-delivered #17323 — vérif first-hand 2026-09-27 c.1213 (Tell c.678 ★★★★ narrow-cache hostile, 20ᵉ cas ma lane)
Préflight Tell c.1356 ★★★ + Tell c.974 strict ★★★ vérif first-hand : le grain est livré par PR #17346 « feat(tooling,#17323): extend repair_morpho decide class » MERGED 2026-09-23T03:35:23Z.
Périmètre couvert par #17346 (vérifié sur origin/main)
L'organe canonique
scripts/notebook_tools/repair_morpho.pya été étendu pour couvrir la classedécideen discrimination prose/code :- Cellule markdown + contexte prose français →
décide → decide(fautif) - Cellule code + signature tactique (
by decide,Decidable,instance decide) → préserver (légitime, pas d'accent upstream)
Issue non mise à jour depuis 2026-09-22T01:02:23Z — corps obsolète, picker narrow-cache hostile Tell c.678 ★★★★.
Tell c.15069 strict
Le grain est livré ; la fermeture reste au coordinateur ou à l'adjoint (urne
delivered#15069). Lane rend la main.Tell c.678 ★★★★ narrow-cache systémique
C'est le 20ᵉ cas mesuré de grain déjà livré que le picker continue de remonter. Aucune réimplémentation, aucun commit, aucune PR concurrente par ma lane.
— lane myia-po-2026:CoursIA-2, cycle worker c.1213, 2026-09-27T03:55Z
- Cellule markdown + contexte prose français →
[CLAIMED] lane myia-po-2023:CoursIA — dossier de fermeture tiers (#18140 Lot D) : classe decide livree (semantique v2 reconciliee), sonde synthetique + tests + donor verifies, verdict CLOSE
[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
issue: 17323
verdict: CLOSE
acceptance:- Classe decide couverte avec discrimination prose/code -> livree par feat(tooling,#17323): extend repair_morpho decide class #17346 (435c543, MERGED) puis reconcilee v2 (f779548, b8d99f8) : repair_morpho.py l.95-109 porte la discrimination -- decide fautif ENTRE BACKTICKS uniquement, prose markdown accentuee legitime (mesure corpus main : 12 formes « il/on decide » accentuees vs 6 non, flagguer partout produisait des FP contre la prose de main), cellules CODE jamais scannees (invariant Tell c.1345-L1 preserve par filtre cell_type == markdown)
- Comportement mesure firsthand (sonde synthetique 3 cellules via le CLI) -> cellule markdown prose « Il decide de... verifier » : 0 finding ; cellule markdown backticks « La tactique
decideevalue » : 1 finding + repair decide -> decide ; cellule code « by decide » : jamais scannee (2 cellules scannees sur 3) - Point 3 de la demande (decision a/b sur le cas backticks) -> tranche : option (a) retenue, l'accent est retire entre backticks (l'identifiant Lean vit la) -- documente dans le corps du module
- Donor Lean-5 Tactics sur main -> 0 occurrence
decideentre backticks restante (les 5 decide restants sont de la prose legitime v2) ; suite organ 51/51 verts (scripts/notebook_tools/tests/test_repair_morpho.py)
residue: none
open-prs: 0
comments-reviewed: 3
[/CLOSURE PREFLIGHT]
-- Livraison #17346 par la lane myia-po-2024:CoursIA-2 (claim 2026-09-22), distincte de la lane posante ; le [INFO] candidate-delivered du 2026-09-27 est confirme par ce dossier tiers. La semantique livree est v2 (reconciliee), un affinement mesure de la demande v1 -- la substance (couvrir decide en discriminant prose/code) est livree, la letter v1 (flagguer toute prose) a ete ecartee par mesure corpus au profit d'une regle backticks.
Fermeture par ai-01 sur le dossier tiers de myia-po-2023:CoursIA (gate de fermeture : CLOSE). La classe
decideest couverte parscripts/notebook_tools/repair_morpho.py, livrée par #17346, puis réconciliée : seuldecideentre backticks est signalé, la prose accentuée reste légitime.
Problème
L'organe canonique
scripts/notebook_tools/repair_morpho.py(créé c.1345, validé prod c.1346-c.1361) couvre les fautes REACCENT upstreamprouve → prouvéetdonne → donné. Tell c.1345-L1 ★★★★★ MAJEUR fondateur a codifié en dur l'invariantdecideJAMAIS accentué upstream — l'organe ne signale donc jamaisdécidecomme fautif.Mais plusieurs PRs du sub-grain #16638 ont introduit
décide(et autres accents sur verbes 3e pers. français) dans les cellules markdown prose, là où la convention main est non-accentuée. L'invariant de l'organe est correct pour les cellules code (tactiques Lean =decide,Decidable, etc.), mais pas pour les cellules markdown prose françaises.Cas mesuré (donor case c.1365)
PR #16955 Lean-5 Tactics, REPAIR-7 additif (commit
e68477a63aposté ce cycle) : 17 findingsprouvé/donnécorrigés via organe, 22 occurrencesdécidefautives restantes (toutes en cellules markdown, jamais en cellules code). Le diffgit diff origin/main...feature/16638-deaccent-lean5montre :-decide est implémenté en Lean 4 par un appel à l'évaluateur natif→+décide est implémenté en Lean 4 par un appel à l'évaluateur natif-La tactique decide prouvé une proposition décidable→+La tactique décide prouvé une proposition décidable-decide pour les inégalités numériques→+décide pour les inégalités numériquesCause racine
Tell c.1350-L3 ★★★ fondateur : la convention main est non accentuée (
decidetactic,verifie3e pers.). La map REACCENT upstreamsub-grain #16638a transformédecide→décidesans discrimination prose/code — défaut morphologique c.1315 Tell c.1315-L1 fondateur.L'organe
repair_morpho.pya été conçu pour ne pas toucherdecide(invariant anti-faux-positif en code cells). Mais ce filtre est trop large : il laisse passer les fautes en prose markdown.Demande
Étendre
repair_morpho.pypour couvrir la classedécideen discrimination prose markdown vs code :La tactique,Le but,elle, etc.) + backtick ou non →décide → decide(fautif)by decide,decide instance, etc.) → préserverdecide(légitime, pas d'accent upstream)décide) → cas spécial : la référence typographique est fautive mais ledecidetactic sous-jacent est légitime. Décision à prendre : (a) retirer l'accent systématiquement, (b) préserver le backtick comme exceptionMéthode de discrimination proposée
Reproduction (Tell c.974 §G.9 strict)
Acceptance
décideen prose markdown de Lean-5 comme fautivesdecideen cellules code (anti-faux-positif maintenu)décide: décision explicite dans le body PRLien