Repository navigation
renum(Lean): refermer la colonne canonique (trous 18 et 25) — mapping 19..32 à 18..31 (fille #5081) #15612
Description
Activity
[CLAIMED] lane myia-po-2027:CoursIA — exécuter la tranche : 17 renames + sweep des refs (README série, lakes, _quarto, curriculum, production-scope). Catalog byte-identique, ledgers intouchés.
- added a commit that references this issue
on Sep 11, 2026 [DELIVERED] tranche refermeture — PR #15613 (17 renames + sweep 388 refs + READMEs réconciliés, cellules code/outputs préservées à HEAD). Colonne passe à 01..30 continue.
Résiduel ouvert sur cette issue : re-exécution papermill (kernel
lean4-wsl) de 5 notebooks dont les commentaires code + miroirs alectryon citent les anciens numéros (16h, 18-Sendov, 19-Tao, 21-MIMO, 26-Munkres — 7 cellules). RECOVERABLE-LOCAL.- added a commit that references this issue
on Sep 11, 2026 Re-exécution résiduelle — tranche 1/5 livrée (PR #15613, commit
aca6413b)- Lean-16h Conway PatternTour : re-exécuté — kernel
lean4-wslcwdconway-build(seul lake Lean reconstitué avec oleans chauds post-reinstall(env): WSL Ubuntu distro post-incident vide (ext4.vhdx perdu 04/09) -- env coursia-wsl + kernels a reconstruire #14631). 27/27 cellules, 0 erreur, 0 ❌,execution_countréels partout. Seule cellule source modifiée : cellule 2 (commentaire du pattern d'importation, Lean-26→Lean-24). Sorties + miroir alectryon régénérés : 0 tokenLean-26résiduel sur sources et sorties. - 4 notebooks restants bloqués sur prerequisite lakes (mesuré firsthand dans WSL) :
~/lean-projects/ne contient quenotebook_context— les lakessendov,teorth/analysis(Tao),mimo_lean,mathlib_examples(Munkres) n'existent plus depuis l'incident 04/09 (reinstall(env): WSL Ubuntu distro post-incident vide (ext4.vhdx perdu 04/09) -- env coursia-wsl + kernels a reconstruire #14631, reconstitution partielle). Chaque re-exécution exige la reconstruction du lake (fetch mathlib + build, multi-heures par lake). - Route proposée : grain dédié de reconstruction, un lake par tranche (conway-build = gabarit : packages
cp -aldepuis un lake même rev quand possible, cf leçon feat(notebook-lean,#14871): Percolation-Lean.ipynb — compagnon exécutable du lake percolation_lean #14927). Les 4 notebooks restent à HEAD (cellules code non modifiées — aucun hand-edit d'output).
Suivi : le résiduel reste ouvert ici, la colonne canonique est livrée dans #15613.
- Lean-16h Conway PatternTour : re-exécuté — kernel
Correctif de mesure — la reconstruction de lake est MINUTES, pas « multi-heures » (prémisse de mon commentaire précédent réfutée)
J'ai mesuré firsthand ce cycle la recette de réassemblage sur
mimo_lean, et elle est bien plus rapide que ce que j'avais écrit :sources (tar depuis le repo) + cp -al <build chaud même rev>/.lake/packages + lake build → Build completed successfully (8702 jobs) en 1m54s oleans : /home/jesse/mimo-build/.lake/build/lib/lean/{Converse,Descent,Lmmse,Objective}.oleanLe déterminant n'est pas la taille du projet, c'est l'existence d'un build chaud à la même rev Mathlib (les packages sont hardlinkés, donc Mathlib n'est jamais recompilé — seul le projet se construit).
Inventaire des builds chauds disponibles (mesuré) :
build toolchain rev Mathlib oleans Mathlib conway-build v4.32.1 520045ab14e2oui gtl-build v4.32.1 520045ab14e2oui knots-build v4.32.1 520045ab14e2oui perc-build v4.32.1 520045ab14e2oui Conséquence par notebook résiduel :
notebook lake requis rev état Lean-21 MIMO mimo_lean(vendorié dans le repo)v4.32.1 520045ab— build chaud existelake WSL réassemblé en 1m54s ✓ ; re-exécution en cours Lean-26 Munkres Mathlib seul ( Mathlib.Topology.*, aucun module projet)v4.33.0 db584cd— aucun build chaudpasse par lake exe cache get(oleans prébuilt) — à tenterLean-19 Tao ~/lean-projects/analysis(clone EXTERNEteorth/analysis, chemin codé en dur)? clone + build à faire Lean-18 Sendov ~/lean-projects/sendov(clone EXTERNE, chemin codé en dur)? clone + build à faire Deux mécaniques distinctes dans les notebooks (mesuré dans les cellules) : MIMO invoque
lakelocalement (MIMO_LEAN_PATHoumimo_lean/voisin du cwd, kernel python3 Windows) ; Tao/Sendov passent parwsl -d Ubuntu -- bash -lc 'cd ~/lean-projects/<lac> && lake env lean …'avec le chemin codé en dur (pas de variable d'environnement) — d'où l'obligation de reconstruire à cet emplacement exact pour ces deux-là.Suite : Munkres (cache get v4.33.0), puis les deux clones externes — chacun en tranche atomique.
- added a commit that references this issue
on Sep 11, 2026 [INFO] Tranche MIMO livrée — PR #15613, commit
50bc14ee.Lean-21-MIMO-Detection-Flips: la cellule 9 portaitLean-21(auto-référence au mauvais numéro de série) → corrigée enLean-20. Re-exécution complète : 13 cellules code,execution_countréels, 0 erreur, 0 marqueur d'échec.Contrôles (tous sur la sortie re-exécutée, relancés après le dernier commit) :
Contrôle Résultat Audit cellule-par-cellule vs HEAD 1 seule cellule à source modifiée (la cellule 9) ; le reste = sorties + métadonnées papermill Ratchet Output-failure(bloquant)0 regressed Ratchet Output-collapse(advisory)0 flagged Voie utilisée — celle que le notebook documente lui-même : la cellule 2 déclare
MIMO_LEAN_PATH« utile pour re-exécuter sans rebuild local ». Lake~/mimo-buildréassemblé par la recette mesurée ce cycle (1 min 54 s) depuis~/conway-build, rev Mathlib identique520045ab14e2. Kernel python WSL adossé à ce lake.Cela confirme, sur un deuxième lake, que le déterminant d'un réassemblage n'est pas la taille du projet mais l'existence d'un build chaud à la même rev — la prémisse « reconstruction multi-heures » qui figurait sur ce fil est bien à corriger (mesure déjà postée plus haut).
Résiduel : 3 notebooks, chacun pour une raison distincte :
Notebook Raison Geste 26-Munkres lake sur une autre rev Mathlib ( db584cd6d46c, v4.33.0) — aucun build chaud à cette revlake exe cache get(oleans prébuilt) puis build ; recette préparée19-Tao lake dans ~/lean-projects/analysis, clone externe à chemin codé en dur dans le notebook (aucune variable d'env)voie différente : rendre le chemin paramétrable ou réassembler à l'emplacement attendu 18-Sendov idem, ~/lean-projects/sendovidem Les deux derniers ne se traitent pas par la recette MIMO : leur notebook ne désigne pas son lake par une variable d'environnement, donc l'emplacement est contraint par le code lui-même.
- added a commit that references this issue
on Sep 11, 2026 Rectificatif — qualification d'une des deux corrections de la cellule 9 (PR #15613).
Le rapport de livraison ci-dessus décrit la cellule 9 de
Lean-21-MIMO-Detection-Flipscomme portant une « auto-référence au mauvais numéro de série ». C'est faux, et la mesure le dit : ce fichier étaitLean-22-…surmain(le renumber est 22→21), donc la chaîneLean-21qu'il contenait ne pouvait pas être une auto-référence — c'était une référence croisée vers le notebook PFR, exactement comme les cellules 0 et 40 du même fichier.Mesure (diff des sources cellule par cellule,
origin/main→ tête de branche) :Cellule Avant Après Nature 0 (markdown) # Lean-22 : …/[Lean-21 (PFR)]/[Lean-23 (Galois)]# Lean-21 : …/[Lean-20 (PFR)]/[Lean-22 (Galois)]titre + 2 réfs croisées 9 (code) # Mecanique identique a Lean-21 : …# Mecanique identique a Lean-20 : …référence croisée — la seule cellule code touchée 40 (markdown) [Lean-21 (PFR)][Lean-20 (PFR)]référence croisée La distinction n'est pas cosmétique : une auto-référence fausse signalerait un titre désynchronisé (défaut de contenu), une référence croisée non migrée signalerait un lien mort (défaut de navigation). Les deux se corrigent, mais pas au même endroit, et un relecteur qui part de la mauvaise qualification cherche au mauvais endroit. Le libellé exact est rétabli dans le body de #15613.
Second résidu trouvé en re-vérifiant, et corrigé : la cellule 9 portait aussi
lean22_{tag}.lean— le préfixe du nom de fichier temporaire interne, resté à l'ancien numéro. Le sweep ne l'a pas vu parce que ses motifs portaient la formeLean-<n>(majuscule + tiret) ;lean22_(minuscule, underscore) y échappait. Un balayage élargi aux deux casses sur les 21 notebooks du diff rend 1 occurrence, celle-là, désormaislean21_.C'est le même angle mort que celui documenté sur les compteurs de prose : un motif se valide par ses faux négatifs — ici, une forme que le sweep ne pouvait structurellement pas attraper. La cellule 9 étant une cellule code, la correction a exigé une re-exécution complète (aucun hand-edit d'outputs, C.2).
- added 5 commits that reference this issue
on Sep 11, 2026 10 remaining items
- added 7 commits that reference this issue
on Sep 13, 2026 - added a commit that references this issue
on Sep 13, 2026 - added a commit that references this issue
on Sep 14, 2026 - added a commit that references this issue
on Sep 16, 2026 FERMEE — verification firsthand contre
origin/main@0dcc80c1fb7b748646b500672ef4df1873ba8013.Livree par #15613 (
5495fb9ebc) et #16039 (fb62633ef2), toutes deux MERGED. Le scope ferme de l'issue — 17 renames + sweep des refs — est atteint : arborescence finale 01..30, 388 references balayees, READMEs reconcilies, cellules code et outputs preserves a HEAD ; #16039 solde les 3 refs Lean stale residuelles de GT-16d.Le residu de re-execution papermill (Lean-26/19/18, bloques sur des prerequisite lakes : Munkres v4.33.0, Tao et Sendov a chemins codes en dur) n'est pas un critere de cette issue — c'est un sujet distinct, qui doit vivre dans son issue propre plutot que tenir la renumerotation ouverte. Lean-16h (27/27 cellules, 0 erreur) et Lean-21 (13 cellules, execution_count reels) sont re-executes.
Fille de #5081 (nommage canonique), dépôt série par série conformément au commentaire user du 2026-09-02 : « des gaps dans GT et Lean qui méritent une renumérotation globale mais compte tenu de l'impact, il faudrait faire série par série sur le principe de cette issue et des suivantes de consolidation (accrétions) ». Sœur directe de #14944 (GameTheory, trous 20-23) — même principe, même tell.
Le défaut, mesuré firsthand (2026-09-11)
Colonne canonique
SymbolicAI/Lean(numéros nus, sans lettre) :Deux trous, provenance vérifiée
git log --all --diff-filter=D:Lean-18-Search-AStar-OptimalityrenomméSearch-03e-AStar-Optimality(fix(search,#13841): minimal rename Lean-18 -> Search-03e + README attribution fix #14250, livrée) — le notebook a déménagé dans la série Search, la colonne n'a pas été refermée derrière lui.Lean-25rangé en accrétionLean-22c-Descente-Budget(refactor(notebooks,#12375): renames FORT — Planners-13->5c, Lean-25->22c (tranche renames) #13355/Reorganisation : ranger en sides (-b/-c) les ajouts recents qui ont pris un numero sequentiel (GT-19..23, Lean-25/26, Audio 04-7..13, ICT-Life, rlpt_, Planners-13) #12375) — le même chantier Reorganisation : ranger en sides (-b/-c) les ajouts recents qui ont pris un numero sequentiel (GT-19..23, Lean-25/26, Audio 04-7..13, ICT-Life, rlpt_, Planners-13) #12375 qui a créé le trou GT 20-23 corrigé par renum(GameTheory): refermer la colonne canonique (trou 20-23) + anomalie de profondeur GT-03 #14944 : il a rangé en sides des ajouts qui avaient pris un numéro séquentiel, sans refermer la colonne.notebook-accretion-numbering.md§1 : « Lire les numéros nus dans l'ordre EST le parcours canonique ». Un trou de palier n'est pas cosmétique : le lecteur du speed-run infère une étape 18 puis une étape 25 qu'il ne trouvera nulle part (tell faux prérequis séquentiel, même classe que #14944).La réparation : un seul décalage referme les deux trous
Tout numéro N ≥ 19 devient N−1. Les trous 18 et 25 disparaissent simultanément, la colonne devient continue 01..30.
17 fichiers renommés, 0 créé, 0 supprimé.
Blast radius mesuré (
git grepsur fichiers tracés)SymbolicAI/Lean/README.md,LEAN_INVENTORY.mdgalois_lean/README.md,mathlib_examples/README.{md,en.md},mimo_lean/README.mdMyIA.AI.Notebooks/SymbolicAI/README.md_quarto.yml,docs/curriculum/ia-symbolique.md,docs/notebook-metadata/production-scope.mdscripts/notebook_tools/hopf_s6_reproduction.py, tests associésCOURSE_CATALOG.generated.*docs/ledgers/*,scripts/results/*datésHors périmètre de cette fille (verdicts conformes, aucune action)
*→b#14950 s'applique : pas de renum de confort.aexplicites (16a, 17a) : déviation mineure au « la base vaut implicitement a » ; renommer 16a→16 nu serait du churn cosmétique à blast-radius non nul. Refusé.Séquençage note
Deux PRs ouvertes de la même lane touchent des fichiers adjacents : #15583 (LEAN_INVENTORY.md, comptes sorry) et #15580 (README série, aération de paragraphes). Régions distinctes ; la tranche se rebase après leur atterrissage si nécessaire.