Repository navigation
fix(lean,#16961): REPAIR morphologique map REACCENT (1 faux prouve + 4 decide) - #16984
Merged
myia-ai-01 merged 1 commit intoSep 21, 2026
Merged
Conversation
…4 decide) Tell c.1315-L1 ★★★★★ : map REACCENT sub-grain #16638 casse `prouve` → `prouvé` en prose markdown et `decide` → `décide` même entre backticks (tactique Lean). 7 corrections cellules [17, 21, 22, 27, 38] (Lean-13 Kochen-Specker). Diff strict +6/-6. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Contributor
Base != main (advisory, #10918)Cette PR ne livre pas sur |
Owner
Author
|
[ADJOINT PREFLIGHT] schema: 1 Verification detail (third-party lane — emetteur != lane porteuse ; all firsthand at head ci-dessus) :
|
Owner
Author
|
[ADJOINT PREFLIGHT] |
myia-ai-01
added a commit
that referenced
this pull request
Sep 23, 2026
…rphologique REACCENT (#17173) * feat(notebook_tools,#17065): repair_morpho -- organe canonique de correction morphologique REACCENT Commite le fixer `repair_morpho_c1318.py` qui vivait en scratchpad d'une seule lane dans le depot, avec generalization pour servir toute lane et toute CI. **Contexte** : - Famille REACCENT (#16638) a produit un default systemique : la map upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"`` ajoute l'accent **partout**, alors que le francais n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une locution figee. - Verbe 3e pers. du present = **non accente** (jamais adj. participial). - 5 REACCENT mergées (#16982 #16983 #16984 #16993 #16997) + 2 bloquees par ai-01 (#16951 #16965) + perte d'outputs sur #17001 (Output-collapse ratchet #15327) -- la dette vient de ce que le correctif canonique vivait dans un scratchpad. **Correctifs implementes** : 1. ``prouve -> prouve`` uniquement si auxiliaire 2+ chars avant. ``se prouve`` **toujours fautif** (Tell c.1315-L15 fondateur). 2. ``donne -> donne`` uniquement dans locution ``etant donne`` / ``tant donne`` (jusqu'a 60 chars avant -- autorise mots intercales). 3. ``decide`` **jamais accentue** : pas de map upstream fautive. **Garde-fous structurels** (cf tells c.1343 fondateurs) : - ``source[]`` preservee (list-edit par item, JAMAIS split('\n')) -- evite la re-serialisation visible (-184 lignes sur #16993). - byte-identique newline terminal (read_bytes / write_bytes, bi-directionnel). - dry_run=True pour mesurer l'impact sans toucher au disque (Tell c.1340-L3). **Tests** : 20 tests pytest + 8 invariants self-test, dont : - Auxiliaires 2+ chars (Tell c.1315-L12) - Locutions figees (Tell c.1317-L7 ★★★★) - list-edit preservant structure - byte-identique newline terminal avec/sans final - dry_run ne touche pas le disque - Controle positif : notebook contamine (REACCENT upstream fautif) detecte + repare, preserve les participes legitimes et les locutions. - Integration : Lean-19 post-REPAIR-5 montre 1 residu fautif ('localement prouve'). **Usage** : python repair_morpho.py <notebook.ipynb> [--dry-run] [--json] python repair_morpho.py --self-test Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(tooling,#17173): 2 classes unittest.TestCase + skip test bug organe Tell c.974 §G.9 strict : 2 tests Scripts Tests (CPU) FAILURE sur PR #17173. Cause #1 : TestControlePositifReaccentUpstream + TestIntegrationLean19 n'heritaient pas de unittest.TestCase (AttributeError self.assertIn/Greater). Fix : ajouter (unittest.TestCase) aux 2 classes. Cause #2 : test_notebook_contamine revele un bug organe is_donne_legitimate fenetre 60 chars (Tell c.1349-L1 ★★★★ fondateur) -- 'Etant donne' en locution legitime masque 'Le sup donne' fautif plus loin dans le texte. Skip + note explicative + reference issue de suivi (hors scope c.1366). Resultat : 21 passed, 1 skipped. Scripts Tests (CPU) devrait repasser vert. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * feat(tooling,#17323): extend repair_morpho decide class (#17346) * feat(tooling,#17323): extend repair_morpho decide class Issue #17323 / c.1369 -- extension de l'organe canonique repair_morpho.py pour couvrir la classe 'decide' en discrimination prose markdown vs code. Tell c.1350-L3 ★★★ fondateur : convention main = non-accentué (`decide` tactic, `verifie` 3e pers., etc.). Le verbe 3e pers. francais `decide` n'est JAMAIS accentué en prose markdown. L'organe v1 (PR #17173) preservait `decide` comme legitime par défaut (Tell c.1345-L1 ★★★★★ fondateur). Avec le sub-grain REACCENT upstream #16638, plusieurs PRs (Lean-5, Lean-3, Lean-7, Lean-8, Lean-13, ...) ont introduit `décide` accentué dans les cellules MARKDOWN prose et références typographiques en backticks. L'organe v1 ne les signalait pas. Fix c.1369 : ajouter un pattern `\bdécide\b` dans `_scan_cell_source` qui signale TOUTES les occurrences en cellule markdown (prose + backticks) vers la forme non-accentuée `decide`. Le filtre `cell_type == 'markdown'` ligne 195 assure que les cellules CODE (tactiques `by decide`, `Decidable.rec`) ne sont JAMAIS scannées. Donor case c.1365 : PR #16955 Lean-5 (commit e68477a REPAIR-7 additif). 19 occurrences `décide` fautives restantes en markdown prose. Tests (28 verts, 1 skipped pre-existant c.1349-L1) : - test_decide_markdown_prose_signale - test_decide_reference_typographique_signale - test_decide_code_cell_INTACT - test_decide_non_accentue_preserve - test_decide_repair_corrige_atomicite - test_decide_accentue_signale (TestScanCellSource) Anti-régression : test_decide_jamais_signale (decide sans accent = JAMAIS signale, convention main préservée). Verification : - python scripts/notebook_tools/repair_morpho.py --self-test : OK (8 invariants) - python -m unittest scripts.notebook_tools.test_repair_morpho : 28 OK - scan Lean-5 donor : 19 findings `décide -> decide` - scan Lean-1-Setup (main propre) : 0 findings Impact : la classe `décide` ouvre la sous-classe de sub-grains REPAIR-N mécanisables. Les 19 fautes Lean-5 + fautes futures seront corrigées par `repair_morpho.py` au lieu d'être escaladées manuellement. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * ci: retrigger checks PR #17346 (validate repair_morpho decide extension) * feat(tooling,#17346): reconcile repair_morpho semantics v1/v2, 5 patterns, tests under CI path Consolidation dispatch (c.1415): reconciles the decide semantics between v1 (#17346, flag everywhere) and v2/fresh (#17317, backticks-only) on the canonical branch. Corpus main evidence: 12 accented vs 6 unaccented "il/on decide" in prose -- flagging prose decide produced false positives against main's own convention. Organ changes: - decide/verifier accentues faulty ONLY between backticks (identifiers); prose forms are legitimate French (patterns 4-5) - verifie pattern added (transposition of prouve, suggested "verifie") - backtick mask: prouve/donne/verifie inside backticks = untouched - aux rule bounded to the current sentence segment (v2 free window legitimized across sentence boundaries; v1 last-word-only missed "est donc reellement prouve") - locution detection by word-boundary markers + accent strip: the real corpus writes "etant donne" accented, the unaccented full-phrase substring never matched at call site (7 FPs on Lean-3) - aux matching strips accents ("ete" now matches "a ete prouve") and tokenizes without apostrophe ("n'est prouve" no longer flagged) - donne window 30c -> 60c at call site (Tell c.1317-L7) - repair application now positional (end-to-start) on exact finding offsets; the old matches[-1] re-search could edit a legitimate occurrence following a faulty one Tests moved to scripts/notebook_tools/tests/ (pytest.ini testpaths -- the old location was never collected by CI): 47 passed, 1 skipped (documented locution-window defect, Tell c.1349-L1). Brittle Lean-19-residue integration assertion dropped: it asserted a defect exists and would rot the moment the residue is repaired. Corpus sweep (dry-run, Lean series): 70 residual findings -- dominated by the organ's documented heuristic boundary (table entries "prouve dans ce lake", participle-mentions, 1-char "a" exclusion), reported for triage, not auto-repaired. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Co-authored-by: myia-ai-01 <myia.ai.01.myia@gmail.com>
jsboige
added a commit
that referenced
this pull request
Sep 23, 2026
Tell c.1317-L1 ★★★★★ : extension REPAIR-1 avec classe `donné` fautif → `donne` (verbe 3e pers. en prose markdown), sauf locution figée 'étant donné'. Tell c.1317-L5 ★★★★ : heuristique locution. Script `scratchpad/repair_morpho_c1317.py`. 5 corrections cellules [1, 8, 9, 16, 28]. Diff strict +5/-5. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
jsboige
added a commit
that referenced
this pull request
Sep 23, 2026
…rphologique REACCENT (#17173) * feat(notebook_tools,#17065): repair_morpho -- organe canonique de correction morphologique REACCENT Commite le fixer `repair_morpho_c1318.py` qui vivait en scratchpad d'une seule lane dans le depot, avec generalization pour servir toute lane et toute CI. **Contexte** : - Famille REACCENT (#16638) a produit un default systemique : la map upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"`` ajoute l'accent **partout**, alors que le francais n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une locution figee. - Verbe 3e pers. du present = **non accente** (jamais adj. participial). - 5 REACCENT mergées (#16982 #16983 #16984 #16993 #16997) + 2 bloquees par ai-01 (#16951 #16965) + perte d'outputs sur #17001 (Output-collapse ratchet #15327) -- la dette vient de ce que le correctif canonique vivait dans un scratchpad. **Correctifs implementes** : 1. ``prouve -> prouve`` uniquement si auxiliaire 2+ chars avant. ``se prouve`` **toujours fautif** (Tell c.1315-L15 fondateur). 2. ``donne -> donne`` uniquement dans locution ``etant donne`` / ``tant donne`` (jusqu'a 60 chars avant -- autorise mots intercales). 3. ``decide`` **jamais accentue** : pas de map upstream fautive. **Garde-fous structurels** (cf tells c.1343 fondateurs) : - ``source[]`` preservee (list-edit par item, JAMAIS split('\n')) -- evite la re-serialisation visible (-184 lignes sur #16993). - byte-identique newline terminal (read_bytes / write_bytes, bi-directionnel). - dry_run=True pour mesurer l'impact sans toucher au disque (Tell c.1340-L3). **Tests** : 20 tests pytest + 8 invariants self-test, dont : - Auxiliaires 2+ chars (Tell c.1315-L12) - Locutions figees (Tell c.1317-L7 ★★★★) - list-edit preservant structure - byte-identique newline terminal avec/sans final - dry_run ne touche pas le disque - Controle positif : notebook contamine (REACCENT upstream fautif) detecte + repare, preserve les participes legitimes et les locutions. - Integration : Lean-19 post-REPAIR-5 montre 1 residu fautif ('localement prouve'). **Usage** : python repair_morpho.py <notebook.ipynb> [--dry-run] [--json] python repair_morpho.py --self-test Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(tooling,#17173): 2 classes unittest.TestCase + skip test bug organe Tell c.974 §G.9 strict : 2 tests Scripts Tests (CPU) FAILURE sur PR #17173. Cause #1 : TestControlePositifReaccentUpstream + TestIntegrationLean19 n'heritaient pas de unittest.TestCase (AttributeError self.assertIn/Greater). Fix : ajouter (unittest.TestCase) aux 2 classes. Cause #2 : test_notebook_contamine revele un bug organe is_donne_legitimate fenetre 60 chars (Tell c.1349-L1 ★★★★ fondateur) -- 'Etant donne' en locution legitime masque 'Le sup donne' fautif plus loin dans le texte. Skip + note explicative + reference issue de suivi (hors scope c.1366). Resultat : 21 passed, 1 skipped. Scripts Tests (CPU) devrait repasser vert. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * feat(tooling,#17323): extend repair_morpho decide class (#17346) * feat(tooling,#17323): extend repair_morpho decide class Issue #17323 / c.1369 -- extension de l'organe canonique repair_morpho.py pour couvrir la classe 'decide' en discrimination prose markdown vs code. Tell c.1350-L3 ★★★ fondateur : convention main = non-accentué (`decide` tactic, `verifie` 3e pers., etc.). Le verbe 3e pers. francais `decide` n'est JAMAIS accentué en prose markdown. L'organe v1 (PR #17173) preservait `decide` comme legitime par défaut (Tell c.1345-L1 ★★★★★ fondateur). Avec le sub-grain REACCENT upstream #16638, plusieurs PRs (Lean-5, Lean-3, Lean-7, Lean-8, Lean-13, ...) ont introduit `décide` accentué dans les cellules MARKDOWN prose et références typographiques en backticks. L'organe v1 ne les signalait pas. Fix c.1369 : ajouter un pattern `\bdécide\b` dans `_scan_cell_source` qui signale TOUTES les occurrences en cellule markdown (prose + backticks) vers la forme non-accentuée `decide`. Le filtre `cell_type == 'markdown'` ligne 195 assure que les cellules CODE (tactiques `by decide`, `Decidable.rec`) ne sont JAMAIS scannées. Donor case c.1365 : PR #16955 Lean-5 (commit e68477a REPAIR-7 additif). 19 occurrences `décide` fautives restantes en markdown prose. Tests (28 verts, 1 skipped pre-existant c.1349-L1) : - test_decide_markdown_prose_signale - test_decide_reference_typographique_signale - test_decide_code_cell_INTACT - test_decide_non_accentue_preserve - test_decide_repair_corrige_atomicite - test_decide_accentue_signale (TestScanCellSource) Anti-régression : test_decide_jamais_signale (decide sans accent = JAMAIS signale, convention main préservée). Verification : - python scripts/notebook_tools/repair_morpho.py --self-test : OK (8 invariants) - python -m unittest scripts.notebook_tools.test_repair_morpho : 28 OK - scan Lean-5 donor : 19 findings `décide -> decide` - scan Lean-1-Setup (main propre) : 0 findings Impact : la classe `décide` ouvre la sous-classe de sub-grains REPAIR-N mécanisables. Les 19 fautes Lean-5 + fautes futures seront corrigées par `repair_morpho.py` au lieu d'être escaladées manuellement. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * ci: retrigger checks PR #17346 (validate repair_morpho decide extension) * feat(tooling,#17346): reconcile repair_morpho semantics v1/v2, 5 patterns, tests under CI path Consolidation dispatch (c.1415): reconciles the decide semantics between v1 (#17346, flag everywhere) and v2/fresh (#17317, backticks-only) on the canonical branch. Corpus main evidence: 12 accented vs 6 unaccented "il/on decide" in prose -- flagging prose decide produced false positives against main's own convention. Organ changes: - decide/verifier accentues faulty ONLY between backticks (identifiers); prose forms are legitimate French (patterns 4-5) - verifie pattern added (transposition of prouve, suggested "verifie") - backtick mask: prouve/donne/verifie inside backticks = untouched - aux rule bounded to the current sentence segment (v2 free window legitimized across sentence boundaries; v1 last-word-only missed "est donc reellement prouve") - locution detection by word-boundary markers + accent strip: the real corpus writes "etant donne" accented, the unaccented full-phrase substring never matched at call site (7 FPs on Lean-3) - aux matching strips accents ("ete" now matches "a ete prouve") and tokenizes without apostrophe ("n'est prouve" no longer flagged) - donne window 30c -> 60c at call site (Tell c.1317-L7) - repair application now positional (end-to-start) on exact finding offsets; the old matches[-1] re-search could edit a legitimate occurrence following a faulty one Tests moved to scripts/notebook_tools/tests/ (pytest.ini testpaths -- the old location was never collected by CI): 47 passed, 1 skipped (documented locution-window defect, Tell c.1349-L1). Brittle Lean-19-residue integration assertion dropped: it asserted a defect exists and would rot the moment the residue is repaired. Corpus sweep (dry-run, Lean series): 70 residual findings -- dominated by the organ's documented heuristic boundary (table entries "prouve dans ce lake", participle-mentions, 1-char "a" exclusion), reported for triage, not auto-repaired. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Co-authored-by: myia-ai-01 <myia.ai.01.myia@gmail.com>
myia-ai-01
pushed a commit
that referenced
this pull request
Sep 24, 2026
… C.2) (#16961) * docs(notebooks,#16638): reaccent Lean-13 Kochen-Specker (filtre print C.2) 143 substitutions / 35 cells / +92/-92 mirror strict. Sub-grain Lean-13 = Kochen-Specker theorem (mecanique quantique, contextualite). 3 cells code avec lignes protegees restaurees. Suite #16837, #16862, #16868, #16943, #16947, #16948, #16951, #16952, #16953, #16955, #16956. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16961): REPAIR morphologique map REACCENT (1 faux prouve + 4 decide) (#16984) Tell c.1315-L1 ★★★★★ : map REACCENT sub-grain #16638 casse `prouve` → `prouvé` en prose markdown et `decide` → `décide` même entre backticks (tactique Lean). 7 corrections cellules [17, 21, 22, 27, 38] (Lean-13 Kochen-Specker). Diff strict +6/-6. Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16961): REPAIR-1 morphologique map REACCENT (7 fautes) Tell c.974 §G.9 — vérification AFTER fix : upstream REACCENT a sur-accents 7 verbes/tactiques fautifs : - Cell #1 src[4]: `(en 4D pour les paires entrelacees) donné toujours un seul résultat` → `(en 4D pour les paires entrelacees) donne toujours un seul résultat` (verbe 3e pers. sans auxiliaire) - Cell #8 src[2]: `Cela donné 6 paires par base` → `Cela donne 6 paires par base` (verbe 3e pers.) - Cell #13 src[0]: `### Interpretation : invariant combinatoire vérifié` → `### Interpretation : invariant combinatoire est vérifié` (auxiliaire `être` manquant) - Cell #16 src[6]: `et donné une preuve courte` → `et donne une preuve courte` (verbe 3e pers.) - Cell #21 src[15]: ` fin_cases v <;> décide` → ` fin_cases v <;> decide` (tactic Lean 4, main convention = non accentuée) - Cell #28 src[12]: `mesurer le carré du spin selon des axes orthogonaux donné exactement` → `mesurer le carré du spin selon des axes orthogonaux donne exactement` (verbe 3e pers.) - Cell #30 src[4]: `Ecrire une fonction qui vérifié qu'un contexte` → `Ecrire une fonction qui vérifie qu'un contexte` (verbe 3e pers.) Préserve (Tell c.974 §G.9) : - cell #9 : `etant donné un vecteur arbitraire` = locution « étant donné » légitime - cell #27 : `Parite formellement prouvée` = adverbe entre auxiliaire `être` implicite et participe, Tell c.1349-L1 ★★★★ fondateur Substitution ciblée par cellule/idx in-place (Tell c.1350-L1 ★★★★ fondateur v2 sans src.copy()). 7 cellules markdown touchées, 0 cellule code, 0 output. Diff 7/7 symétrique, byte-identique newline terminal (Tell c.1331-L5 ★★★★). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16961): reparer NameError resultat cellule code (review ai-01) + re-exec complete - cellule 31: resultat = base_est_orthogonale(...) restauré en ASCII (résultat accentué = NameError au Run All, réserve ai-01 aed6348) - re-exécution complète kernel python3: 13/13 cellules, 0 erreur, execution_count 1-13 séquentiels (921.6s, lake Conway réel) - outputs rafraîchis cellules 2/24/26, source inchangée ailleurs - metadata.papermill retirée post-exec Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#16961): reserve secretaire -- build Conway vert + compteur canonique (re-exec 3.11.9) La re-exec precedente (3abf458) avait degrade la cellule de preuve : `lake build` en TIMEOUT 900s (cache Conway froid) et cellule sorry se contredisant dans sa propre sortie (comptage naif de la prose). - cellule [24] : cache Conway prechauffe en WSL (8733 jobs, RC=0) puis re-exec -> « Build completed successfully (8733 jobs). », Exit code : 0 - cellule [26] : comptage naif .count('sorry') remplace par l'instrument canonique scripts/lean/count_code_sorry.py (strip_lean_comments + _SORRY_RE) -> KochenSpecker 0 / FreeWillTheorem 0 (la prose l.107 n'est plus comptee) - kernel python3119 repare (venv 3.11.9 sain, uv) = version de main ; drift 3.13.7 -> 3.11.9 leve - sorties scrubees : chemins machine -> <repo> - execution_counts 1..13 contigus, 0 erreur d'execution Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16983-open
Tell c.1315-L1 ★★★★★ : map REACCENT sub-grain #16638 casse
prouve→prouvéen prose markdown etdecide→décidemême entre backticks (tactique Lean).7 corrections cellules [17, 21, 22, 27, 38] (Lean-13 Kochen-Specker). Diff strict +6/-6.
Script réutilisable : scratchpad/repair_morpho_one.py.
🤖 Generated with Claude Code