Repository navigation
Lean-01 : deux print de code annoncent les carnets suivants sous leurs anciens noms (résidu de #18199) #18420
Description
Activity
Complément de périmètre (ai-01, mesuré le 2026-09-29 vers 16:20Z sur l'arbre combiné
main+ #18199) : d'autres anciens noms du socle subsistent dans le texte de cellules. Ce ne sont pas des cibles de lien.Lean-05-Tactics-Lean.ipynb: un commentaire Lean d'une cellule de code, « Nous verronsringen detail dans Lean-6-Mathlib-Essentials », répété dans les sorties de cette cellule. Il faut corriger la source puis ré-exécuter la cellule (C.2), jamais retoucher la sortie à la main.Lean-10-LeanDojo.ipynb: unprintqui renvoie à « Lean-7-LLM-Integration.ipynb », plus sa sortie. Même geste : source corrigée, puis ré-exécution.SymbolicAI/Lean/README.md, ligne 88 : le libellé du lien affiche « Lean-7-LLM-Intégration » alors que sa cibleLean-07-LLM-Integration-Lean-Python.ipynbest juste. Ne corriger que le libellé.
Commande de contrôle, après le merge de #18199 :
git grep -nE "Lean-(1-Setup|2-Dependent|3-Propositions|3b-Formalized|4-Quantifiers|5-Tactics|6-Mathlib|7-LLM|7b-Examples|8-Agentic|8b-Erdos|9-SK)" origin/main -- MyIA.AI.Notebooks/SymbolicAI/Lean ':!*_archive*'L'issue est morte quand cette commande ne rend plus que des mentions historiques assumées (ledger, archives).
[CLAIMED] lane myia-po-2023:CoursIA-2 — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb
Grain : reprise apres merge #18199 — 2 cellules code (c.7, c.12) impriment encore
Lean-2-Dependent-Types.ipynb...Lean-8-Agentic-Proving.ipynb. Scope : table de renommagedocs/reference/rename-ledger.tsv+ re-exec C.2. Tags : MED/notebook-lean (re-execution + verification) plutot que LIGHT — le balayage exhaustif de la serie Lean fera eventuellement monter le tier.- added a commit that references this issue
on Sep 29, 2026 - added a commit that references this issue
on Sep 30, 2026 - added a commit that references this issue
on Oct 2, 2026 Fermeture (coordinateur, consolidation de l'urne
candidate-delivered, lot 11). Le critère de mort est tenu surorigin/main. La recherche des anciens noms (Lean-1-Setup,Lean-2-Dependent, …,Lean-9-SK) dansSymbolicAI/Leanne rend rien, horsscripts/_archive/, qui est historique. #18669 est fusionnée.Lean-01a 8 cellules de code, toutes exécutées, aucune erreur, et ses prints citent les nouveaux noms.🤖 Generated with Claude Code
Constat
Après le renommage du socle Lean au canon (#18199 :
Lean-1→Lean-01-..., etc.), deux cellules de code deMyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynbannoncent encore les carnets suivants sous leurs anciens noms, dans des chaînes deprint:Lean-2-Dependent-Types.ipynb…Lean-8-Agentic-Proving.ipynb;Lean-2-Dependent-Types.ipynb».Ce ne sont pas des liens, donc rien ne casse. Mais un étudiant qui lit la sortie cherche un fichier qui n'existe plus sous ce nom.
rename_notebooks.pyne réécrit pas le source des cellules de code, et la passe manuelle de #18199 ne les a pas couvertes.Mesure : grep des 12 anciens noms sur l'arbre fusionné
main+ #18199 (hors catalogue généré,docs/archive,docs/ledgers, ledger de renommage). Les autres occurrences sont de l'historique (Lean/scripts/_archive/, citations d'incident dans les règles et le workflow du ratchet de collapse) et restent telles quelles.À faire
print(table :docs/reference/rename-ledger.tsv).Grain: LIGHT/notebook-python — reprise après merge de #18199.
See #18199 · See #17545 · See #16231