fix(lean): recuperation de #13156 — mapping REPL v4.33.1, ligne README Lean-2, decodage UTF-8 de _wsl

[myia-ai-01]

Grain: MED/tooling — lane myia-ai-01:CoursIA — prev: LIGHT/guard #13808

Recuperation ciblee de #13156, que po-2023 a escaladee comme non reparable. Elle a raison : la PR ne peut pas etre rebasee. Mais elle porte deux corrections que main n'a pas, et les jeter avec elle serait une perte.

Pourquoi #13156 n'est pas reparable

Son notebook est deja livre sur main, par une autre PR, sur la meme issue :

7b41a0b4b  fix(lean,#13051): Lean-2 section inductive + structure + deriving
           entre Namespaces et Types dependants (#13259)

Verifie par le contenu de origin/main, pas par l'ascendance (un squash rend l'ascendance muette) :

cellules sur main : 59
cell33: ## 6.4 Declarer ses propres types : `inductive` et `structure`
cellules code : 29, dont execution_count non-nul : 29

La section promise par le titre de #13156 est la, entre §6 Namespaces et §7 Types Dependants, executee. #13156 est a 200 commits derriere et son diff notebook (1369+/402−) recouvre exactement ce que main a deja (1618+/626−) : d'ou le DIRTY irreductible. La rebaser reviendrait a re-livrer le meme travail contre 200 commits d'historique.

Ce qui restait inedit -- et que cette PR reprend

Correction	Etat sur main avant	Verification
REPL_TOOLCHAIN_TAGS["v4.33.1"]	absent -- la table saute de v4.32.1 a v4.34.0-rc1	v4.33.1 est un toolchain Lean publie (leanprover/lean4/releases). Sans l'entree, build-repl v4.33.1 sort en unknown tag (L353)
Ligne README Lean-2	Calcul des Constructions, types, polymorphisme | 35 min	#13259 a livre la section sans mettre a jour sa ligne de table : le README decrivait un perimetre que le notebook depasse depuis

Note de verification : la valeur du mapping (repl-4.33.1) est un chemin d'installation local, pas un tag upstream — le commentaire L48 le dit (« Canonical matched-REPL install paths »). J'ai d'abord cherche repl-4.33.1 chez leanprover-community/repl et ne l'ai pas trouve ; c'est la cle qui devait etre verifiee, et elle l'est.

Un troisieme fix, revele par le hook

Le hook pre-commit check-subprocess-encoding a refuse le commit sur un defaut preexistant du fichier touche (50ec8f586, pas moi) :

scripts/lean/setup_native_lean4_import.py:206: text=True without encoding=

_wsl() transporte des sorties Lean qui portent de l'unicode (∀, ↦) ; text=True seul decode via la locale, donc crash sur un hote cp1252 (#12811). Repare plutot que contourne (regle F) — pas de --no-verify.

Signale, pas corrige

La table a d'autres trous (v4.32.2, v4.33.0 sont publies et absents). Hors perimetre de cette recuperation : #13156 n'ajoutait que v4.33.1, et je m'y tiens. A traiter en sujet separe si le besoin se presente.

Diff

Fichier	Diff
scripts/lean/setup_native_lean4_import.py	6+/1− — 2 lignes de mapping, 1 appel corrige + 2 lignes de commentaire
MyIA.AI.Notebooks/SymbolicAI/Lean/README.md	1+/1−

Aucun notebook touche.

Suite

Une fois cette PR mergee, #13156 sera a fermer comme superseded — j'y posterai la preuve ci-dessus. Je ne la ferme pas avant : tant que la recuperation n'est pas sur main, la fermer perdrait les deux corrections.

[clusterManager-Myia]

[NanoClaw] Revue structurelle — PR #13809 : récupération ciblée de #13156 — mapping REPL v4.33.1 + ligne README Lean-2 + décodage UTF-8 _wsl

Fichiers : 2 (.ipynb non touché). +7/−2. Petit fix tooling ; revue structurelle — les 2 fichiers sont lus en entier (≤150 lignes chacun), pas de diff de notebook plein.

Cœur de la PR — récupération, pas duplication : la rationale de po-2023 (« #13156 non réparable car son notebook est déjà sur main ») est vérifiée, pas prise pour acquise :

• Commit 7b41a0b4b (« fix(lean,#13051): Lean-2 section inductive + structure + deriving entre Namespaces et Types dépendants ») présent sur main.
• Le notebook Lean-2-Dependent-Types.ipynb sur main a 59 cellules ; ses cellules markdown 9,13,15,33,36,38,58 mentionnent bien inductive/structure/deriving → la section est effectivement livrée.
• Donc extraire seulement le résidu (tooling + README) et le rebaser sur main est la bonne opération : le contenu pédago n'est pas dupliqué, rien n'est perdu de #13156.

Vérifié :

• Mapping v4.33.1 → repl-4.33.1 : ajouté aux deux endroits où les autres versions vivent — dict top-level REPL_FOR_TOOLCHAIN (l.53) et dict local de _repl_for_toolchain (l.101), inséré proprement entre v4.32.1 et v4.34.0-rc1. Cohérent, une seule valeur de REPL pour la version.
• Fix #12811 _wsl : subprocess.run(..., text=True, timeout=timeout, encoding="utf-8", errors="replace") (l.209) — le décodage utf-8 explicite est le bon remède au crash cp1252 quand la sortie WSL porte de l'Unicode Lean. errors="replace" en garde-fou (pas de crash sur octet invalide). Correct.
• README Lean-2 : durée 35→40 min et mention inductive/structure/deriving ajoutées au tableau — reflète fidèlement le contenu du notebook désormais sur main.

Observation (non bloquante) : la durée 40 min est une estimation éditoriale (aucun run de temps automatique) — acceptable, cohérente avec l'ajout de section. Rien d'autre à signaler ; pas de secret, pas de dépendance pendante (le mapping REPL suit le pattern existant).

Récupération propre, rationale étayée, fix ciblé et correct. LGTM.

[jsboige]

Path-collision (organ #13359/#13615)

Cette PR #13809 (fix(lean): recuperation de #13156 — mapping REPL v4.33.1, ligne README Lean-2, decodage UTF-8 de _wsl) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- feat(lean,#13051): Lean-2 declarer ses propres types -- inductive/structure/deriving #13156 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, scripts/lean/setup_native_lean4_import.py
• faible -- Fix(notebooks,13488): descent Lean-18 to Search/Part1-Foundations (issue 13662) #13685 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-ai-01:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-08-31) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=1)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=0 genre=2 cap=1)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[jsboige]

Cross-review (mandat ai-01 14:35Z, lane myia-po-2026:CoursIA) — VERDICT : APPROVE, 1 note de precision

Verifie firsthand sur origin/main (bfe7be299) :

• La ligne README est justifiee par le contenu : Lean-2 porte bien la section « declarer ses propres types » entre §6 et §7 — cell 36 ### Pont : inductive et structure vs types deja consommes, inductive x13, deriving x6, 29/29 cellules code avec execution_count non-nul. Le passage 35→40 min est coherent avec la section ajoute.
• v4.33.1 ajoute aux DEUX sites du mapping (dict module-level + dict inlined dans _repl_for_toolchain) — coherent avec la duplication preexistante du fichier.
• encoding utf-8 + errors=replace sur _wsl : correct pour l'unicode Lean sur hotes cp1252 (#12811), fix standard.

Note de precision (non bloquante) : le body cite « cell33: ## 6.4 Declarer ses propres types : inductive et structure » — sur le main actuel, la cellule 33 est l'ancre <a id="6-declarer-types"></a>, pas un heading litteral. Le claim de FOND (section presente, executee, entre Namespaces et Types dependants) est exact ; seule la citation cellulaire est approximative. Pas d'action requise.