Repository navigation
SymbolicAI(lean) : le canonique FR ecrit les noms de lakes en *_lein au lieu de *_lean (53 occurrences de prose sur 7 fichiers) #24198
Description
Part of #24143 (fidelite semantique des miroirs i18n Lean).
Constat
Le canonique FR de la serie Lean ecrit de facon systematique les noms de lakes avec un suffixe *_lein la ou les repertoires reels portent *_lean :
| forme ecrite (prose FR) | repertoire reel |
|---|---|
grothendieck_lein |
MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/ |
conway_lein |
MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/ |
knot_lein |
MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/ |
Mesure sur origin/main (grep *.lean, forme exacte) :
knot_lein: 8 occurrencesconway_lein: 25 occurrencesgrothendieck_lein: 20 occurrences
Total 53 occurrences reparties sur 7 fichiers .lean, toutes dans la prose (commentaires et docstrings), aucune dans une declaration :
grothendieck_lean/Grothendieck/CategoryAndSites.lean(15 + 11 + 7 = 33)conway_lein/Conway/KochenSpecker.lean(3 + 8 + 1 = 12)conway_lean/Conway/CollatzLike.lean(2 + 4 = 6)conway_lein/Conway/FreeWillTheorem.lean(1)conway_lein/Conway/Life/GridCanonical.lean(1)
Portee
Correction prose uniquement : remplacer *_lein par *_lean dans les commentaires et docstrings. Aucun code de preuve n'est touche, aucun sorry n'est ajoute ni retire (le lake grothendieck_lean est a distinct_code_sorry = 0).
Contrainte de coherence i18n (#4980)
Un miroir _en doit reproduire verbatim les jetons de son canonique. Corriger le canonique FR impose donc une seconde passe sur les miroirs concernes, dans la meme PR ou dans une PR de suivi, sinon l'organe scripts/lean/check_i18n_token_fidelity.py signalera un ecart DUR inverse.
Instance : le miroir CategoryAndSites_en.lean porte aujourd'hui knot_lein (7 occurrences) parce que son canonique le porte ; la correction du canonique fera basculer ces 7 occurrences en ecart DUR tant que le miroir n'est pas remis a jour dans la meme livraison.
Verification attendue
grepexactknot_lein|conway_lein|grothendieck_leinsur*.lean: 0 occurrence ;python scripts/lean/check_i18n_token_fidelity.py --all --json: 0 ecart DUR ;python scripts/lean/count_code_sorry.py --json:distinct_code_sorryinchange sur les lakes concernes.
Activity
jsboige commentedon Nov 2, 2026
[CLAIMED] lane myia-po-2024:CoursIA -- correction prose
*_lein->*_leansur les canoniques FR et leurs miroirs EN dans la meme livraison (contrainte #4980), verification parcheck_i18n_token_fidelity.py --all --jsona 0 ecart DUR etcount_code_sorry.pyinchange.Grain: MED/lean -- lane myia-po-2024:CoursIA -- prev: DEEP/notebook-lean #24166
paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/, MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/**
Garde anti-collision passee avant claim : aucun commentaire sur l'issue, aucune PR ouverte mesuree sur ces chemins.
jsboige commentedon Nov 2, 2026
[DELIVERED] lane myia-po-2024:CoursIA -- PR #24237
paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/
53 remplacements octet-exacts sur 39 lignes de prose, 5 fichiers.
git grepsur les troisgraphies -> 0 fichier residuel ;
check_i18n_siblings.pysur les deux lakes -> 0 drift,0 orphan ;
distinct_code_sorryinchange (conway_lean 1, grothendieck_lean 0).Deux ecarts mesures contre le body de l'issue, detailles dans la PR : les occurrences sont sur
5 fichiers et non 7, et les miroirs
_enn'en portent aucune (la correction referme l'ecarti18n, elle n'en ouvre pas).
check_i18n_token_fidelity.py, cite par la verification attendue,n'existe pas sur
main; les deux organes existants ont ete utilises a la place.La cloture revient au coordinateur : le critere 2 de l'issue nomme un organe absent, donc
l'acceptance n'est pas integralement « executable telle qu'ecrite » meme si la propriete visee
est prouvee.