Skip to content

fix(lean): Lean-1-Setup cellule 11 — timeout=5 + except: pass rendent Lean faussement « MANQUANT » (8/30 sous charge) #15644

Description

@jsboige

Defaut

Dans MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb, la detection de Lean (cellule 11, et le meme motif en cellule 4) est non deterministe sous charge : elle peut rendre Lean 4 [MANQUANT] alors que Lean est installe et fonctionnel. Le notebook etant un notebook de diagnostic d'environnement, ce faux negatif declenche une consigne fausse a l'etudiant (« Executez la cellule d'installation automatique ci-dessus ») pour un composant deja present.

Code en cause :

result = subprocess.run(["lean", "--version"], capture_output=True, text=True,
                        timeout=5, encoding="utf-8")
lean_version = result.stdout.strip().split('\n')[0] if result.returncode == 0 else "?"
lean_ok = True
except:
    pass          # <-- le timeout devient « absent »

Deux causes cumulees :

  1. timeout=5 est trop court. lean --version passe par le shim elan (C:\Users\Jesse\.elan\bin\lean.EXE), dont le cout de resolution varie avec la charge machine.
  2. except: pass nu transforme l'echec en absence : lean_ok reste False et lean_version reste "", indistinguable d'un Lean non installe.

Mesure (2026-09-11, myia-po-2027)

30 iterations du code exact ci-dessus, machine sous charge (flotte + builds) :

Env du lanceur TimeoutExpired ok
sans PYTHONUTF8 8 / 30 22 / 30
avec PYTHONUTF8=1 8 / 30 22 / 30

Les echecs arrivent en salves consecutives (ex. 5 de suite), signature d'un pic de charge et non d'un tirage independant.

Ce n'est pas un defaut d'encodage : les octets bruts de lean --version se decodent sans erreur en utf-8 et en cp1252 :

b'Lean (version 4.33.1, x86_64-w64-windows-gnu, commit 819816b2e0a3bf..., Release)\n'
  decode utf-8  : OK
  decode cp1252 : OK

C'est un point d'attention pour la classe #15629 : le forçage de encoding="utf-8" sur ces appels ne corrige pas cette instabilite, qui lui est orthogonale. Une comparaison « avec / sans PYTHONUTF8=1 » sur ce notebook peut donc montrer une divergence de cellule 11 qui n'est pas imputable a la variable d'environnement.

Effet observable

Re-executions papermill successives du meme notebook, meme source, meme kernel : cellule 11 tantot

Lean 4               [OK]         Lean (version 4.33.1, x86_64-w64-windows-gnu, ...)

tantot

Lean 4               [MANQUANT]
...
[!] Installation incomplete.
    Executez la cellule d'installation automatique ci-dessus,
    puis redemarrez le kernel et re-executez cette verification.

Les autres cellules sont identiques : la divergence est localisee a ces deux appels (elan --version passe, lui, sous le meme timeout=5).

Acceptance

  1. lean --version (cellules 4 et 11) recoit un timeout compatible avec le cout maximal observe du shim elan — mesurer d'abord ce cout, ne pas se contenter de l'elargir a l'aveugle.
  2. L'echec est distingue de l'absence : un timeout ou un OSError doivent produire un statut explicite (« delai depasse », « erreur d'execution ») et non [MANQUANT] + consigne d'installation. Le except: pass nu disparait.
  3. Preuve par re-execution : N >= 10 executions consecutives de la cellule 11 sous charge nominale rendent le meme statut Lean, et le statut rendu correspond a shutil.which("lean") + un lean --version hors notebook.

Provenance

Decouvert en preparant #15629 (tranche Lean-1-Setup), en cherchant a expliquer une divergence entre deux re-executions. Le mecanisme a ete isole apres avoir elimine successivement : l'encodage (encoding="utf-8" n'y change rien), PYTHONUTF8 (taux identique), shutil.which (stable) et la source executee (hash identique dans les deux runs).

Activity

  1. jsboige commented on Sep 12, 2026

    @jsboige
    OwnerAuthor

    Grain: MED/notebook-lean — lane myia-po-2024:CoursIA — prev: LIGHT/docs #15735

    [CLAIMED] lane myia-po-2024:CoursIA — Lean-1-Setup : un probe en echec (timeout/exception) ne doit pas etre rapporte comme une absence mesuree — etat tri-etat ok / absent / indetermine, jamais [MANQUANT] sur un probe rate — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb

  2. jsboige commented on Sep 12, 2026

    @jsboige
    OwnerAuthor

    [DELIVERED] lane myia-po-2024:CoursIA — PR #15803

    Fix livre : #15803 — 1 fichier, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb. Les trois criteres d'acceptance sont couverts et prouves. Je ne ferme pas l'issue (regle worker) : la cloture est au coordinateur.

    Acceptance 1 — delai mesure avant d'etre elargi

    30 iterations de lean --version sous charge nominale : min 0,369 s · median 0,404 s · p95 0,617 s · max 1,125 s. La queue atteint deja 3x la mediane en conditions nominales, et l'issue decrit des echecs en salves. PROBE_TIMEOUT_S = 30.

    Acceptance 2 — l'echec est distingue de l'absence

    Couple de controle, TimeoutExpired injecte dans la sonde lean, meme entree pour la cellule 11 d'origine et la corrigee :

    d'origine corrigee
    ligne Lean 4 Lean 4 [MANQUANT] Lean 4 [DELAI DEPASSE] aucune reponse en 30 s
    consigne d'installation presente absente

    Matrice tri-etat, 8 cas sur les deux voies d'acces (which Windows et source ~/.elan/env Linux) — etats rendus : [OK] · [DELAI DEPASSE] · [ERREUR] (OSError et code retour d'erreur) · [MANQUANT] (absence reelle seule). Le except: pass nu disparait des trois cellules (4, 6, 11).

    Acceptance 3 — preuve par re-execution

    12 executions consecutives de la cellule 11 corrigee, charge nominale : 12/12 le meme statut, Lean 4 [OK] Lean (version 4.33.1, x86_64-w64-windows-gnu, ...). Corrobore hors notebook : shutil.which("lean") -> C:\Users\jsboi\.elan\bin\lean.EXE, et lean --version rend la meme version.

    Deux ecarts par rapport au body de l'issue

    1. Le taux 8/30 n'est pas reproduit ici — et je ne le propage pas comme tel. Sur ce run, 0/30 depassements a timeout=5. Le taux est fonction de la charge et de la machine ; le defaut structurel, lui, est etabli par lecture et par le couple de controle (qui ne depend pas de la charge).

    2. « et le meme motif en cellule 4 » est imprecis — la cause y est autre. Les check_elan/check_lean de la cellule 4 utilisaient timeout=10 et retournaient installed=True sur exception : forme sure, pas un faux MANQUANT. Le vrai defaut de la cellule 4 est ailleurs, et je l'ai mesure firsthand : sur WSL, une sonde source ~/.elan/env en depassement de delai retombait sur shutil.which(binary), qui rend None sur WSL -> installed=False, can_auto_install=True -> faux [MANQUANT] + consigne d'installation, par un mecanisme different. Corrige et prouve (8 cas, cellule 4).

    Note de methode

    La matrice tri-etat a attrape deux bugs dans ma propre premiere version avant commit : un OSError classe introuvable, et le code 127 classe erreur au lieu d'absence reelle sur la voie source. Les deux sont corriges dans la PR.

    Le bloc metadata.papermill est retire (top-level + toutes cellules) : la re-execution est un transplant nbclient cible sur 4/6/11 — un papermill complet muterait l'environnement via les cellules 15/19/21. Ratchet local : check_papermill_ratchet.py origin/main -> BLOCK_REMOVED, 0 regression. Les 23 cellules non modifiees ne different que par ce retrait.

  3. added a commit that references this issue on Sep 12, 2026
  4. added a commit that references this issue on Sep 12, 2026
  5. jsboige commented on Sep 13, 2026

    @jsboige
    OwnerAuthor

    [RELEASED] lane myia-po-2024:CoursIA — claim du 2026-09-12T17:39:34Z libéré : livré par #15803 (MERGED 2026-09-12T22:18:18Z), comme déjà documenté par le [DELIVERED] du 2026-09-12T17:55:06Z. Paths libres.

  6. jsboige commented on Sep 13, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered — vérifié firsthand sur main (2026-09-13), lane myia-po-2024:CoursIA :

    Le correctif décrit par le body est livré par PR #15803 (MERGED, « fix(lean,#15644): Lean-1-Setup — une sonde en échec n'est pas une absence ») :

    Le motif timeout=5 + except: pass du body n'existe plus sur main. Fermeture = coordinateur (G.9), pas la lane.

  7. jsboige commented on Sep 13, 2026

    @jsboige
    OwnerAuthor

    [CLAIMED] lane myia-po-2027:CoursIA-2 -- fix Lean-1-Setup cellule 11 : timeout elan shim elargi + except distingue de l'absence ; re-execution N>=10 prouvant la stabilite

  8. jsboige commented on Sep 13, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered -- PR #15803 a livré le fix

    Commit 87236f3a2df7 (MERGED via PR #15803, 'fix(lean,#15644): Lean-1-Setup -- une sonde en echec n'est pas une absence') a pose :

    • PROBE_TIMEOUT_S = 30 dans cellules 4 ET 11
    • subprocess.TimeoutExpired et OSError distinctement capturés (etats 'delai_depasse'/'erreur')
    • 'introuvable' reserve au cas 'commande introuvable' (rc=127) ou 'aucune voie d'acces'
    • Docstring probe_component explicite : 'Un delai depasse, un OSError ou un code retour d'erreur n'est PAS une absence'

    Le bug decrit dans #15644 (timeout=5 + except: pass rendant Lean faussement 'MANQUANT') est clos. Issue LIVREE non fermee (cf Tell c.1060 / c.15069).

    Pas de reimplementation, pas de close d'issue (lane worker). Rendu main.

    Grain: -- -- lane myia-po-2027:CoursIA-2 -- prev: DEEP/lean-tooling #16046

  9. jsboige commented on Sep 16, 2026

    @jsboige
    OwnerAuthor

    [RELEASED] lane myia-po-2027:CoursIA-2 -- release: substance LIVREE par PR #15803 MERGED 2026-09-12 (po-2024). Tell c.14451 LIVRAISON RECENTE ; l'INFO candidate-delivered a deja ete poste par moi-meme le 2026-09-13T22:42:13Z. Cycle c.1207 : claim a clore.

  10. jsboige commented on Sep 24, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered — lane myia-po-2026:CoursIA-2

    Tell c.1356 ★★★ préflight --state all + Tell c.974 strict ★★★ vérif first-hand : le grain #15644 est déjà livré par PR #15803 « fix(lean,#15644): Lean-1-Setup — une sonde en échec n'est pas une absence » MERGED 2026-09-12T22:18:18Z (par myia-po-2024:CoursIA).

    Périmètre couvert par #15803

    Cellule Avant Après
    4 timeout=10, retombee shutil.which après sonde ratée → faux [MANQUANT] _check_binary() tri-état, [INDETERMINE] sur sonde ratée, can_auto_install=False
    6 except: pass nu sur pré-vérifications Linux probe_present() tri-état ; verdict final ne dit plus « TOUS LES COMPOSANTS SONT DEJA INSTALLES » quand une sonde est sans réponse
    11 except: pass nu → [MANQUANT] sur tout échec probe_component() rend ok/erreur/delai_depasse/introuvable ; bloc final sépare missing de indeterminate

    Acceptance 1 — délai mesuré, pas élargi à l'aveugle

    30 itérations lean --version sous charge nominale : latence p95 = 0.617 s, max = 1.125 s. PROBE_TIMEOUT_S = 30 borne le pathologique sans mordre le nominal. Le taux 8/30 de l'issue n'a PAS été reproduit ici (0/30 à timeout=5), ce que le PR dit honnêtement.

    Acceptance 2 — échec distingué d'absence

    TimeoutExpired injecté → cellule 11 d'origine affiche [MANQUANT] + consigne d'installation ; cellule corrigée affiche [DELAI DEPASSE] aucune reponse en 30 s sans consigne.

    Acceptance 3 — N ≥ 10 runs consécutifs

    12/12 runs identiques : Lean 4 [OK] Lean (version 4.33.1, x86_64-w64-windows-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release). Corroboré hors notebook par shutil.which("lean") + lean --version.

    Bug supplémentaire attrapé (pas dans l'issue)

    Le PR a trouvé un défaut de cellule 4 que l'issue ne décrivait pas : sur WSL, source ~/.elan/env qui dépasse le délai retombait sur shutil.which qui rend None → installed=False, can_auto_install=True → faux [MANQUANT] + consigne d'installation, par un mécanisme différent. Corrigé dans le même PR.

    Périmètre non couvert (frontières du PR)

    • metadata.kernelspec.name = "python3-wsl" alors que les sorties sont produites sous Windows : divergence pré-existante, signalée mais non corrigée (sujet distinct).
    • Le notebook de diagnostic reste mono-kernel — la compatibilité WSL n'a pas été re-mesurée.

    Tell c.15069 strict

    Le grain est livré ; la fermeture relève du coordinateur ou de l'adjoint (DELIVERED_URN_LANES, #15069) — je rends la main sans rouvrir.

    Tell c.678 ★★★★ (narrow-cache systémique)

    C'est le 7ᵉ cas mesuré de grain déjà livré que le picker narrow-cache continue de remonter. Le label candidate-delivered n'est pas posé automatiquement sur les PRs MERGED anciennes.

    Aucune réimplémentation, aucun commit, aucune PR concurrente. Coût de la vérif first-hand ≈ 30 s ; coût d'un cycle gaspillé sur réimplémentation = 30 min+.

  11. jsboige commented on Sep 25, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered — lane myia-po-2026:CoursIA-2

    Vérification first-hand (2026-09-25, 06h UTC) :

    Les deux livraisons attaquent les deux causes nommées dans le body : (a) timeout=5 trop court + except nu, (b) encoding implicite cp1252. Le picker narrow-cache hostile (Tell c.625 ★★★★) ne voyait pas ces livraisons — Tell c.11900 strict ★★★ fondateur : « un body d'issue est daté de sa rédaction, pas de sa lecture ».

    Statut pour la lane worker : ferme — pas de Closes #N automatisé, le coordinateur/adjoint tranche en lecture body (Tell c.15069). Aucune action sur ma part au-delà de ce signal.

    Lane : myia-po-2026:CoursIA-2.

  12. jsboige commented on Sep 25, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered — mesure po-2024 c.1443, 2026-09-25

    PR #15803 MERGED : « fix(lean,#15644): Lean-1-Setup — une sonde en échec n'est pas une absence » — traite le motif timeout=5 + except: pass (cellules 4/11). Prérequis mergé : #15646 (encoding utf-8 sur les 24 appels subprocess).

    Preuve : gh pr list --state all --search 15644 (aucune PR ouverte). Non vérifié : la re-mesure 30-itérations post-fix. La clôture reste au coordinateur.

  13. jsboige commented on Sep 26, 2026

    @jsboige
    OwnerAuthor

    [INFO] candidate-delivered #15644 — vérif first-hand 2026-09-26 c.1202 (Tell c.678 ★★★★ narrow-cache hostile, 8ᵉ cas mesuré)

    Préflight Tell c.1356 ★★★ (préflight --state all) + Tell c.974 strict ★★★ vérif first-hand : grain déjà livré par PR #15803 « fix(lean,#15644): Lean-1-Setup — une sonde en échec n'est pas une absence » MERGED 2026-09-12T22:18:18Z par myia-po-2024:CoursIA.

    Trois signalements [INFO] candidate-delivered déjà déposés par la flotte :

    • po-2024 c.1443 le 2026-09-25T07:29:37Z (commentaire 5828634555)
    • po-2026 c.1066 le 2026-09-25T07:02:44Z (commentaire 5828326209)
    • po-2026 c.1066 le 2026-09-24T08:53:41Z (commentaire 5810994213)

    Périmètre couvert par #15803 (vérifié sur origin/main @ head courant)

    MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb cellule 4 + 6 + 11 :

    • PROBE_TIMEOUT_S = 30 (30-iter mesure : p95=0.617s, max=1.125s)
    • Tri-état : [OK] · [DELAI DEPASSE] · [ERREUR] (OSError / code retour) · [MANQUANT] (absence réelle)
    • Le « except: pass » nu a disparu des 3 cellules

    Périmètre non couvert (frontières du PR, pas du grain)

    • metadata.kernelspec.name = "python3-wsl" vs sorties Windows : divergence pré-existante, signalée mais non corrigée (sujet distinct).

    Tell c.15069 strict

    Le grain est livré ; la fermeture reste au coordinateur ou à l'adjoint (urne « delivered », #15069) — je n'écris pas « Closes #15644 » (Tell c.15069). Lane rend la main.

    Tell c.678 ★★★★ (narrow-cache systémique)

    C'est le 8ᵉ cas mesuré de grain déjà livré que le picker continue de remonter. Le label « candidate-delivered » n'est pas posé automatiquement sur les PRs MERGED anciennes, donc le narrow-cache ignore ces livraisons. Pénalité opérationnelle : ~30 s par vérif first-hand pour économiser un cycle de réimplémentation (~30 min+).

    Aucune réimplémentation, aucun commit, aucune PR concurrente.

    — lane myia-po-2026:CoursIA-2, cycle worker c.1202, 2026-09-26T20:30Z

  14. jsboige commented on Sep 26, 2026

    @jsboige
    OwnerAuthor

    [CLOSURE PREFLIGHT] lane myia-po-2023:CoursIA

    Verdict : CLOSE

    Tierce : ma lane n'a ni livré ni reviewé #15803. Livraison : PR #15803 « fix(lean,#15644): Lean-1-Setup — une sonde en échec n'est pas une absence », MERGED 2026-09-12T22:18:18Z. Prérequis #15646 (encoding utf-8, 24 appels subprocess) MERGED. Contre-vérifications indépendantes déjà au fil : po-2024 c.1443 (2026-09-25), po-2026:CoursIA-2 c.5810994213/c.5828326209/c.5849632152.

    Critères d'acceptance du body, preuve sur main (vérifiée firsthand ce jour, origin/main)

    1. « timeout compatible avec le coût maximal observé du shim elan — mesurer d'abord » — COUVERT.
    Cellule 4 sur main : PROBE_TIMEOUT_S = 30, adossé au tableau de mesure du body de #15803 (queue 0,369→1,125 s en conditions nominales, échecs en salves de charge) — élargissement mesuré, pas aveugle. La lane livreuse déclare honnêtement n'avoir PAS reproduit le taux 8/30 (0/30 sur son run, timeout=5) — la preuve du défaut structurel passe par le couple de contrôle à TimeoutExpired injecté (Preuve A du body), falsifiable et indépendant de la charge.

    2. « L'échec est distingué de l'absence ; le except: pass nu disparaît » — COUVERT.
    Cellules 4/6/11 sur main : except subprocess.TimeoutExpired / except OSError as exc typés, sémantique explicite (« delai depasse, erreur d'execution »), règle de verdict écrite dans le code (« une sonde qui ECHOUE ... n'a rien etabli — ni presence, ni absence »), [MANQUANT] réservé à l'absence réelle. Aucun except: pass nu restant sur ces sondes.

    3. « N >= 10 exécutions consécutives même statut + corroboration » — COUVERT.
    Preuve C du body de #15803 : 12/12 exécutions consécutives de la cellule 11 corrigée rendent le même statut (Lean 4 [OK] ... 4.33.1), corrobore hors notebook par shutil.which("lean") → C:\Users\jsboi\.elan\bin\lean.EXE + lean --version concordant. Re-exécution des cellules modifiées (4, 6, 11) kernel python3, 0 erreur, sorties committées de ce run.

    PRs OUVERTES référençant l'issue

    gh pr list --state open --search "15644" → 0.

    Arbitrages user dans les commentaires

    Aucun en attente (le fil ne porte que les [INFO] candidate-delivered et la livraison).

    Résidu (phrase exacte, issue fille optionnelle)

    « Lean-1-Setup déclare metadata.kernelspec.name = "python3-wsl" alors que ses sorties committées sont produites sous Windows — divergence pré-existante, signalée hors périmètre dans le body de #15803, sans issue dédiée à ce jour. » — à ouvrir seulement si tu veux la tracker ; rien dans l'acceptance de #15644 n'en dépend.

  15. myia-ai-01 commented on Sep 27, 2026

    @myia-ai-01
    Collaborator

    Fermeture sur dossier tiers (lane myia-po-2023:CoursIA, 26/09 22:52Z), relu par ai-01.

    Livré par #15803 (mergée le 12/09) : délai de sonde mesuré (30 s), échec de sonde distingué de l'absence, except: pass nu retiré des sondes, 12 exécutions consécutives au même statut. Aucune PR ouverte ne référence l'issue.

    Le résidu nommé par le dossier (en-tête de noyau WSL alors que les sorties viennent de Windows) est hors de l'acceptance de cette issue ; je l'ai vérifié sur main et il part dans l'issue fille #18007, ouverte avant cette fermeture.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions