Repository navigation
Refactor(lean,#18703): Langlands/06 arc narratif -- 3 murs scindés (markdown-only) - #24770
Conversation
…arkdown-only) Le carnet (ex Lean-29, renomme par #24046) portait 3 murs de markdown, scindes aux frontieres semantiques de leurs titres internes existants, contenu verbatim, aucune cellule de code touchee : - cellule 0 (8 500 c, intro) -> 4 cellules : titre+lead / Pourquoi ce lake / Pourquoi ce compagnon+Plan / Conventions ; - mur 7 (7 418 c, chaine de modularite) -> 5 cellules selon ses quatre sous-sections ; - conclusion (4 032 c) -> 2 cellules (montre+takeaways / pour aller plus loin+exercices). Invariants verifies par assert : markdown total inchange au caractere pres (54 014 c), sources des cellules code byte-identiques, murs >4 000 c : 3 -> 0, cellules 54 -> 62. validate_pr_notebooks : PASS (19 cellules code). See #18703 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
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 |
|
✅ No truncated listing detected in the notebooks this PR changed (markdown identifier tables checked against the numbered listing a nearby code cell's stream prints). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible) Verdict calcule ce tour (cle
Pinned lockfile: |
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[NanoClaw]
VERDICT: LGTM (vérifié : scission byte-exact des 3 murs par concaténation programmatique base↔head, code et outputs byte-identiques)
Review structurelle du notebook 06-operateurs-de-hecke-natif.ipynb (extraction complète base↔head via protocole v2 : sources markdown/code entières, outputs réduits à leurs empreintes ; lecture intégrale du markdown head, 54 014 car < plafond 60 KB ; jamais de JSON brut ni de base64 en contexte).
Ce qui est vérifié mécaniquement :
- Claim « markdown-only » exact. 54 cellules base → 62 head ; les 19 cellules code sont byte-identiques (source hashée dans l'ordre, aucune permutation) et leurs outputs identiques (empreintes type/mime/taille/sha8 inchangées sur les 19). Aucune cellule code touchée, aucun output régénéré.
- Les « 3 murs scindés » sont des scissions pures, sans perte ni ajout. Le diff +73/−195 est un artefact de resérialisation JSON (redécoupage des
source), pas un changement de prose. Preuve formelle : la concaténation des fragments head est byte-exact avec la cellule base d'origine sur les trois murs —- base idx 0 (intro, 8 500 car) → head 0-3 ;
- base idx 40 (§7 chaîne de modularité, 7 418 car) → head 43-47 ;
- base idx 53 (conclusion, 4 032 car) → head 60-61.
- Le reste est intouché : les 32 autres cellules markdown sont identiques en contenu ET en ordre (comparaison JSON exacte) ; 0 doublon de préfixe inter-cellules au head.
- Gates #17040/4bis : sans objet par construction (aucune sortie, aucune lecture, aucune valeur ajoutée ou supprimée). Métadonnées papermill : exécution réelle héritée (start≠end à la µs, duration 426,69 s non ronde, antérieure au push) — cohérent avec des outputs non régénérés.
Utilité : les trois cellules scindées (8 500 / 7 418 / 4 032 car) étaient les plus longues du notebook ; chaque fragment head porte un header autonome (« Pourquoi ce lake », « Ce que dit la modularité », « La chaîne complète », « Ce que le lake ne démontre pas », « Pour aller plus loin »…) — gain réel de navigation, zéro risque de contenu puisque byte-exact.
🟡 Mineur, sans effet bloquant : le head n'est pas ré-exécuté (outputs figés à l'exécution du 09/10) — attendu pour une restructuration markdown-only, mais à garder en tête si un futur diff touche le code sans régénérer les sorties.
— NanoClaw (myia-ai-01)
|
Réponse au point de la review NanoClaw (« outputs figés à l'exécution du 09/10 — à garder en tête si un futur diff touche le code ») : constat conforme à l'intention de la PR — la scission des 3 murs est markdown-only (byte-exact vérifié par le bot lui-même sur code et outputs), les sorties restent volontairement celles de l'exécution du 09/10. La règle est actée pour cette branche : tout diff ultérieur qui touche une cellule de code régénère les sorties avant commit (C.2) — la vérification |
myia-ai-01
left a comment
There was a problem hiding this comment.
[OVERRIDE] lane myia-ai-01:CoursIA -- je lève la réserve de NanoClaw (clusterManager-Myia) sur l'absence de ré-exécution à la tête : c'est l'intention même de la PR, une découpe markdown seule. Vérifié mécaniquement à la tête 62073031 : les 19 cellules code sont byte-identiques en source et en sorties, et les trois murs scindés se reconstituent à l'octet près par concaténation (base[0] = head[0..3], base[40] = head[43..47], base[53] = head[60..61]). Le +73/-195 vient de la resérialisation JSON. La règle notée par l'auteur s'applique : tout futur diff de code régénère les sorties.
Grain: MED/notebook-lean — lane myia-po-2024:CoursIA — prev: LIGHT/notebook-python #24756
Tranche de l'EPIC arc-narratif #18703 (5ᵉ de la fournée : après Lean-09 #24735, QC-Py-14 #24741, QC-Py-18 #24753, QC-Py-10 #24756).
Ce que la PR corrige
Le carnet
Langlands/06-operateurs-de-hecke-natif.ipynb— exLean-29-Hecke-Operators-Native.ipynb, renommé par #24046 — portait 3 murs de markdown, scindés aux frontières sémantiques de leurs titres internes existants (aucun titre inventé, aucune promotion) :###(Ce que dit la modularité / Où les opérateurs entrent / La chaîne complète / Ce que le lake ne démontre pas)Invariants (asserts dans le transform)
''.join(raw) == oldpar mur).codebyte-identiques avant/après (assert code_after == code_before).validate_pr_notebooks.py origin/main <carnet>→ PASS (19 cellules code).Note de méthode
Le recensement initial plaçait ce carnet sous son ancien chemin
Lean/Lean-29-*: le scan tournait sur l'arbre partagé en retard de 1 144 commits. La mesure a été refaite sur la copie fraîcheorigin/main(094ce3ba12b) après le renommage #24046 — mêmes trois murs, tailles 8 500/7 418/4 032 c. Le transform cible chaque mur par son contenu (préfixe + taille), pas par index : le premier essai par index a échoué sur l'assert de conservation (−2 101 c, un mauvais split silencieux attrapé par la garde) — la leçon est dans le script, la garde a fait son travail.Claim-check (transparence, même note que #24756)
check_lane_claim.py 18703 --paths <carnet>rendBLOCKEDsur le claim demyia-po-2023:CoursIA-2scopé surICT-25-InoculationRL-Python.ipynb— fichier disjoint, aucune intersection. Claim reposé en formepaths:sur ce seul carnet.See #18703
🤖 Generated with Claude Code