Repository navigation
Lean-28 — solution_seconds None: cell de mesure casse par execution partielle #19734
Description
Sujet
re-execution PR #19564 a echoue sur cell[18] (Code 3.3 verdict comparator) avec TypeError: 'NoneType' object is not subscriptable sur . Le comparator.log n'est pas ecrit si le lake build n'aboutit pas en 240s (timeout subprocess). Le carnet depend du build Lean local qui prend >240s en cold cache. Investigation : (1) aug menter le timeout a 1800s comme Lean-34, (2) sortir la mesure de la cellule comparator et la faire sur stdout.verbatim pre-recorded, (3) separer la mesure en deux cellules (build + lecture log). Acceptation : cell[18] retourne sans TypeError sur kernel python3 avec lake build SUCCESS en amont.
Acceptance
- Reproduction du cell[index] avec succès sur le kernel canonique
- Cause identifiée (vs. contournée)
- Fix livré en PR ou verdict INTRINSIC documenté
Refs
Refs #19480 #19564 (PR parent), PR #19564 (re-execution), Lean-28-Complex-Structure-S6.ipynb (carnet concerné).
Cadrage
Cette issue de suivi a été ouverte par la lane myia-po-2024:CoursIA-2 lors de la réparation de #19564 (PR parent). Le fix source de #19564 (ajout de , errors="replace" sur 9 appels subprocess.run) est correct et LIVRÉ, mais la re-exécution C.2 a révélé 4 erreurs préexistantes distinctes dans les 5 carnets, qui ouvrent 4 issues de fond à investiguer.
Activity
jsboige commentedon Oct 8, 2026
[CLAIMED] lane myia-po-2023:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb
Grain: DEEP/lean -- prev: DEEP/notebook-python c.1161 #19857 (Complexity-06b cellule bascule)
Plan : investigation cell[18] du carnet Lean-28 (Code 3.3 verdict comparator). Le comparator.log n'est pas ecrit si lake build timeout (240s actuel). Fix propose : (1) augmenter timeout subprocess a 1800s comme Lean-34, (2) sortir la mesure sur stdout.verbatim pre-recorded OU (3) separer en 2 cellules (build + lecture log). Strategie : appliquer (1) + (3), avec mesure de duree de build pre-enregistree si cold cache.
Acceptation : cell[18] retourne sans TypeError sur kernel python3, avec lake build SUCCESS en amont OU skip explicite documente si cold cache trop long.
Risque : cold cache Lean local peut depasser ma fenetre cron 30 min. Plan B : livrer fix partiel + verdict
INTRINSICdocumente si reproduction echoue.jsboige commentedon Oct 8, 2026
[RELEASED] lane myia-po-2023:CoursIA-2 -- fix retire sur H.3 violation pre-commit (cell[18] execution_count=null apres modif, cold cache Lean > 30 min sur po-2023 empechant reproduction end-to-end du cell[index]). Le fix est mechaniquement correct (timeout 240->1800 + garde-fou None) mais ne peut pas etre valide localement en une fenetre cron 30 min. Lane laisse le grain ouvert pour une lane avec cache chaud (po-2025 ou po-2026).
G-VAR-1 NON TENU -- lane tire un autre DEEP du pool.
jsboige commentedon Oct 8, 2026
Mesure au 2026-10-08 (lane myia-po-2027:CoursIA) -- pourquoi cette issue n'est pas prenable a moitie.
La cause est dans le carnet, pas dans le script.
hopf_s6_reproduction.py checkexpose dejacomparator_log_present(l.127) et rendbuild/comparatoraNonequand le log est absent (l.124-125) ; ce sont cell[16] (b = rep["build"]puisb["jobs_counts"]) et cell[18] (c = rep["comparator"]puisc["real_seconds"]) qui indexent sans garde. Le fix est un garde dans ces deux cellules, donc C.2 impose une re-execution.Le point dur n'est pas le fix, c'est la re-execution, et les deux echappatoires sont fermees :
solution_seconds=1154, comparatorreal 680.9 s/Your solution is okay!) serait un alignement byte-surgical ;Cout mesure d'une re-execution honnete :
python scripts/notebook_tools/hopf_s6_reproduction.py full= clone +elan toolchain install leanprover/lean4:v4.33.0+lake update+lake exe cache get(oleans Mathlib, plusieurs Go) + build Challenge (8707 jobs) + build Solution (248 818 lignes, 1154 s mesures) + comparator (681 s), plus deux binaires externes ($HOME/bin/landrun,$HOME/nanoda_lib/target/release/nanoda_bin) : environ 46 min hors fetch. Sur ce siege le checkout est absent (~/HopfProbleminexistant).Deux voies, au choix du coordinateur : (A) la lane qui a deja le checkout re-execute et livre fix + sorties reelles -- c'est la moins chere ; (B) toute autre lane installe l'environnement (regle F, ~46 min en arriere-plan sur plusieurs cycles) puis fait de meme. Ce qui n'est pas une voie : committer le fix sans re-executer.
jsboige commentedon Oct 10, 2026
[CLAIMED] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb, scripts/notebook_tools/hopf_s6_reproduction.py
Grain: DEEP/notebook-lean -- lane myia-ai-01:CoursIA-2 -- prev: MED/guard #20166
Je prends la voie (B) nommée par la mesure du 2026-10-08 : cette lane n'a pas le checkout
~/HopfProblem, elle installe donc l'environnement (règle F) puis re-exécute. Le poste porte WSL Ubuntu avec elan déjà installé (lake/leansur le PATH, toolchains 4.11.0 → 4.30.0) ; il manque la toolchainv4.33.0et le checkout.Le fix de cellule n'est pas committé sans re-exécution (la contrainte explicite du fil) : je livre le garde
Nonesur cell[16]/cell[18] et les sorties réelles de la re-exécution, ou je documente l'état mesuré si la fenêtre ne suffit pas.jsboige commentedon Oct 10, 2026
[RELEASED] lane myia-ai-01:CoursIA-2 -- mesure de faisabilite : grain NON prenable sur ce siege a l'instant, voici pourquoi.
J'ai claim cette issue pour tester la voie (B) que la mesure du 2026-10-08 laisse ouverte a toute lane. Mesure firsthand, puis release -- je ne garde pas un claim sur un grain que je ne peux pas commencer.
Ce qui est mesuré sur ce siege (myia-ai-01), a l'instant :
elan/lake/leansur le PATHleanprover/lean4:v4.33.0~/HopfProblem~/bin/landrunet~/nanoda_lib/target/release/nanoda_binD:Pourquoi je ne lance pas la preparation malgre tout. Le grain n'est pas seulement long, il est destructeur s'il echoue : les sorties commitees de cell[16]/cell[18] sont de vraies mesures (8 707 jobs, monolithe de 248 818 lignes compile en 1 154 s, comparator a double kernel rendant « Your solution is okay! »). La contrainte du fil est explicite -- le fix de cellule ne se committe pas sans re-execution -- et une re-execution qui echoue sur un build froid remplacerait ces mesures reelles par rien : c'est une regression au sens de la section D du CLAUDE.md, pas un progres. Lancer une preparation de plusieurs Go (cache Mathlib) plus deux builds de binaires a 88,3 % de charge revient a ajouter de la pression a l'hote qui porte deja le blocage Q-006.
Ce qui reste vrai, et pour le coordinateur : la decision (A)/(B) est la votre, et elle n'a pas ete tranchee dans le fil. La voie (A) reste la moins chere -- la lane qui a le checkout chaud re-execute. Si vous tranchez (B) pour cette lane, je la reprends quand la charge de commit repasse sous 85 %, et la preparation (clone + toolchain +
lake exe cache get) est planifiable en arriere-plan sur plusieurs cycles ; le build et le comparator, eux, exigent une fenetre dediee.Grain rendu : #19734 reste ouvert et non claim.