Repository navigation
[Lean-37] Re-executer le carnet Capstone Serre100 apres fix raw-strings (#19628) #19730
Description
Activity
[CLAIMED] lane myia-po-2023:CoursIA-2 — re-execution du capstone Lean-37 (outputs C.2 + preuve check_equivalence) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb
Deconfliction : la PR #19628 de la lane myia-ai-01:CoursIA-2 porte sur Serre100/01-corps-finis-borne-hasse.ipynb, pas sur le capstone. Perimetres disjoints, partition par fichier.
Mesure firsthand sur
main(1fa9ae8143) : la re-execution ne peut pas satisfaire le critere 1 aujourd'hui, et ce n'est pas le carnet qui est en cause.La source des deux avertissements est un autre fichier. Le capstone lit les carnets de la sous-serie et les passe a
ast.parse; il herite donc de leurs avertissements. Scan local de chaque cellule de code deSerre100/*.ipynb(warnings.catch_warnings+ast.parse) :01-corps-finis-borne-hasse.ipynb, cellule 14 : deuxSyntaxWarning, sur\spuis\l— exactement le fichier et la cellule que corrige la PR fix(lean,#19581): Serre100/01 raw-strings suppriment les SyntaxWarning Python 3.12+ #19628 ;08-serre-dans-mathlib-Lean.ipynb: 14 cellules rendent uneSyntaxError(code Lean, hors grammaire Python) — attendu, deja documente par le carnet, et sans effet sur le present critere.
#19628 est encore ouverte. Tant que son correctif n'est pas sur
main, re-executer le capstone reproduit les deux memes lignes : le critere « 0 ligne stderr » est inatteignable, non par un defaut du carnet mais par une dependance externe. Je rends donc le claim plutot que de geler le grain.Ce qui reste a faire est mecanique, et le carnet ne demande aucun cache Lean.
Lean-37-Capstone-Serre100.ipynbporte 4 cellules de code, toutes en Python pur (aucun appel alake, aucun WSL) : lecture des carnets de la sous-serie, deux recensements, une regeneration de table. La suite tient en trois gestes, a jouer une fois #19628 surmain:- re-executer le carnet (kernel
python3-lean) et verifier 0 ligne deSyntaxWarning; - rejouer
scripts/notebook_tools/check_equivalence.py --notebook Lean-37-Capstone-Serre100.ipynb --base-url https://jsboige.github.io/CoursIA; - committer les sorties reelles.
Toute lane peut le prendre : la contrainte de cache chaud qui bloque les grains
notebook-leande cette flotte ne s'applique pas ici.[CLAIMED] lane myia-po-2023:CoursIA-2 -- re-execution Lean-37 Capstone Serre100 (c.1178, post-#19628-MERGE 10:42:38Z -- prérequis levé) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb
Vérif firsthand (c.1178) :
git merge-base --is-ancestor 1fa9ae8143 origin/main= exit 0 ;git log origin/main -- MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/01-corps-finis-borne-hasse.ipynb= commitd6eb1ce50b(Fix(lean,#19581): Serre100/01 raw-strings sur \sqrt et \leq — supprime les SyntaxWarning Python 3.12+ (#19628)) -- 12 cellules, 0 SyntaxWarning sur ast.parse + warnings.catch_warnings.Re-exécution Papermill kernel
python3en cours (run background bxy12xee8, timeout 600s). Acceptance : 0 SyntaxWarning dans les outputs + check_equivalence 20/20 EQUIVALENT + commit C.2.[INFO] Livré c.1178 — PR #19918 (DEEP/notebook-lean, lane myia-po-2023:CoursIA-2).
Re-exécution Papermill kernel
python3(timeout 600s, cwdMyIA.AI.Notebooks/SymbolicAI/Lean/) : 4/4 cellules, exec_count 1..4, 0 SyntaxWarning, 6 outputs réels C.2. La cause du FileNotFoundError anterieur etait le cwd par defaut de Papermill (racine worktree, ouSerre100n'existe pas) -- corrige viacwd=(Stop & Repair, regle 6 secrets-hygiene.md).Acceptance :
- 0 SyntaxWarning : PASS (verifie par
ast.parse+warnings.catch_warnings) - 4/4 cellules executees C.2 : PASS (table 15 carnets + 3 stubs
return NoneC.1 conformes) - check_equivalence 20/20 EQUIVALENT : RESIDU -- LOST_OUTPUTS (16/23, 7 lignes de la table a 15 carnets absentes de la page GH Pages). Cause : la page publiee contient la table a 8 carnets (etat historique), la re-publication Quarto GH Pages est externe au repo.
Acceptance finale deleguee coord/adjoint : la lane ne peut pas declencher la re-publication Quarto. Soit declencher le workflow externe, soit accepter la desynchronisation transitoire (les outputs source du notebook sont corrects).
- 0 SyntaxWarning : PASS (verifie par
{"title": "[Lean-37] Re-executer le carnet Capstone Serre100 apres fix raw-strings (#19628)", "body": "# [Lean-37] Re-executer le carnet Capstone Serre100 apres fix raw-strings (#19628)\n\n## Contexte\n\nLa PR #19628 (fix(lean,#19581)) supprime les SyntaxWarning des cellules du carnet
01-corps-finis-borne-hasse.ipynb(cellule 14, L6 et L8) en prefixant les chaines LaTeX parr(raw strings). La verification a ete faite parast.parse(source)+warnings.catch_warnings(helperscripts/notebook_tools/scan_serre100.py) sur les 15 carnets de la sous-serie Serre100/, mais les sorties committées du carnet Lean-37-Capstone-Serre100.ipynb lui-meme n'ont pas ete re-executees par cette PR.\n\n## Ce qui reste a faire\n\n1. Re-executer le carnetMyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynben local (kernel Python 3.12+) et verifier que les outputs sont exempts de SyntaxWarning.\n2. Re-jouerscripts/notebook_tools/check_equivalence.py --notebook Lean-37-Capstone-Serre100.ipynb --base-url https://jsboige.github.io/CoursIAet confirmer 20/20 EQUIVALENT.\n3. Committer les outputs reels re-executes (C.2 : notebooks committes AVEC outputs).\n\n## Acceptance\n\n- Outputs du carnet exempts de SyntaxWarning (0 lignes stderr).\n- Verdict check_equivalence : 20/20 EQUIVALENT.\n- PR dediee livree (lanemyia-ai-01:CoursIA-2probable, ou reprise par lane qui le livre en premier).\n\n## Liens\n\n- Issue originale : #19581\n- PR fix raw-strings : #19628\n- Issue parente potentielle (Lean-37) : a confirmer.\n\n## Sub-issue\n\nSans parent : #19581 (la PR #19628 a ferme le sous-ensemble raw-strings, ce qui reste est la re-execution du capstone).\n\nRefs #19628, #19581", "labels": ["lean"]}