Skip to content

Prose de GOL-02 et Lean-39 perimee par la re-execution C.2 du lake descendu (#23164) #24232

Open

Description

@jsboige

Part of #23164 (tranche Conway). Suite de #24166, la PR qui descend le lake conway_lean sous GOL/conway_lean.

Le defaut

La PR #24166 a re-execute trois carnets parce qu'elle changeait une cellule de code (regle C.2). Deux d'entre eux portent une prose de lecture en markdown qui cite des mesures precises, et cette prose est byte-identique a la base : elle n'a pas suivi la nouvelle execution. Les cellules de code affichent donc des valeurs que le texte juste au-dessus contredit.

C'est la classe que la §C.4 appelle une derive de contenu, sauf qu'ici la cause est connue et benigne : les durees dependent de la machine, et la re-execution a tourne sur une machine plus chargee. Le remede est mecanique — realigner la prose sur la mesure fraiche, jamais l'inverse.

Aucune sortie de cellule n'est a retoucher : la mesure au head est la bonne, c'est le texte qui est perime (regle Stop & Repair respectee).

GOL-02-Golly.ipynb — 5 cellules markdown

Mesures lues dans les outputs committes au head 431f8f756c9, non recopiees d'une review.

Cellule Texte actuel (source, inchangee depuis la base) Mesure au head Ou la lire
28 « La cellule 31 (Python pur) mesure 5.10s pour advance(35,328 generations) » temps=7.29s c31
29 « ~42 jours (estimation cellule 25) » et « ~160 s pour les 100 000 premieres generations (et ~1597 s estimes pour les 33M) » ~63.7 jours ; 169.42s puis ~1694s c25, c35
32 « En ~5.1 secondes de Python pur (mesure cellule 31) » temps=7.29s c31
34 « evolue sur 1 000 generations en ~6.4 secondes (mesure cellule 33) » temps=8.16s c33
36 table : I ~5.1s, II ~6.4s, III ~160s, numpy ~42 jours ; puis « Le cout est de ~5.1s » et « ~160 s grace a la compression temporelle » 7.29 / 8.16 / 169.42 s ; ~63.7 jours ; ~1694s c31, c33, c35, c25

Deux remarques de cadrage, parce qu'elles changent le geste :

  1. La prose est deja honnete sur sa nature : chaque chiffre porte une mention « dependante de la machine » (cellules 28, 29, 32, 34). Le defaut n'est donc pas l'absence de reserve, c'est que le chiffre precis est faux. Une option plus robuste que le realignement un-pour-un serait de remplacer les valeurs par un ordre de grandeur (« quelques secondes », « les dizaines de jours ») et de renvoyer a la cellule de mesure — la §C.4 recommande de ne pas figer un nombre qui changera au prochain passage kernel. A trancher par le coordinateur ; les deux gestes sont acceptables, le statu quo non.
  2. La ligne | **Gemini 33M gen** | des dizaines de jours | de la cellule 28 reste juste avec ~63.7 jours ; seules les valeurs explicitees sont perimees, pas toutes les phrases.

Lean-39-Capstone-GOL.ipynb — 6 cellules markdown

Le carnet porte trois chiffres differents pour la meme sous-serie, dont deux etaient deja faux avant la PR (seul l'output a bouge) :

Cellule Texte actuel Verite mesuree
1 « La sous-serie GOL — neuf carnets » 10
2 « ## 2. Ou entrer : les neuf carnets » 10
5 « quels kernels tournent les neuf carnets » 10
7 « Neuf carnets, trois kernels : lean4-wsl pour GOL-03, GOL-05 et GOL-07 — … leurs cellules illisibles par ast (10, 9 et 14) » 10 carnets ; quatre lean4-wsl (GOL-03, GOL-05, GOL-07, GOL-08b) ; illisibles 10, 9, 16, 11
13 « Le README de la sous-serie annonce neuf carnets » 10
15 « sept carnets, trois kernels, quarante-trois modules de preuves » 10 carnets ; 47 modules Conway/Life

La cellule 15 (« sept carnets ») est fausse depuis sa redaction, independamment de cette affaire — elle merite sa propre correction.

Decompte mesure des kernels, sur l'arbre du head : lean4-wsl GOL-03 / 05 / 07 / 08b, python3-lean GOL-01 / 06, python3 GOL-02 / 04 / 08 / 09 — soit 4 + 2 + 4 = 10 carnets, 3 familles de kernels.

GOL/README.md est deja correct : sa table porte 10 lignes GOL-01 a GOL-09 en incluant GOL-08b, sur main comme au head. L'exercice 3 du carnet (« la table du README ne doit pas deriver ») passe donc sur ce fichier ; c'est la prose du capstone qui est en retard.

La ligne 39 de SymbolicAI/Lean/README.md (le tableau des capstones, pas GOL/README.md) annoncait « 9 carnets, 3 kernels (les trois lean4-wsl …) » : deja corrigee en 10 carnets / quatre lean4-wsl par 431f8f756c9, dans la PR #24166 elle-meme.

Pourquoi cette issue existe au lieu d'un commit

La jambe d'ecriture du serveur MCP jupyter-papermill de ce siege est morte. Mesure ce cycle, trois outils distincts, meme erreur serveur :

create_notebook -> {"error":"There is no current event loop in thread 'asyncio_0'.","success":false}
update_cell     -> {"error":"There is no current event loop in thread 'asyncio_0'.","success":false}
write_notebook  -> {"error":"There is no current event loop in thread 'asyncio_0'.","success":false}

Les lectures (read_notebook, read_cells, get_notebook_info) repondent normalement sur les memes fichiers. C'est donc un defaut du serveur (appel asyncio.get_event_loop() dans un thread sans boucle), pas un probleme de droits ni de chemin, et il ne se contourne pas depuis le depot : NotebookEdit est deny dans le harnais et l'edition manuelle du JSON d'un carnet est explicitement interdite.

Quatrieme cycle consecutif (c113, c115, c116, c117). Le correctif est un redemarrage de l'hote MCP, qui n'appartient pas a la lane — d'ou le registre MCP-WRITE-PO2024.

Geste attendu quand la jambe d'ecriture revient

  1. mcp__jupyter-papermill__update_cell sur les cellules listees ci-dessus, avec les valeurs du tableau — ou la version « ordre de grandeur » si le coordinateur retient cette option.
  2. Re-executer GOL-02 et Lean-39 pour que prose et output soient figes ensemble (C.2), puis committer les carnets avec leurs sorties.
  3. Refermer cette issue en citant le commit.

Aucune de ces etapes ne demande de decision de fond : les valeurs cibles sont deja mesurees et citees ici.

Controle de non-regression

  • Aucune sortie de cellule ne doit etre editee a la main (Stop & Repair).
  • GOL/README.md et SymbolicAI/Lean/README.md ligne 39 ne doivent plus bouger : ils sont alignes sur la mesure.

Activity

  1. jsboige commented on Nov 3, 2026

    @jsboige
    OwnerAuthor

    [CLAIMED] lane myia-po-2024:CoursIA -- la jambe d'ecriture MCP est revenue (sonde carnet jetable OK : create_notebook/add_cell/update_cell vivants), le geste 3 etapes de l'issue se declenche : realignement prose GOL-02 (timings -> ordre de grandeur + renvoi a la cellule de mesure, option C.4) et Lean-39 (comptes exacts : 10 carnets, quatre lean4-wsl, 47 modules), puis re-execution des deux carnets pour figer prose et sorties ensemble.

    paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/GOL-02-Golly.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-39-Capstone-GOL.ipynb -- 2026-11-03T04:35Z

  2. jsboige commented on Nov 3, 2026

    @jsboige
    OwnerAuthor

    [INFO] lane myia-po-2024:CoursIA — séquencement du geste derrière #24166 (mesuré, pas différé par commodité)

    La jambe d'écriture MCP est de retour (sonde ce cycle sur carnet jetable : create_notebook/add_cell/update_cell vivants) — la barrière qui fondait cette issue est levée. Mais le geste lui-même a une dépendance d'ordre de merge réelle, mesurée à l'instant sur l'arbre :

    Le claim reste posé. Le geste démarre au merge de #24166 (re-mesure des valeurs sur le main rafraîchi, édition des cellules via le MCP, re-exécution C.2 des deux carnets, PR dédiée refermant cette issue). Si #24166 restait ouvert >48 h, la lane relance l'arbitrage sur le dashboard au lieu d'éditer en aveugle.

    Choix documenté pour GOL-02 : timings → ordre de grandeur + renvoi à la cellule de mesure (option C.4 recommandée par l'issue, robuste aux re-exécutions), comptes (Lean-39) → réalignement exact (valeurs stables, indépendantes de la machine).

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