fix(lean,#19733): Lean-21 cell[9] WSL/native subprocess fork

[jsboige]

Grain: DEEP/lean -- lane myia-po-2026:CoursIA-2 -- prev: LIGHT/lean c.1435

Issue : #19733 (re-execution PR #19564 a echoue sur cell[9] subprocess.run(["lake", "env", "lean", str(tmp)], cwd=...) avec FileNotFoundError [WinError 2] sur une machine ou MIMO_LEAN_PATH est un chemin WSL).

Cause-racine documentee

Le subprocess.run(["lake", ...]) natif Win32 ne peut pas traverser un chemin WSL (/home/..., /mnt/..., /tmp/...) ni trouver le binaire lake si celui-ci vit en WSL plutot qu'en elan natif. Le cell[9] original n'a aucune detection : il assume que LAKE_DIR est un chemin natif Windows.

Fix

Ajout d'une detection WSL dans le helper run_lean_snippet(cell[9]) : la regex ^/[A-Za-z0-9._-] matche les chemins absolus POSIX. Si le match est positif, on detourne par wsl -e bash -lc "cd $LAKE_DIR && lake env lean $WSL_TMP" (patron canonique Lean-03b cell[11/13, deja valide sur po-2024). Sinon, on garde le subprocess natif Win32 inchange (cas canonique po-2026 avec lake elan natif C:\Users\jsboi\.elan\bin\lake.exe).

La branche Windows est byte-egale au code d'origine (memes cwd=str(LAKE_DIR), memes args, meme timeout). La branche WSL est ajoutee, jamais substituee.

# Detection WSL : un chemin absolu POSIX (/home/..., /mnt/..., /tmp/...) provient
# de WSL et ne peut pas etre traverse par subprocess.run natif Win32 (cf. issue
# #19733). On detourne alors par `wsl -e bash -lc` (patron Lean-03b cell[11/13]).
_WSL_PATH_RE = re.compile(r"^/[A-Za-z0-9._-]")

def _is_wsl_path(p):
    return bool(_WSL_PATH_RE.match(str(p)))

def run_lean_snippet(snippet, tag):
    tmp = Path(tempfile.gettempdir()) / f"lean21_{tag}.lean"
    tmp.write_text(snippet, encoding="utf-8", errors="replace")
    if _is_wsl_path(LAKE_DIR):
        wsl_tmp = subprocess.run(
            ["wsl", "-e", "wslpath", "-a", str(tmp).replace(chr(92), "/")],
            capture_output=True, text=True, encoding="utf-8", errors="replace"
        ).stdout.strip()
        cmd = f"cd {LAKE_DIR} && lake env lean {wsl_tmp}"
        res = subprocess.run(
            ["wsl", "-e", "bash", "-lc", cmd],
            capture_output=True, text=True, encoding="utf-8", errors="replace",
            timeout=600,
        )
    else:
        res = subprocess.run(
            ["lake", "env", "lean", str(tmp)],
            cwd=str(LAKE_DIR), capture_output=True, text=True,
            encoding="utf-8", errors="replace", timeout=600,
        )
    ...

Acceptation #19733

• Cause identifiee (vs contournee) : chemin WSL + subprocess natif Win32.
• Fix livre en PR (cette PR, scope 1 fichier + 1 cellule + 1 helper inline).
• Reproduction du cell[index] sur kernel canonique : reportee -- le lake env lean cold cache sur po-2026 prend > 10 min (charge Mathlib complet), et la validation runtime de la branche WSL necessite un test sur po-2024 ou un mock avec chemin WSL. La logique de detection est validee en isolation (regex True/False OK) et la branche WSL suit le patron canonique Lean-03b (deja valide en production).

Verifications pre-commit

• H.3 pre-commit : 11 hooks PASSED (rapport inline).
• AST parse : source cell[9] valide Python 3.10+ (ast.parse OK).
• Branche Windows : logique validee (is_wsl_path("D:\\...") == False, is_wsl_path("/home/...") == True).
• Branche WSL : patron canonique copie de Lean-03b cell[11/13 (deja valide en production sur po-2024).

Perimetre

• 1 fichier modifie : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb
• 1 cellule modifiee : cell[9] (Code 2.1 Localisation du lac + #check des quatre theoremes phases)
• +31/-6 sur la cellule (helper is_wsl_path, branche WSL dans run_lean_snippet, docstring explicative)
• cell[14] (Code 2.3) beneficie automatiquement du fix : il appelle le meme run_lean_snippet defini en cell[9]

Refs : #19733, #19564 (PR parent), Lean-03b cell[11/13 (patron canonique).

Co-Authored-By: Claude Haiku 4.5 (1M context) noreply@anthropic.com

---

🤖 Generated with Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.3s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	17.5s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.9s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.9s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 13
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19858 (fix(lean,#19733): Lean-21 cell[9] WSL/native subprocess fork) 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 -- Fix(lean,#19480): errors=replace sur subprocess utf-8 dans 5 carnets Lean #19564 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19858
head: 45fc63f
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 941df13f4fc9be3b52ec740cf21d93282fece5a862858a2fbfc5674d92777227
diff-files: 1
diff-additions: 31
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19858
organ-rc: 0
[/ADJOINT PREFLIGHT]

Reserves nommees, verifiees firsthand -- elles ne bloquent pas, elles doivent se lire avant le merge.

1. La branche WSL est ecrite, jamais exercee au runtime. Mesure : la cellule code[9] change (sources-code modifiees=1) et la sortie totale du carnet est byte-stable (base=79790 head=79790). Ce n'est pas une sortie falsifiee -- la branche Windows est byte-egale au code d'origine, donc les sorties committes restent celles que le code produit sur la machine qui les a produites. Mais la branche ajoutee (wsl -e bash -lc) n'a tourne nulle part : le body le dit lui-meme (« Reproduction du cell[index] sur kernel canonique : reportee », case non cochee, > 10 min de cold cache Mathlib sur po-2026). C'est un residuel RECOVERABLE-MACHINE -- la validation demande un po-2024 (WSL), patron Lean-03b deja valide la-bas. Le merge ne ferme pas #19733 (closingIssuesReferences=0, aucun mot-cle de fermeture dans le body) : l'acceptation reste ouverte, et c'est exact.

2. Ordre de merge -- cette PR doit passer AVANT #19564. Mesure : git merge-tree --write-tree entre les deux tetes rend rc=1 (conflit reel de contenu sur Lean-21-MIMO-Detection-Flips.ipynb, meme fichier, cellules voisines). Et la cause n'est pas une coincidence : la re-execution de #19564 a echoue sur subprocess.run(["lake", ...]) en FileNotFoundError [WinError 2] sur chemin WSL -- c'est exactement #19733, dont cette PR est le correctif. Merger #19858 puis #19564 (qui devra rebaser) est l'ordre qui coute un rebase ; l'inverse coute un rebase et laisse #19564 bloque sur la meme panne.

3. C.1/C.2 structurels : 13 cellules code, exec_null=0, sans_output=0, erreurs=0, aucun motif C.1. Fold vert : 94/94 jambes.