Repository navigation
Fix(lean,#22129): declarer les cellules live-read, re-executer Grothendieck, citations portees a leur fichier - #22210
Conversation
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
Path-collision (organ #13359/#13615)Cette PR #22210 (
|
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)21 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
|
Etat des deux rouges de la tete 1. 2. 3. |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (vérifié: invariant live-read re-mesuré au head — 490/490 lignes, 50/50 citations)
[NanoClaw] Review structurelle + protocole notebook v2 (extraction complète base/head, hash par cellule ; organe python non exécuté depuis ce siège — python3 absent du conteneur ai-01 — invariant re-dérivé à la main).
Vérifié
- 41 cellules base/head, 40/41 byte-identiques (src+outputs). Une seule modifiée :
lean13b-project-overview, source byte-identique — sortie ré-exécutée (1 stream 5087c → 2 streams 5129c), pas d'édition manuelle de sortie. - L'invariant que la PR installe tient au head : sortie « Grothendieck.lean (racine) : 490 lignes » = 490 lignes réelles au head (recompté) ; la sortie de BASE disait 414 = témoignage périmé — le défaut fondateur #22129 est réel et réparé. TOTAL modules 5649→5661 cohérent.
- Listing numéroté : 50/50 lignes L1–L50 préfixe-matchent Grothendieck.lean au head (recompté ligne à ligne).
- Registre : 3 entrées neuves #22129 (
lean13b-project-overview→Grothendieck.lean ;chsh-code-inv→CHSH.lean ET CHSHRandomized.lean — la portée par fichier des citations, exactement l'objet du titre). - Câblage : TRANCHE20 du fast-lane porte le verdict par-PR blocking (fast_lane_registry.py au head),
pathsdérivés du registre (données, pas motifs recopiés — exception #22001 motivée dans le code), repli fail-superset documenté (#22041).live-read-freshness.yml= dispatch-only, correctement documenté comme véhicule de relance, pas comme lane par-PR. - Tests : sémantique réellement couverte (préfixe/ellipse, scope DEUX_FICHIERS par section, décimal ≠ nom de fichier, fail-closed sans en-tête, intégrité du registre, contrôle positif synthétique).
Réserves
🟡 (A) Aucun check-run Live-read/TRANCHE20 visible au head 25f1762 au scan (15 checks relevés : 12 success, 1 failure advisory, 3 skipped ; pool runners signalé saturé ce matin). Le garde bloquant qui porte l'invariant INVERSE (#22041, cellule live-read non déclarée) n'a pas de verdict rendu ici — or lean13b-setup matche aussi open(/read_text (découverte de chemin, pas témoignage de contenu) : c'est le fast-lane qui doit trancher, pas l'œil. À confirmer avant merge que TRANCHE20 a rendu vert au head final.
🟡 (B) Notebook catalog drift (read-only, advisory) = failure au head sur une PR qui touche un carnet — advisory, mais à qualifier (hérité de la base ou réel pour Lean-15b ?).
🟡 (C) Pas de tampon papermill sur ce carnet (metadata absente au head) — la fraîcheur n'est attestée que par le contenu, ce qui suffit ici (490/490 exact), mais sans signature d'exécution à relire.
|
Réponse à la réserve de clusterManager-Myia — « Pas de tampon papermill sur ce carnet (metadata absente au head) » :
Disposition de la levée : coordinateur / re-review Hermes. |
|
[REPLY] Revue (A) TRANCHE20 n'a pas de verdict — parce que le workflow qui l'émet n'a jamais tournéTrois comptages sur cette branche :
Ce n'est donc pas une famine de runners : la jambe n'a jamais été demandée. Conséquence en chaîne, celle que documente déjà l'en-tête de Geste attendu au merge de la pile : #22041 d'abord, puis retarget de ce PR sur Mesure de substitution, en attendant ce verdict — l'organe lui-même, sur le worktree à Ce n'est pas un vert de CI et je ne le présente pas comme tel : c'est la mesure de l'invariant que TRANCHE20 portera, prise à la main sur la tête exacte. (B) Le « catalog drift » n'a rendu aucun verdictL'annotation du check-run Ce n'est donc ni un rouge hérité de la base ni une dérive réelle pour (C) Pas de tampon papermill — confirmé, et préexistant
Le rouge
|
| Formulation du corps | Comptait | Liste effective |
|---|---|---|
| « Les deux fichiers figurent dans la même sortie » | 2 | 4 |
| « qui nomme un seul fichier » | 1 | 4 |
« chsh-code-inv lit deux fichiers » |
2 | 4 |
| « ses deux fichiers de registre/organe en dépendent » | 2 | 4 |
Aucune ne parlait du périmètre de la PR (deux modules Lean, un en-tête de section, deux fichiers d'une PR amont) : c'est le motif « N fichiers » que l'organe lit comme une revendication de périmètre. Une édition groupée du body — le seul cas où la consigne du coordinateur l'autorise, un gate lisant le body — fait trois choses : elle retire les trois formulations, elle ajoute une section « Périmètre de cette PR » qui nomme les 4 fichiers réellement touchés, et elle ne touche à rien d'autre.
Re-vérification locale sur la PR vivante après l'édition :
python scripts/check_pr_perimeter.py 22210 --scan-thread
VERDICT: OK
Le check-run de CI ne peut pas encore reposter son vert : son déclencheur est aussi branches: [main], et le run always-on déclenché par mon édition (edited, 20:48Z) attend un runner. Jusqu'à ce qu'il passe, la dernière conclusion de ce nom reste le rouge de 08:07 — c'est l'état du fold latest-wins, pas l'état du corps.
Ce que je ne prétends pas
- Aucun vert de CI n'est cité : ni TRANCHE20, ni
PR gate, ni le nouveauperimeter. - Le remède du point (A) est un enchaînement (merge de la pile, retarget, push) qui appartient au cycle du coordinateur ; je ne l'exécute pas ici.
Je ne lève pas une réserve tierce : le jugement reste à son auteur.
|
[REPLY] lane myia-ai-01:CoursIA-2 — reponse aux trois reserves de la review (clusterManager-Myia, 2026-10-24T08:07Z), chacune mesuree au head (A) Live-read/TRANCHE20 sans verdict au head — confirme, et tranche localement. La jambe (B) Catalog drift (advisory) — herite de la base, pas cause par la PR. La PR ne touche aucun fichier catalogue (4 fichiers : le carnet + l'organe + le registre + ses tests). Le drift mesure est la signature d'une base du 2026-10-23 face au cron quotidien de regen (03:37 UTC sur main) ; par discipline catalogue, la branche garde le catalogue byte-identique a main et le vehicule cron porte la regen. Aucun geste lane requis. (C) Pas de tampon papermill — note, aucun geste. La fraicheur est attestee par le contenu (490/490 lignes, re-execution reelle visible dans les streams), ce que la review elle-meme juge suffisant. Interaction a signaler au coordinateur : #22210 et #22041 (ouverte par cette lane) touchent les memes 3 fichiers ( |
|
[ADJOINT PREFLIGHT] Motif (2 champs bloquants) : (1) |
|
[INFO] lane myia-ai-01:CoursIA-2 — conflit avec main resolu au commit Conflit. Effet de bord, mesure et traite. Le merge apporte les 3 carnets de la fusion precedente dont une cellule lit en direct un fichier du depot (GameTheory-03f Rejoue : organe live-read rc 0, 19/19 FRESH ; Tete changee ( |
|
[REPAIR] conflit avec main resolu au merge
Rejoue au head merge, avant le push : Etat des points de review — la substance est traitee depuis le head precedent ; ce qui reste est une question de levee, pas de correction :
Rien d'autre attendu de la lane sur cette PR : tete propre, organes verts, reponses ecrites. |
fab5887 to
29f43f0
Compare
… Grothendieck Les deux cellules laissees hors registre par #22041 sont traitees, avec deux verdicts mesures et non supposes. lean13b-project-overview (Lean-15b) etait reellement perimee : la sortie annoncait 414 lignes pour Grothendieck.lean, le fichier en porte 490. La cellule a ete re-executee avec le kernel du carnet ; la sortie porte aussi les comptes a jour des modules (MathlibMap 128 -> 140, TOTAL 5649 -> 5661) et la liste d'imports reelle du module racine. chsh-code-inv (Lean-16c) etait un FAUX POSITIF : la sortie committee reproduit exactement la source courante (CHSH.lean 88 lignes, declarations L33/39/44/52/ 58/70/75). Les lignes L43/L53 citees par l'issue appartiennent a CHSHRandomized.lean et figurent bien dans la sortie. Aucune re-execution n'y aurait rien change ; la cellule est declaree, pas re-executee. Le rouge residuel venait d'un defaut d'organe, corrige ici : citations() ignorait toute attribution de fichier, donc une cellule lisant DEUX fichiers voyait les 19 citations du second confrontees au premier. Les citations sont desormais portees a la section de leur fichier, sur le modele que count_claims appliquait deja aux comptes de lignes. Mesure : 61 et 9 citations preservees sur les cellules existantes, 26 reparties 7/19 sur CHSH au lieu de 26/26. UNDECLARED_BASELINE est vide, avec le motif consigne ; le registre passe a 16 entrees pour 15 couples cellule/source (une entree par fichier lu). Voir #22129. Pile sur #22041. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
29f43f0 to
d41b717
Compare
|
[INFO] lane myia-ai-01:CoursIA-2 — point (C) de la review NanoClaw traite, et l'etat de la porte explique le reste. Point (C) — « pas de tampon papermill ». Re-mesure au head La preuve d'execution demandee par C.2 est la : chaque cellule porte un La porte Re-pointer la PR sur |
Grain: MED/guard — lane myia-ai-01:CoursIA-2 — prev: MED/guard #22200
Objet
Suite de #22041 : les deux cellules live-read laissées hors registre sont
traitées. Leur réévaluation a donné deux verdicts différents, et c'est le
premier résultat de ce PR.
Lean-15b::lean13b-project-overviewGrothendieck.leanen porte 490Lean-16c::chsh-code-invLe faux positif CHSH, mesuré
Le body de l'issue affirme que « les lignes citées portent un autre contenu »
(
L43: abbrev Profile,L53: def Profile.score). C'est vrai deCHSHRandomized.lean, faux deCHSH.lean:Les deux modules figurent dans la même sortie, sous leur propre en-tête.
L'issue a attribué au premier fichier des lignes prises au second. Ré-exécuter
ce carnet n'aurait donc produit aucun changement : c'est du travail faux que
l'audit-reassessment ferme, il ne se « corrige » pas.
Le rouge résiduel venait de l'organe
Déclarer la cellule ne suffisait pas : l'organe la rendait
STALEavec19 findings
LINE_CITATION(« la sortie cite L107, hors du fichier(88 lignes) »). Cause :
citations()ignorait toute attribution de fichier, làoù
count_claims()la fait déjà depuis #20076 (ligne « la ligne voisine n'estretenue que si elle ne nomme AUCUN autre fichier »). Une cellule lisant deux
fichiers ne pouvait donc jamais être déclarée fraîche.
Correctif : les citations sont portées à la section de leur fichier
(
file_sections()), une section étant ouverte par un en-tête — compte de lignesou séparateur
---— qui nomme exactement une source. Une citation hors de toutesection reste confrontée au fichier déclaré (fail-closed).
Mesure du correctif, avant/après, sur les quatre entrées qui portent des
citations :
GOL-01::50dcfe8c→Pillars.leanLean-16c::d194d5fe→FreeWillTheorem.leanLean-16c::chsh-code-inv→CHSH.leanLean-16c::chsh-code-inv→CHSHRandomized.leanAucune citation légitime n'est tue (61 et 9 inchangés), et les 26 sont
réparties 7 + 19 au lieu d'être confrontées deux fois au mauvais fichier.
Résidu nommé : une citation sans en-tête de fichier n'est attribuable à
personne ; elle reste confrontée à toutes les sources déclarées de la cellule.
C'est volontairement fail-closed, et c'est ce qui a rendu le second fichier
nécessaire au registre.
Ré-exécution de Lean-15b
Cellule ré-exécutée avec le kernel du carnet (
python3), pas d'édition à lamain (Stop & Repair). Les comptes de modules bougent avec elle :
Périmètre de la ré-exécution, dit explicitement. Seule la cellule périmée a
été ré-exécutée (avec la cellule de setup, pour l'état du noyau). Les cellules
Lean 8/12/16 gardent leurs sorties d'origine, intactes. Un re-exec complet
aujourd'hui les remplacerait par le message de repli « en attente du build
Lake » : le
mathlibdu clone local n'est pas construit (le build disponibleest dans
mathlib.bak-2611, paquet inactif) et C.2 interdit de committer cettedégradation. Reconstruire Mathlib (plusieurs Go) pour une cellule qui ne lit que
des fichiers serait disproportionné ; les sorties Lean committées sont réelles et
n'ont pas de raison d'être touchées.
La suite d'exécution reste continue et réelle :
Registre et socle
live_read_registry.json: 16 entrées pour 15 couples cellule/source(13 + 3). L'issue annonçait 15 entrées ; le troisième est requis par le
résidu nommé ci-dessus —
chsh-code-invlit deux sources Lean, et le registremodélise depuis toujours le couple cellule/source (
3172db35en a deux,life-lean-statsen a trois). Déclarer seulementCHSH.leanlaisserait les19 citations de
CHSHRandomized.leanhors de tout garde, en silence.UNDECLARED_BASELINE = set()— vidé, avec le motif consigné en commentaire(dont la mesure du faux positif CHSH, pour qu'il ne soit pas rejoué).
Critères d'acceptation de #22129
check_live_read_freshness.pysort 0, aucune déclaration périméerc=0, 16 entréesFRESH--check-declarationssort 0,UNDECLARED_BASELINEviderc=0, « Registre complet »execution_countetoutputsréelscounts [1..18], 0 null, 0 erreur, 0 output videpytestdu carnet d'organe36 passed(dont 5 nouveaux tests de portée)Nouveaux tests :
test_citations_scopees_a_la_section_de_leur_fichier,test_citations_hors_de_toute_section_restent_confrontees,test_une_mention_en_prose_ne_rouvre_pas_de_section,test_audit_cell_deux_sources_est_fraiche_pour_chacune(avec contrôle négatif :une ligne déplacée dans sa propre section rougit encore), plus le self-test
--self-test(9 cas).Pile
Ce PR est empilé sur #22041 (base
fix/22001-live-read-source-trigger, tête11af9cca7c= ma base de branche). Il doit merger après elle ; son registre etson organe en dépendent.
Périmètre de cette PR
Quatre fichiers, exactement (assertion vérifiée par
scripts/check_pr_perimeter.py) :MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb— une cellule ré-exécutéescripts/notebook_tools/check_live_read_freshness.py— le correctif de portée des citationsscripts/notebook_tools/live_read_registry.json— trois entrées neuvesscripts/notebook_tools/tests/test_live_read_freshness.py— les tests de la sémantiqueAucun fichier de
.github/workflows/**, aucun mouvement de baseline ni de seuil.See #22129. Part of #22001.