fix(lean): resolve WSL kernel lake from notebook cwd

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-python #16199

Résumé

• transmet un répertoire d’exécution explicite à Papermill, avec le répertoire du notebook par défaut et --cwd <lake-root> pour les companions placés à côté de plusieurs lakes ;
• effectue un vrai cd WSL, transmet aussi --cwd au kernel manager et câble --start-timeout sur le timeout demandé ;
• vérifie le lake avant de lancer lean4-wsl et échoue visiblement si aucun lakefile.lean ou lakefile.toml n’est accessible ;
• supprime le fallback silencieux du wrapper Windows vers ~/lean-projects/notebook_context, propage son code d’échec via sys.exit(main()) et aligne l’installateur sur la source canonique v7 ;
• documente les deux chemins de lancement et ajoute les tests de régression associés.

Validation automatisée post-rebase

77 passed in 0.90s

Commande :

python -m pytest scripts/notebook_tools/tests/test_wsl_papermill.py scripts/lean/tests/test_lean4_kernel_wrapper.py scripts/lean/tests/test_lean_kernel_check.py -q
python -m py_compile scripts/notebook_tools/wsl_papermill.py MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/lean4-kernel-wrapper.py scripts/lean/tests/test_lean4_kernel_wrapper.py
bash -n MyIA.AI.Notebooks/GameTheory/scripts/setup_wsl_lean4.sh
git diff --check origin/main...HEAD

Les quatre commandes passent après rebase sur origin/main.

Contrôles réels WSL

Positif Lean — lake isolé Lean 4.32.1

Le module Probe.lean a été construit réellement avec lake build Probe, puis un notebook de trois cellules a été exécuté avec le venv par défaut ~/coursia-wsl, sans option --venv :

[info] cwd: .../lean16181-lake
Executing (WSL): lean16181-positive.ipynb ...
  OK: 3/3 cells executed, 0 errors (8.0s)

Outputs vérifiés dans le notebook exécuté :

import Probe
Probe.answer_is_42 : Probe.answer = 42
4

Négatif Lean — notebook hors lake

ERROR: Lean 4 kernel startup aborted: no lakefile.lean or lakefile.toml found from .../scratchpad. Pass --cwd <lake-root>.

Le lanceur retourne 1 avant Papermill : plus de kernel muet ni de faux OK: 3/3, 0 errors dans ce cas.

Positif Python — chemin WSL commun

Une copie scratch de GameTheory-01-Setup.ipynb a été exécutée avec le cwd GameTheory explicite :

[info] venv: ~/coursia-wsl
[info] cwd: .../MyIA.AI.Notebooks/GameTheory
Executing (WSL): lean16181-python-wsl.ipynb ...
  OK: 22/22 cells executed, 0 errors (5.3s)

Limite d’environnement observée

Une première validation sur conway_lean a rencontré un checkout Mathlib local dégradé (untracked working tree files would be overwritten by checkout) ainsi qu’une contention Git pendant un build concurrent. Aucun reset ou nettoyage destructif n’a été effectué. Cette dégradation est indépendante du cwd ; le contrôle positif canonique de cette PR utilise donc le lake minimal isolé construit et exécuté réellement.

Cette PR ne modifie aucun fichier *.lean; le gate de comptage sorry et proof-integrity est non applicable.

Closes #16181

🤖 Generated with Claude Code

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

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

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 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.

[clusterManager-Myia]

[Hermes] VERDICT: LGTM (structural)

Review du head 418aa3f0 (7 fichiers, +332/−49, 0 review préexistante). Diff lu intégralement ; wrapper v7 rapatrié et relu au head.

Vérifié

• find_lake_root while True : pas de boucle infinie — garde parent == d → break lue au head (wrapper_head.py), le plafond arbitraire range(12) (qui arrêtait la recherche 12 niveaux au-dessus du notebook, ratant des lakes plus hauts) est correctement remplacé. OSError → break conservé.
• Échec visible au lieu du fallback stub (#16181) : return 2 + message stderr avec la mention --cwd <lake-root> ; sys.exit(main()) propage le code. C'est le cœur du fix et il est cohérent des deux côtés (wrapper v7 ET execute_notebook_wsl qui abort avant Papermill).
• Quoting : _quote_wsl_path préserve l'expansion ~ tout en shell-quotant les chemins absolus — corrige un vrai bug latent (venv avec espaces). --start-timeout {timeout} : int argparse, interpolation sûre.
• Preuve-vive CI (règle du 14/09) : le job Scripts Tests (CPU) (scripts-tests.yml) — trigger pull_request: paths: scripts/** couvre les 2 fichiers de tests ; pytest step inclut scripts/lean/tests + scripts/notebook_tools/tests ; checkout v4 complet → le wrapper testé via REPO_ROOT/MyIA.AI.Notebooks/... est bien celui du PR head ; test_entrypoint_propagates_failure_exit_code exécute réellement le wrapper en subprocess et assert exit 2 + stderr — l'assertion échouerait si la garde cassait. Le vert attendu est une vraie preuve. Le job était encore in_progress à 22:20Z (run 34903275562, started 22:16:32Z) — à confirmer avant merge.
• Security scan sur le diff : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN=, ghp_/sk-).

Mineur (non bloquant)

• setup_wsl_lean4.sh : l'heredoc WRAPPER_EOF (~150 lignes de template v5 périmé) est toujours écrit puis immédiatement écrasé par le cp $CANONICAL_WRAPPER. Fonctionnellement correct (le test test_installer_deploys_versioned_wrapper verrouille le cp), mais l'heredoc mort est de la charge trompeuse pour le prochain lecteur — candidat à une suppression dans un follow-up.

— Hermes (po-2026), head 418aa3f0, COMMENT (CoursIA cap #15511 + opener jsboige)

[jsboige]

Rerun infrastructure terminé sur la tête inchangée 418aa3f0c445c434cba00ab2a40b9dcb8aa173d8 : le child run 34903275562 est SUCCESS. Le job Scripts Tests (CPU) passe intégralement en 8m50s, y compris les tests, les floors audit/secrets/GradeBook et les post-steps. Cela confirme que le crash natif SciPy/HiGHS observé au premier passage était transitoire et hors diff ; aucun commit artificiel ni nouveau push n’a été produit. L’ancien PR gate reste un snapshot rouge gelé et est relancé séparément sur le même head.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16212 (fix(lean): resolve WSL kernel lake from notebook cwd) 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(tooling,#16176): les organes Lean natifs ne rendent plus un vert qu'ils ne peuvent pas voir #16280 partage : scripts/notebook_tools/tests/test_wsl_papermill.py, scripts/notebook_tools/wsl_papermill.py

[myia-ai-01]

Exact-head review of 418aa3f0c445c434cba00ab2a40b9dcb8aa173d8 complete.

APPROVE — the execution directory is propagated consistently through native and WSL Papermill, Lean startup now resolves a real Lake context from that directory and fails visibly without one, the wrapper entrypoint propagates failure, and the installer deploys the versioned canonical wrapper. The exact-head Scripts Tests rerun, PR gate, perimeter guard, Lean wrapper tests, and all latest checks are green.

I read the complete body, all comments, commit, full seven-file diff, exact-head structural review, inline-comment surface, and closing references. The dead installer heredoc is non-blocking technical debt because the canonical copy immediately replaces it and the deployment test pins that behavior.

This PR overlaps #16280 in wsl_papermill.py and its tests. Sequence #16212 first, then require #16280 to refresh/reconcile against the landed cwd changes before any later merge. This PR carries Closes #16181; approval does not waive issue-closure evidence/authorization discipline.