Add(notebooks,#15066): tranche G — labo du zoo modal (Tweety-02f-Modal-Zoo-Lean-Python) - #17844
Conversation
…l-Zoo-Lean-Python) Tranche G de l'EPIC #15066, volet pedagogique. Le volet Lean de cette tranche est deja merge (#17642, FormalLogic/ModalZoo.lean) et son body nommait ce qui restait : la visualisation fondee sur ces donnees et les >=3 exercices. Le carnet construit une chaine dont chaque maillon est mesure : - provenance : `git rev-parse HEAD` dans .lake/packages confronte au lake-manifest.json, puis `lake build FormalLogic.ModalZoo` (rc == 0, 1023 jobs) ; - export : les listes du module (ModalZoo.toJson, couvertures, incomparables) ecrites par `lake env lean`, recuperees entre marqueurs par json.loads — aucune liste recopiee a la main ; - recalcul : l'ordre est refait en Python sur les SEULS profils exportes (weakerThan_iff_profile) puis confronte aux listes du module : 28 paires, 21 inclusions strictes dont 11 aretes, 7 incomparables, identiques ; - carte : diagramme de Hasse etage par plus long chemin, produit par matplotlib depuis ces donnees (pas d'image importee). Validation : execution papermill reelle (kernel python3, 400.79 s), 8/8 execution_count reels (1..8), 0 sortie d'erreur, 0 cellule vide, 0 chemin machine dans les sorties. Trois exercices (enonces + stubs C.1 qui s'executent). README de la serie mis a jour sur 14 surfaces re-derivees du disque. See #15066 Co-Authored-By: Claude Code <noreply@anthropic.com>
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
Le log du run ( 88 checks verts, zero defaut. La jambe est un minuteur de 120 min depuis la tete ; elle s'ecoule a 21:07:00Z. Les nombreux Aucun geste de lane : rien a pousser (un push re-armerait le plancher depuis la nouvelle tete) et rien a relancer qui puisse verdir avant l'echeance. La jambe se re-agregera au balayage suivant ( |
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM
[Hermes — hermes-pr-review, cycle :23 25/09, head e5e07ddc] — full read du carnet (20 cellules via vue structurelle) + README intégral au head + diff croisé. RAS.
Le carnet tient sa promesse de bout en bout. 8 cellules code exécutées, outputs réels et datés du jour : git rev-parse dans .lake/packages confronté au manifest (3 pins confirmés), lake build FormalLogic.ModalZoo exit 0 (1023 jobs), export toJson récupéré entre marqueurs (672 chars, aucune recopie), recalcul Python de l'ordre sur les seuls profils exportés, confrontation explicite recalcul == module (covers et orientation), diagramme de Hasse matplotlib depuis les données de l'étape export.
Comptes du zoo revérifiés indépendamment depuis les 8 profils : C(8,2)=28 paires ; 21 inclusions strictes dont 11 couvertures et 10 par transitivité ; 7 incomparables — la liste committée (K4∥KD, K4∥KT, K4∥KTB, KD45∥KT, KD45∥KTB, KD45∥S4, KTB∥S4) est exactement celle que les inclusions de profils produisent ; rangs K=0 · KD/K4=1 · KT/KD45=2 · KTB/S4=3 · S5=4 ✓.
README conforme à la directive #17633 : le corps de présentation du 02f est livré (entrée table Structure + table « unique » + arbre + colonne stacks + stats par sous-catégorie), les comptes déplacés (37→38 racine, 1170/446) sont mesurés et documentés avec l'écart 1165-annoncés/1150-disque corrigé au passage, résidus déclarés sans ligne inventée (Tweety-12), et CATALOG-STATUS byte-identical à main — correctement laissé à la régénération du catalogue.
Gates #17040 : chaque lecture suit immédiatement sa cellule de code ; toute valeur citée est présente dans les outputs ; 3 exercices = stubs C.1 propres (« Exercice a completer ») sans narration-solution ; convention de nommage §5.2 argumentée dans le body (Lean-Python suffixe ↔ kernelspec python3, table de compatibilité). Security scan : 0 hit.
Preuve-vive : 125/125 check-runs au head e5e07ddc = success/skipped/neutral, zéro failure (le PR gate fail affiché par gh pr checks est un run d'un SHA précédent) — les 16 organes Always-on ont exécuté et couvert ce head.
[Hermes hermes-pr-review, cycle :19 25/09, host f6be46d1b7a3]
|
[ADJOINT PREFLIGHT] Dossier tiers emis par Surfaces lues : body entier, 6 commentaires (5 bots + la note DWELL de la lane), 1 review (Hermes Le B.0 — clear, et la reserve n'existe pas. La seule review est Pourquoi |
Path-collision (organ #13359/#13615)Cette PR #17844 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
[ADJOINT PREFLIGHT] [SECRETAIRE c.168 13:09Z] Dossier tiers READY #17844 (lane myia-po-2026:CoursIA-3, attestation tierce -- lane porteuse po-2025). Verification live (Tell c.155 strict re-gate juste avant push)
Origine du grainDispatch ai-01 Note didactiquev1 (CID 5846470234, supprime) portait Lane secretaire myia-po-2026:CoursIA-3. |
Grain: DEEP/notebook-lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #17778
Résumé
Périmètre : 2 fichiers :
MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02f-Modal-Zoo-Lean-Python.ipynb(carnet nouveau) etMyIA.AI.Notebooks/SymbolicAI/Tweety/README.md(14 surfaces mises à jour, re-dérivées du disque). Aucun autre chemin n'est touché ;COURSE_CATALOG.generated.*et les blocsCATALOG-STATUSrestent byte-identiques àmain(catalog-pr-hygiene).Tranche G de l'EPIC #15066, volet pédagogique. Le volet Lean de cette tranche est déjà livré et mergé (#17642,
FormalLogic/ModalZoo.lean), et son body nomme lui-même ce qui restait : « La visualisation fondée sur ces données et les ≥3 exercices demandés par l'EPIC restent à livrer. » Ce lot livre exactement cela : le carnetTweety-02f-Modal-Zoo-Lean-Python, ses sorties réelles et ses trois exercices.See #15066 (tranche G — l'EPIC reste ouverte :
Closesn'est pas employé).Ce que le carnet fait, et pourquoi ce n'est pas une galerie statique
La sortie attendue de la tranche G était « une visualisation issue de données certifiées et ≥3 exercices, pas une galerie statique ». Le carnet est donc construit autour d'une chaîne dont chaque maillon est mesuré :
git rev-parse HEADdans.lake/packages/{mathlib,ModalLogic,Foundation}, confronté àlake-manifest.jsonassert), sinon arrêtlake build FormalLogic.ModalZoo(idempotent)rc == 0exigé ; c'est le module du pin qui compile, pas un binaire préexistantModalZoo.toJsonet les générateurs, imprimés par#evalentre marqueurs<<<MZJSON>>>/<<<MZGENS>>>json.loadssur la charge entre marqueurs) : aucune liste recopiée à la maincoverségal, orientation comprise)matplotlibà partir des données de l'étape 6, pas d'une image importéeLe droit de recalculer l'ordre en Python n'est pas une commodité : c'est un théorème du module.
weakerThan_iff_profileénonces.logic ⪯ t.logic ↔ profile(s) ⊆ profile(t)— l'ordre du cube est l'inclusion des profils. C'est ce qui autorise le carnet à retrouver l'ordre à partir des seuls profils, puis à le confronter aux listescovers/incomparablesque le module certifie par ailleurs (strict_of_mem_covers,incomparable_of_mem).Résultat mesuré, imprimé par le carnet :
K0 ·KD/K41 ·KT/KD452 ·KTB/S43 ·S54.L'écart profil / générateurs est mesuré aussi — la derniere colonne du tableau, imprimee par la cellule d'export sous le nom
Profil \ gens. Il porte une leçon que le carnet souligne : un système prouve plus que ce qu'il pose (KTprouveD,KTBprouveD,S4prouveD,S5prouveD,Bet4) — d'oùgens ⊂ profile, vérifié par le carnet sur les huit systèmes (gens_subset_profile).Enfin la distinction que le carnet prend pour cible d'apprentissage : « incomparable » n'est pas « un peu plus faible » ni « on ne sait pas ». Deux systèmes peuvent ne pas se dominer tout en divergeant sur une même axiome (
K4contreKD:K4 ⊨ 4sansD,KD ⊨ Dsans4).Position du carnet dans la série (convention d'accrétion, §5.2)
Le nom suit la grammaire arbitrée le 25/09 (#16231 / #17784) :
<Prefixe>-<NN><lettre?>-<Titre>-<Noyau>.ipynb, noyau toujours présent et toujours dernier. Ici le noyau estLean-Python— et ce n'est pas un ornement :check_kernel_suffix_canon.pyrefuse un carnet ajouté dont le suffixe contredit lekernelspecréel, et le carnet est bien un carnet Python (kernelspec python3) qui pilote Lean par sous-processuslake/lean— exactement le cas que la table de compatibilité nomme (SUFFIX_KERNEL_COMPAT = {..., "lean-python": {"python"}}).Le parent pédagogique, et l'argument écrit qu'exige la §5.2 : ce carnet approfondit le palier
02(« Basic Logics »), et c'est l'argument qui lui donne sa lettre. La branche02porte déjà sa base (Tweety-02) et quatre accrétions (bsémantique,cFOL,dlabo FOL-Lean,ecalculs de preuve) ; la lettre demandée estf, dans la norme §4 (e-fau maximum par branche). Le carnet ne « prolonge » pas le survol02: il le creuse sur un point que la série ne touchait qu'en passant — la modale n'y était qu'un exemple d'API (Tweety-3-ModalLogic-Csharpcôté Java), alors qu'ici huit systèmes sont posés avec leur ordre et chaque trait du dessin est certifié. C'est un acte pédagogique déclaré, celui que la §1 décrit (« une lettre dit : ceci approfondit »), pas un rangement.Déclaration de cohérence, mesurée et non supposée :
rename_notebooks.py --propose(l'outil du chantier #16231) proposerait de renommer toute la série (Tweety-3-*→Tweety-03-*, et les-Leande noyaupython3→-Lean-Python). Ce lot ne fait pas ce chantier — il ne touche que le carnet ajouté, qui naît directement au canon. Le reste de la série garde son nom : la mise en conformité de l'hérité est le chantier #16231, pas ce lot (un PR par série, jamais un composite).Audit README fichier-entier (§E)
Le README de la série est mis à jour sur 14 surfaces, chacune re-dérivée du disque, avec assertion d'occurrence par substitution (script conservé, sorties citées) : tableau des stacks (colonne Python), vue d'ensemble (notebooks, cellules), table Structure (+ entrée
2f), deux paragraphes « notebooks principaux », table « En quoi chaque notebook est unique » (+ entrée), arbre de structure, statistiques par sous-catégorie (Lean companion6 → 7, Total38 → 39), deux phrases de prose, et le changelog (Version 1.2.6).Écart mesuré au passage, et déclaré : la vue d'ensemble annonçait 1165 cellules pour 37 carnets racine + 1 probe ; le disque en portait 1150 (1138 racine + 12 probe). Les 438 cellules de code, elles, étaient exactes. Après ajout du carnet : 1170 cellules dont 446 code (mesure :
1158 + 12racine/probe, dont441 + 5de code).Contrôles indépendants sur le README patché : liens
.ipynb40/40 résolus sur disque, 0 cible absente ; blocsCATALOG-STATUSlaissés byte-identiques (2 blocs,pedagogical_count: 36—catalog-pr-hygiene: ils décriventmainet se résorberont à la régénération).Résidus déclarés, non comblés ici :
Tweety-12-Grounded-Via-TweetyProjectreste absent des deux tables (résidu hérité des versions 1.2.3 à 1.2.5 — aucune ligne inventée) ; la ligne « Durée estimée ~6h (tutorat) » n'est pas re-dérivée (notion distincte de la somme par carnet).Validation
raise NotImplementedError/assert False/1/0: absents du carnet (grep, 0 hit). Les trois exercices sont des stubs qui s'exécutent et affichent leur consigne.python3, cwd = dossier de la série). Résultats committés sur le fichier : 8/8 cellules de code portent unexecution_countréel (1..8), 0 sortie d'erreur, 0 cellule vide.metadata.papermill:exception: None,duration: 400.79s. Mesure automatique complémentaire : 0 chemin machine dans l'ensemble des sorties — quatre motifs cherchés (lettre de lecteur Windows suivie de deux-points, préfixe/mnt/,C:+WINDOWS, chemin absolu du depot), 0 occurrence, ce que les carnets jumeaux 02d/02e/3b respectent aussi.lake env leanen WSL) et leurs sorties portent le[exit 0]du moteur ; la sortie de la cellule 6 reproduit le JSON tel qu'écrit par Lean.## Exercice N: contexte / objectifs / indices) et stub C.1 qui s'exécute.git rev-parsedans.lake/packages) et confrontés aulake-manifest.json; le build de la cible est relancé par le carnet lui-même (rc == 0,Build completed successfully (1023 jobs)).Déviations déclarées
Tweety-02f-Modal-Zoo-Lean), avant que la grammaire du 25/09 (Remise d'aplomb de la nomenclature des notebooks — suffixe noyau, sans-numero, profondeur d'accretion #16231/tool(#16231): rename_notebooks.py — renommer une série en une commande (table, git mv, référents, organes), aide au rebase, cliquet sur les noms ajoutés #17784) soit appliquée. Entre les deux, deux corrections de SOURCE ont été portées, puis le carnet a été ré-exécuté en entier — c'est cette seconde exécution, et elle seule, qui est committée :-Lean→-Lean-Python(le carnet est un carnet Python qui pilote Lean ;check_kernel_suffix_canon.pydéclarekernel_mismatchbloquant sur un carnet ajouté dont le suffixe contredit lekernelspec) ;D:\dev\...,C:\WINDOWS\system32\wsl.EXE) dans ses sorties. Aucune sortie n'a été éditée à la main (Stop & Repair,secrets-hygiene.mdrègle 6) : la cause a été corrigée — impression de chemins relatifs à la racine du dépôt — puis le carnet ré-exécuté. La sortie committée porte désormaisMyIA.AI.Notebooks/SymbolicAI/TweetyetWSL : present, et la mesure automatique ci-dessus rend 0 chemin machine (les jumeaux 02d/02e/3b en portent 0 également : c'est la convention de la série que la première version violait).Une troisième écriture, sur une cellule markdown seule, a suivi la ré-exécution : le texte de la section « Lecture : ce que l'export certifie » nommait une colonne « Ecart profil / gens » que le tableau n'imprime pas sous ce nom — corrigé en
Profil \ gens, tel que le moteur l'écrit. Empreinte des sorties vérifiée identique avant/après cette retouche (assertion sur le hash desoutputs+execution_count), donc C.2 intacte.Enfin la normalisation tolérée
metadata.papermill.input_path/output_pathramenés au basename (tolérance 1 desecrets-hygiene.md— des métadonnées, pas une sortie de cellule), qui est exactement ce que portent les trois jumeaux de la série (mesuré :input='Tweety-02d-FOL-Lab-Lean.ipynb', idem 02e et 3b).formal_logic_lean/sont couvertes par le claim d'une autre lane ; ce lot n'y écrit pas — il lit le module et l'exécute.gh pr list --state all --search "Tweety-02f"→ vide) ; l'entrée bloquante rendue parcheck_lane_claim.pysur l'EPIC porte le marqueur DELIVERED (pr_ref: 17757, MERGED) sans clausepaths:— lue epic-wide par l'organe, sans intersection avec le périmètre de ce lot (consigné dans le commentaire[CLAIMED-AMEND]).is:pr is:open "lane myia-po-2025:CoursIA" in:body) rend 16 PRs ouvertes au 2026-09-25T18:4xZ pour un cap de 15. La famille parquée est le lot densité fix(density,#17040): redressement paquet P04 - 41 lectures dupliquees retirees #17048/fix(density,#17040): redressement paquet P14 — RL + Search CSP/Hybrid #17054/fix(density,#17040): redressement paquet P19 — SemanticWeb + SmartContracts + SymbolicLearning + Tweety #17056/fix(density,#17040): redressement paquet P18 — SMT/Z3-API + SemanticWeb #17059/fix(density,#17040): redressement paquet P09 -- series IIT #17060/fix(density,#17040): redressement paquet P02 — 6 notebooks GameTheory #17062/fix(density,#17040): redressement paquet P03 — GameTheory 4x, GenAI 7x #17064, en attente de revue coordonnateur (décision Redressement campagne densité #13410 : remplissages dégénérés — 233 notebooks, 20 paquets d'audit #17040). Ce lot ajoute la 17ᵉ : mesure déclarée ici plutôt que tue, la dette étant de digestion, pas de production.🤖 Generated with Claude Code