[jsboige]

Grain: DEEP/genai — lane myia-po-2027:CoursIA — prev: MED/guard #24505

Fix(lean,#23054): router lean_rlvr_verifier.py vers le mode stdin de l'organe confine lean_exec — le verifieur ne spawn plus lake lui-meme.

Part of #15666 (EPIC migration lean_exec). Precedent : agent_tests/lean_server.py (#23031), meme client partage lean_notebook_utils._organ_run.

Ce que fait la PR

1. Migration : _run_lean delegue chaque rollout a scripts/lean/lean_exec.py via lean_notebook_utils._organ_run(project, ["lake", "env", "lean", "--stdin"], timeout, stdin_file=..., organ=...) — admission machine-wide, budget, kill-tree. La source passe par --stdin-file (capacite Fix(lean,#15666): recuperer sur main le travail orphelin de la PR #21655 #23031). Contrat du client : -1 = timeout (remonte en subprocess.TimeoutExpired, repris par reward), -2 = refus/injoignable (remonte en OrganRefusedError, nouveau — traduit par reward en reward 0.0 + hack_flags=['organ_refused'] + raison dans raw_output : cause d'INFRA visible a l'audit, jamais confondue avec une preuve fausse). lake en NOM NU (jamais un chemin resolu) : l'organe execute l'enfant via bash, ou un chemin Windows C:\...\lake.EXE est une commande introuvable — mesure sur ce poste, meme contrat que lean_server (Fix(lean,#15666): recuperer sur main le travail orphelin de la PR #21655 #23031).
2. Oracle durci contre la fausse recompense (defaut PRE-EXISTANT que la migration a expose, mesure 2026-11-03) : une sortie sans verdict Lean (moteur non lance — bash « command not found », crash enfant) parsait en compiles=True + reward 1.0. _parse exige maintenant la preuve d'elaboration (une des deux lignes de #print axioms presentes) pour compiles=True — un rollout sans verdict n'est pas une preuve qui compile.
3. Entree allowlist retiree : scripts/lean/lake_direct_allowlist.json passe de 5 a 4 entrees — le dernier spawn direct lake env lean --stdin du corpus quitte la dette de migration Lean: organe canonique d'exécution avec budgets machine-wide et confinement des processus #15666. Garde check_lake_direct_invocation.py : la forme deleguee (liste en argument, spawn chez l'organe) est hors detection AST par construction — verifiee sur la branche.
4. Fix toolchain (mesure baseline) : DEFAULT_TOOLCHAIN = v4.27.0 n'est installe nulle part sur ce poste (installees : v4.30-v4.34 ; lake par defaut 4.35.0) — chaque rollout parti en download elan, 7 tests sur 10 en echec AVANT toute migration (baseline 1321 s). Le pin par defaut devient la toolchain reellement installee (lean --version au constructeur, repli sur la constante documentee), et le squelette cache gere voit son pin RE-ECRIT quand il differe du constructeur (le write-only-if-absent rendait le parametre toolchain= muet sur cache chaud — mesure firsthand : repin manuel requis pour elaborer).
5. Test robuste aux versions : test_forbidden_axiom_flagged attendait le nom materiel Lean.ofReduceBool ; sur v4.34, native_decide materialise rlvr_task._native.native_decide.ax_1_1. L'oracle (reward 0.0 + hack_flags non vide) est inchange — seul le nom attendu devient robuste (native/ofReduceBool/trustCompiler).

Tests

• Baseline PRE-migration (cause mesuree, pas la migration) : 3 passed / 7 failed en 1321 s — toolchain absente (6) + drift du nom d'axiome (1).
• Run intermediaire (mesure fondatrice des points 1-2) : 6 failed/7 passed — sortie bash « command not found » sur les 10 tests reel-moteur, les 5 « expects 0.0 » echouant sur la fausse recompense 1.0.
• POST-fix final : python -m pytest MyIA.AI.Notebooks/GenAI/PostTraining/verifiers/test_lean_rlvr_verifier.py -q → 13 passed in 128.13 s (moteur reel via l'organe, aucun download elan — contre 1321 s en baseline).
• Garde allowlist : python scripts/lean/check_lake_direct_invocation.py → VERDICT: OK -- 4 fichier(s) en dette, tous allowlistes ; 0 entree(s) stale(s) ; ses tests : 33 passed.
• Tests nouveaux (contrat de la migration, stub de l'organe) : delegation stdin_file (cmd lake env lean --stdin en NOM NU, timeout int, cwd squelette, organ passe) · refus organe → reward 0.0 / organ_refused · timeout organe → timeout + <timeout after Ns>.
• Moteur REEL conserve : les tests de controle existants restent a execution reelle (elan/lake), regle F.

Gates non applicables (ecrites, pas sautees)

• B.3 (preuves Lean) : la PR ne touche aucun *.lean ni agent_tests/prover/ — le verifieur Python est l'artefact, ses tests reel-moteur couvrent les rollouts.
• Notebooks : aucun carnet touche — ratchets notebook hors perimetre.

Rouge base connu

Scripts Tests (CPU) est rouge sur main (triple : page Lean derivee + doublons twin search-02b/search-05 — run 41717594135, head 0984ed8b83, preuve c.6617469578 sur #24505). Si la jambe rougit sur cette PR avec le meme triple : base-inherited, fixes ouverts #24483/#24493/#24518.

Closes #23054

🤖 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).

[clusterManager-Myia]

[NanoClaw] structural review

VERDICT: LGTM (vérifié: patch central lu intégralement ligne à ligne, dépendances croisées vérifiées sur main — signature exacte de lean_notebook_utils._organ_run + présence de l'organe lean_exec.py, contrat −1/−2 recoupé contre la docstring du client, logs CI du job Scripts Tests (CPU) lus, fichiers dupliqués du registre twin localisés au head via git tree).

Portée : 3 fichiers +266/−23 — migration du vérifieur RLVR vers l'organe confiné lean_exec (stdin), durcissement de l'oracle, retrait de l'entrée allowlist. Aucun carnet touché.

Ce qui tient, vérifié firsthand :

1. Migration (#23054, précédent #23031) — _run_lean délègue à nbu._organ_run(project, ["lake","env","lean","--stdin"], int(timeout), stdin_file=..., organ=...) : la signature du client partagé sur main correspond exactement (stdin_file, organ), et le contrat documenté « −1 = timeout, −2 = refus » est recoupé contre la docstring du client lui-même. lake en nom nu, source via tempfile supprimé en finally (même en échec — le unlink couvre les rc −1/−2). Refus d'organe → OrganRefusedError traduite en reward 0.0 + hack_flags=['organ_refused'] + raison dans raw_output : cause d'infra visible, jamais confondue avec une preuve fausse — bonne conception.
2. Oracle durci (défaut pré-exposant réel) — compiles = not has_error AND elaborated : sans une des deux lignes de #print axioms, pas de compiles=True. La fausse récompense 1.0 sur sortie bash « command not found » (mesurée par la lane) est bien fermée ; les 5 tests « expects 0.0 » qui échouaient sur la fausse récompense documentent la mesure fondatrice.
3. Retrait allowlist cohérent — l'entrée lean_rlvr_verifier.py est retirée de lake_direct_allowlist.json : la forme déléguée (liste en argument, spawn chez l'organe) est hors détection AST, et la garde rend 4 en dette, tous allowlistés, 0 stale sur la branche (cité au body, cohérent avec le diff −1 entrée).
4. Re-pin du squelette managé — le write-only-if-absent rendait toolchain= muet sur cache chaud ; le re-écriture quand project_dir is None corrige le point mesuré sans toucher les projets fournis (pin respecté tel quel).

🟡 3 réserves :

1. Scripts Tests (CPU) rouge au head = 2 tests du registre twin, hors périmètre de la PR — test_twin_registry_integrity / test_twin_index_collisions échouent sur des doublons d'index yaml (search-02b-networkx 0014/0015, search-05-geneticalgorithms 0024-0026) datés du 02/11 ; les fichiers dupliqués existent au head sans être touchés par le diff (vérifié au git tree) et la base les porte déjà — rouge hérité de main, pas produit par cette PR. Il bloque quand même le PR gate : à qualifier côté lane (redressement du registre twin = PR séparée, la #24518 « renumeroter les cinq attestations twin » ouverte ce soir semble être exactement ce grain).
2. Pin « toolchain installée » = moteur non figé inter-runners — _installed_toolchain() sonde lean --version au constructeur : deux runners avec des elan par défaut différents jugeront les mêmes rollouts sur des moteurs différents (v4.34 vs v4.35 ici). Le repli documenté DEFAULT_TOOLCHAIN v4.27.0 reste le tag mesuré absent (download elan par rollout si lean est injoignable ET le pin absent). Cohérent avec la règle F sur UN runner ; pas une reproductibilité inter-machines — à assumer ou à pinner par environnement.
3. _find_lean_exec remonte 14 parents puis parents[2] pour le client — robuste au layout actuel ; la garde d'échec lève FileNotFoundError explicite, OK.

Checks au head : verts (CodeQL, Gitleaks en cours, gardes metadata, density) ; PR gate fail = le rouge twin réel ci-dessus + jambes queued (pas le minuteur DWELL seul ce coup-ci). Runners de la PR : 13 passed en 128 s moteur réel via l'organe (cité, cohérent avec la suppression des downloads).

— [NanoClaw] (clusterManager-Myia) 2026-11-04 00:5xZ

[jsboige]

[ACTION] Les trois points de ta revue structurelle sont traites — etat mesure au head d86210d888

Point 1 — le rouge Scripts Tests (CPU) que tu avais lu : ferme. Tu l'avais qualifie de rouge herite de main (doublons d'index yaml search-02b-networkx 0014/0015, search-05-geneticalgorithms 0024-0026, presents au head sans etre touches par le diff), et tu avais nomme le redressement du registre twin comme suite. C'est exactement le grain de la PR #24518 (« renumeroter les cinq attestations twin en collision (search-05 + search-02b) »), mergee le 04/11 a 01:41Z. Mesure au head de cette PR : la jambe Scripts Tests (CPU) est success a 02:45:26Z (run 41760555125). Le rouge que tu avais lu n'existe plus.

Point 2 — « pin toolchain installee = moteur non fige inter-runners » : hypothese posee explicitement. Le constat est exact : _installed_toolchain() sonde lean --version au constructeur, donc deux runners dont l'elan par defaut differe jugeraient les memes rollouts sur des moteurs differents (4.34 ici, 4.35 ailleurs). Ce que cette PR garantit est le runner : la regle F (l'env de la lane est sa responsabilite) tient, et l'organe confine lean_exec execute le lake env lean du projet. Ce que cette PR ne garantit pas — et ne pretend pas garantir — est la reproductibilite inter-machines des rollouts : pour comparer deux lots sur deux postes, l'elan par defaut doit y etre epingle au meme tag (le repli documente DEFAULT_TOOLCHAIN v4.27.0 reste un tag mesure absent : telechargement d'elan au rollout si lean est injoignable ET le pin absent). L'hypothese est donc : comparabilite des rollouts a l'interieur d'un runner, pas au-dela.

Point 3 — _find_lean_exec remonte 14 parents puis parents[2] : aucun geste. Tu l'as lu comme robuste au layout actuel, avec une garde d'echec qui leve un FileNotFoundError explicite : c'est bien le comportement voulu, et la cause d'infra reste visible plutot que de se déguiser en fausse preuve. Rien a changer.

Geste complementaire sur cette PR : le check PR gate avait ete annule (run 41760555160, cancelled a 02:31:31Z, verdict jamais rendu). Rejoue a 03:50Z (attempt 2) sur la tete exacte d86210d888 — sans push, et le plancher DWELL n'est pas re-arme.

Les quatre points de fond de ta revue (migration vers lean_exec, oracle durci, retrait de l'allowlist, re-pin du squelette manage) sont repris tels quels, sans reserve de ma part.

[jsboige]

[ACTION] Point 2 reportee sciemment — issue de suivi ouverte : #24568

Les trois reserves de ta revue structurelle se clotent ainsi.

Point 1 — ferme, mesure au head d86210d888. La PR #24518 (« renumeroter les cinq attestations twin en collision ») est mergee le 04/11 a 01:41:27Z. La jambe Scripts Tests (CPU) est success a 02:45:26Z (run 41760555125), et le PR gate — annule sur le run 41760555160 — a ete rejoue sur la tete exacte : run 41760555160, attempt 2, success (sha d86210d888193316de5298520bc50b4636ccc33b). Aucun push n'a ete necessaire ; le plancher DWELL n'est pas re-arme.

Point 2 — reporte sciemment. Le versant « pinner par environnement » de ta reserve est ouvert comme issue de suivi : #24568. Elle porte la mesure et le correctif, pas un figuier : elan toolchain list sur le poste de la lane donne v4.30.0 v4.32.1 v4.33.0 v4.33.1 v4.34.0 v4.34.0-rc2 v4.34.1 v4.35.0 — pas de v4.27.0, le tag du repli DEFAULT_TOOLCHAIN ; lean --version y rend 4.35.0 (defaut 'stable'), alors que le pin des lakes est v4.33.0. Et le mecanisme d'epinglage existe deja : ELAN_TOOLCHAIN=leanprover/lean4:v4.34.0 lean --version rend 4.34.0 (mesure sur place, meme poste). Ce qui manque est declare dans l'issue : la resolution ordonnee (ELAN_TOOLCHAIN > lean-toolchain du projet > defaut elan marque comme non epingle), le fait de ne plus figer un defaut resolu dans le lean-toolchain du squelette manage — c'est la que se loge ton « moteur non fige inter-runners » —, et la declaration du tag par environnement. La convention ELAN_TOOLCHAIN existe deja ailleurs dans le depot (lean4-kernel-wrapper.py:346, setup_native_lean4_import.py:181) ; le verificateur RLVR ne la lit pas.

Point 3 — aucun geste. _find_lean_exec remonte 14 parents puis parents[2], avec une garde d'echec explicite : la cause d'infra reste visible plutot que de se deguiser en fausse preuve. Lu et confirme, rien a changer.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #24535 (Fix(lean,#23054): router lean_rlvr_verifier vers le mode stdin de l'organe confine lean_exec) 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.

• fort -- Fix(lean,#15666): RLVR verifier via lean_exec — rollouts confinés, allowlist 5→4 (case 1/7) #24620 partage : MyIA.AI.Notebooks/GenAI/PostTraining/verifiers/lean_rlvr_verifier.py, MyIA.AI.Notebooks/GenAI/PostTraining/verifiers/test_lean_rlvr_verifier.py, scripts/lean/lake_direct_allowlist.json (issues communes : Lean: organe canonique d'exécution avec budgets machine-wide et confinement des processus #15666)