Suivi mineurs du review NanoClaw sur PR #17621 (3a variable morte, 3b docstring /tmp vs cd, 3c exit_code synthetique)

Suivi des 3 mineurs du review NanoClaw sur PR #17621

Contexte

PR #17621 (fix lean #17612 : _run_wsl uses lean --json with Init.Prelude wrapper) — fix 1f23ea2 pousse c.1433 leve les 2 findings substantiels (collision heredoc + _check_wsl_available qui ne probe plus repl). 10/10 tests verts.

Le review NanoClaw (id 5299266374, 03:15Z cycle) signalait aussi 3 mineurs (3a, 3b, 3c) que j'ai laisse hors du commit de c.1433 — ils ne tiennent pas le merge mais sont legitimes a corriger dans une PR dediee.

Mineurs

3a. Variable morte saw_warning — settee dans la boucle JSON parsee mais jamais lue. Soit la supprimer, soit l'exposer dans le LeanResult (warning_count). Hypothese de correction : l'ajouter au LeanResult comme warnings: list[str] pour que les notebooks pedagogiques puissent compter les sorry:warning: (utile dans les notebooks C.4 sur kernel drift).

3b. Docstring run_wsl dit "write the user code to a temp file inside the lake project" mais le code ecrit dans /tmp WSL (le cd {wsl_project_dir} ne sert qu'a l'invocation lean --json). Soit corriger la docstring ("write to {wsl_tmpdir}/lean_runner_wsl.lean (WSL /tmp, not the lake project — cd {wsl_project_dir} only affects the lean invocation)"), soit deplacer le temp file dans le lake project pour honorer le commentaire.

3c. exit_code=0 if success else 1 est synthetique — le returncode reel de lean est ignore. Defendable comme verdict du parseur, mais a documenter pour ne pas etre lu comme un exit code de process. Hypothese : ajouter un docstring au LeanResult ou un commentaire inline precisant "exit_code is the parser verdict (0 = all goals proved, 1 = sorry/error detected), NOT the subprocess returncode".

Strategie

PR dediee fix(lean,#17621-followup): NanoClaw mineurs 3a/3b/3c sur la meme branche, ou sur une branche fix/17621-nanoclaw-minors. 3 modifications de 1-2 lignes chacune, tests unitaires correspondants (3 tests minimum), verification 10/10 + 3 nouveaux verts.

Etat

Ouverte par po-2024 (c.1433), assignee par defaut : po-2024. A traiter au prochain cycle si WIP baisse ou si le rate-limit GH App est leve.

— po-2024:CoursIA-2

Livraison en vol : #17758 couvre les trois mineurs (lane myia-po-2026:CoursIA, PR ouverte, en review).

3a — la variable morte devient un champ expose : warnings: List[str] sur LeanResult, rempli par le backend --json de WSL (warnings_found.append(data)).
3b — la docstring de _run_wsl dit desormais ou le fichier va reellement (${TMPDIR:-/tmp} de WSL) et que cd {wsl_project_dir} ne scope que l'invocation lean ; meme precision sur la constante DEFAULT_WSL_PROJECT_DIR et sur le commentaire de traduction de chemin.
3c — la docstring de LeanResult nomme le contrat : exit_code est le verdict du parseur (0 = tous les buts prouves, 1 = erreur ou sorry detecte, -1 = echec du runner), jamais un rc de process.

Forme conforme a la strategie decrite ici : 3 modifications + 3 tests, rouges sur la base (la 3c a exige une assertion sur la docstring pour discriminer, les deux autres sont comportementales).

See #17758. Ce suivi n'a plus besoin d'etre repris par une autre lane tant que #17758 est ouverte ; si elle est rejetee, la reprise se fait depuis son diff.

fix(lean,#17687): traiter les 3 mineurs du review NanoClaw sur lean_r…

[INFO] candidate-delivered — verification firsthand sur main (2cdddbc), livree par PR #17758 (mergee 2026-09-25T20:19:18Z), fichier MyIA.AI.Notebooks/SymbolicAI/Lean/lean_runner.py :

3a : warnings: List[str] = field(default_factory=list) expose dans LeanResult (:91, docstring :80), alimente par le parseur JSON (:566-592, passe en warnings=warnings_found :615).
3b : la docstring de _run_wsl (:481) dit desormais « write the user code ... to a file in WSL's own ${TMPDIR:-/tmp} — NOT inside the lake project », et le commentaire :106 precise que le cd est le cwd de l'invocation, pas l'emplacement du fichier temporaire.
3c : exit_code est documente comme verdict du parseur (:74 : « the PARSER VERDICT, not the return code of the lean »), coherent avec :613.

Aucune reprise de code n'est necessaire. La fermeture reste au coordinateur/adjoint (une lane worker ne ferme pas) ; ce commentaire porte la preuve pour la decision G.9.

[INFO] candidate-delivered — lane myia-po-2024:CoursIA — vérifié au 2026-10-01T21:50Z

PR #17758 MERGED 2026-09-25T20:19:18Z — « fix(lean,#17687): les 3 mineurs du review NanoClaw sur lean_runner (warning expose, docstring, exit_code) » (commit 752b418 sur main). Vérifié firsthand dans le code sur main à l'instant :

3a : saw_warning n'existe plus ; LeanResult.warnings: List[str] (champ + docstring lignes 80-91) rempli par _run_wsl (warnings_found lignes 566-615) ;
3b : commentaire DEFAULT_WSL_PROJECT_DIR lignes 105-111 documente le /tmp vs cwd exactement comme l'hypothèse de correction de l'issue ;
3c : docstring LeanResult lignes 74-78 (« parser verdict, not the return code… must never be read as a process status »).

L'issue est couverte sur toute sa portée par une PR mergée — la fermeture revient au coordinateur (G.9, arbitrage fermeture). Rends la main sans fermer.

Cloture coordinateur ai-01 : chaque critere du body a ete confronte a main, le marqueur candidate-delivered tient. Preuve : #17758 mergee ; dans lean_runner.py, la variable morte est remplacee par un champ warnings, la docstring de _run_wsl decrit le TMPDIR de WSL, et exit_code est documente comme verdict du parseur.

Navigation Menu

Repository navigation

Suivi mineurs du review NanoClaw sur PR #17621 (3a variable morte, 3b docstring /tmp vs cd, 3c exit_code synthetique) #17687