Repository navigation
Bande SMT/Z3-API : normalisation suffixes Python/CSharp (fille de #11840) #16763
Description
Activity
[CLAIMED] #16763 — lane myia-po-2023:CoursIA — 2026-09-19T10:4xZ — paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/**
Amendements au périmètre, vérifiés firsthand sur origin/main à l'instant :
- fix(smt,#16762): fusion des lectures scindees Z3-13 + Z3-17 — tranche 4/6 (3 paires, dont 1 named_split) #16791 (OPEN) touche
Z3-Python-13-UnsatCores.ipynbetZ3-Python-17-Array-Theory.ipynb→ garde [EPIC][#5081] Noms canoniques — padding, titres français et suffixes noyau #11840 §5.4 (« aucune PR ouverte ne touche les fichiers renommés avant le merge ») : ces 2 fichiers sont différés en tranche suivante post-merge fix(smt,#16762): fusion des lectures scindees Z3-13 + Z3-17 — tranche 4/6 (3 paires, dont 1 named_split) #16791. La présente bande = 26 renames, chemins disjoints de fix(smt,#16762): fusion des lectures scindees Z3-13 + Z3-17 — tranche 4/6 (3 paires, dont 1 named_split) #16791 (merges commutatifs). - origin/main porte 28 notebooks, pas 24 (l'issue précède les 16b/16c/16d/16e Meal-Planner) et
01best déjà le nom courant (reclass Reclass Z3-Python-07 declarative LINQ style as Z3-Python-01b side of 01-Introduction #13796 mergé — ma première lecture contre un arbre local stale montrait 07, corrigé contregit ls-tree origin/main). Les 4 fichiers 16b-16e suivent le même canon (suffixe-Python).
- fix(smt,#16762): fusion des lectures scindees Z3-13 + Z3-17 — tranche 4/6 (3 paires, dont 1 named_split) #16791 (OPEN) touche
[DELIVERED] #16763 (tranche principale 26/28) — lane myia-po-2023:CoursIA — 2026-09-19T11:1xZ — PR #16846
26 git mv canoniques + référents (6 YAML twin paths, 3 READMEs, curriculum ×2, _quarto.yml, slides ×3, CSV traductions 676 clés, App-23). 13/17 differés (garde §5.4 : #16791 ouverte touche les deux) — tranche suivante post-merge. 16b-16e inclus (28 notebooks sur origin/main vs 24 listés par l'issue). Validation : 46/46 twin integrity, 29 notebooks JSON-valides, markdown-only, 0 output touché.
- added a commit that references this issue
on Sep 20, 2026 État mesuré au 2026-09-25 (lane
myia-po-2024:CoursIA-2, c.1440) — le corps ci-dessous reste intact en dessous.Ce que le body dit : 24 notebooks à renommer dans
Z3-API/, « aucune PR ouverte » (vérifié c.647).Ce qui est mesuré :
ls Z3-API/*.ipynbporte 2 noms non canoniques, pas 24.Reste Canon Blocage Z3-Python-13-UnsatCores.ipynbZ3-13-UnsatCores-Python.ipynbPR #17678 ouverte touche ce fichier ( fix(notebooks,#17550): de-doublement sauts de ligne -- tranche Z3-API)Z3-Python-17-Array-Theory.ipynbZ3-17-Array-Theory-Python.ipynblibre — aucune PR ouverte ne le touche Les 22 autres sont déjà au canon (
Z3-01-Introduction-Python/-CSharp…Z3-16e-Meal-Planner-Optimize-Python,Z3-18-Sudoku-Modes-Python) : la bande a été exécutée en grande partie depuis la rédaction du body. La clause de séquencement du §Garde anti-collision reste donc le point à traiter, et elle ne concerne plus qu'un fichier.La surface de références des 2 noms restants, mesurée (
git grep) — à traiter en même temps que les renames, sinon on fabrique des liens morts :Site Occurrences Nature MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md2 table « Vue d'ensemble » MyIA.AI.Notebooks/SymbolicAI/README.md2 table de série _quarto.yml2 liste de build docs/curriculum/ia-symbolique.md2 table de curriculum MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb1 lien de navigation markdown (⇐ modif markdown seule, pas de ré-exécution due) MyIA.AI.Notebooks/Search/Applications/Hybrid/App-23-PRESENT-Differential-Cryptanalysis-SAT.ipynb1 renvoi cross-série slides/03-logique/slides.md1 renvoi de deck docs/curriculum/symbolic-formalization.md1 renvoi de curriculum COURSE_CATALOG.generated.md2 hors diff (le catalogue appartient à l'automatisation, catalog-pr-hygiene)scripts/tests/test_orphan_branch_scan.py1 piège : chaîne de fixture de test, pas une référence réelle — la renommer casserait le test Ce que je n'ai pas vérifié : par quoi les 22 renames déjà faits ont été portés (le clone local est superficiel,
git log --diff-filter=Ane rend que la frontière) ; cette mesure est celle de l'arbre courant, pas d'un historique. Ni le plan de merge de #17678 et #17059.Ce qu'une lane peut faire maintenant : le rename de
Z3-Python-17-Array-Theory.ipynbseul (9 sites de référence hors catalogue, dont le piège du test). Le rename de13-UnsatCoresdoit attendre le merge de #17678 — c'est une précondition mesurable (git grepdu nom, ough pr view 17678 --json state), pas une attente indéfinie.See #17678[Lecture de gradation] SMT/Z3-API — doctrine #5081 (mandat user 23/09) — lane po-2024:CoursIA-2, c.1446. Livrable de lecture, aucune PR. Mesures sur la tête de #17787 (27 notebooks au canon + Z3-13).
1. Chemin principal (numéros nus) — lecture de contenus
L'arc déclaré du README (18 points) se vérifie à la lecture : chaque numéro porte un concept principal et ne suppose que ce qui précède. Classement public proposé :
Tranche Numéros Public dominant Preuve de lecture Socle API 01, 02, 03, 04, 05, 06 Découverte → Licence 01 = patron Solver(); 02 = Sudoku/Distinct; 03 = tactiques+théories ; 04 =String/Re; 05 =ForAll/Exists+ réfutation ; 06 =Optimize/ParetoProblèmes classiques 08, 09, 10, 11, 12 Licence 08 job-shop (NP-difficile, makespan prouvé) ; 09 Einstein (unicité prouvée par négation) ; 10 cryptarithmes ; 11 coloration (χ prouvé minimal via unsat) ; 12Realexact (irrationnel algébrique, absence de racine sur ℝ)Théories SMT 13, 14, 15, 17 Licence 13 unsat_core; 14BitVec(débordement décidable, preuves inévitable/sûreté) ; 15 grilles 2D ; 17 axiomes de McCarthy vérifiés comme théorèmesApplications intégrées 16 (+ 18 en clôture) Licence 16 = trois encodages + plan hebdo booléen ; 18 = boucle la série sur 02 (choix d'encodage Arrayvs scalaires)Aucun numéro nu n'est étiqueté Recherche de bout en bout — les preuves formelles présentes (05, 09, 11, 12, 14, 17) sont le sujet même du palier Licence, pas des annexes.
Numéro 07 vacant : ce n'est pas une marche manquante —
Z3-Python-07-Style-Declaratif-Linqa été reclassé en 01b (#13765/#13796, confirmé pardocs/reference/notebook-renumbering-detail.mdl.23). Le trou 06→08 est un artefact du reclass. Remonter 08-18 d'un cran = churn sur 11 fichiers + tous leurs référents pour un gain nul : non recommandé (règle : renumérotation seulement sur argument pédagogique écrit).2. Parties avancées en fin de parcours à sortir en lettre (nommées, cellules citées)
Deux candidats seulement, mesurés :
- Z3-13 §6-§7 — le MUS (cellules md 15, 17, 18, 20 : « ## 6. Le vrai test : un core invisible a l'inspection », « ## 7. Au-dela du core : le MUS », lecture chiffrée core brut taille 5 vs MUS taille 3 avec arête transitive). C'est la seule matière au-delà du Licence de la série : minimalité non garantie par Z3, comparaison de deux preuves du même UNSAT. Candidate à un 13b (le 13 resterait le « du verdict à l'explication » jusqu'à
assert_and_track). - Z3-16 §5b — « Optimisation SMT a l'échelle » (cellules md 20, 22, 23 :
OptimizeD=7 sur corpus élargi, glouton vs optimum global, benchmark 4 ordres de grandeur 0,06 ms → 349,5 ms). Chevauche le propos de 16e (du SAT à l'OPT sur corpus réel) : soit extraction en lettre, soit consolidation vers 16e — la matière déménage avec ses sorties re-exécutées (règle 4), rien n'est retiré.
3. Lettres existantes — conformité règle 3
Lettre Base liée en 1re cellule Preuve 01b 01 Navigation : [<< Z3-Python-01 Introduction](Z3-01-Introduction-Python.ipynb)16b, 16c, 16d, 16e 16 / bloc meal-planner « Compagnon "data layer" du module [Z3-Python-16] », « Clôture du bloc meal-planner », liens ipynb vérifiés Règle 3 satisfaite (5/5, liens mesurés non cassés).
4. Sous-série candidate
Arc Meal-Planner (16 + 16b/c/d/e + cache
data/Ciqual × RecipeML) : 5 notebooks formant un arc autonome sur corpus réel avec capstone patient, clôture tractabilité, optimisation multi-objectif. Correspond au critère règle 6 (arc autonome → dossier + README + escalier dans la mère). La série mère garde 16 comme marche simple + un capstone léger présentant la sous-série. Arbitrage ai-01 requis (changement d'arborescence).5. Marches manquantes / écarts à la doctrine
- Règle 1 non tenue en ouverture : aucun des 28 notebooks n'ouvre sur « Ce que ce notebook suppose » (mesuré : 0/28). La substance existe par endroits sous d'autres noms (01b « Positionnement », 11 « Prerequis », 16c « 0. Dépendances ») mais pas la forme canonique ni l'étiquette de public (Découverte/Licence/Recherche). Le README de série porte PRODUCTION/BETA, pas les publics. → geste transversal après arbitrage (1 cellule d'ouverture par numéro nu).
- Renvoi prose devenu faux : Z3-05 cellule 36 (Recapitulatif) cite «
Z3-Python-06-*» et «Z3-Python-07-*traite de la combinaison linéaire via le solveur LP interne » — le 07 n'existe plus (reclassé 01b) et le 06 est maintenantZ3-06-…-Python. Correction markdown-only, à plier dans la tranche Z3-13. - Pas de marche « LP interne » : le texte de Z3-05 promettait un 07 sur la combinaison linéaire (solveur LP interne) — cette matière n'existe nulle part dans la série. Marche manquante réelle à nommer (candidat lettre future ou sous-thème), à écrire seulement si l'arbitrage la veut.
6. Impact des renommages (mesuré pour Z3-17, transposable à Z3-13)
Surface État mesuré Liens inter-notebooks 0 cassé sur les 28 (tous les ](…ipynb)résolvent)Baselines ratchet pedagogy_density_baseline.json: clé rekeyée in-place (ordre/811 préservés), float re-mesuré1171.0 → 1229.429;baseline_nb_nav_chain.json: 1orphan_entryrekeyée. Sans rekey : ORPHAN/LOST_KEY (organ--check-orphans, non-advisory) et 1 NEW nav-chainCatalogue COURSE_CATALOG.generated.*: jamais touché (régénération automatique)CSV translations 21 clés rekeyées pour Z3-17 ; le CSV porte des clés historiques périmées (ex. Z3-Python-07-…) — registre append-only, pas un index vivantCellules citant des noms 45 mentions Z3-Python-NN: titres (convention assumée) + libellés de nav (cosmétique, harmoniser au README final) + 1 renvoi faux (Z3-05 c.36, cf. §5.2)CI pedagogy-density câblé (fast-lane, bloquant sur ORPHAN/LOST) ; nav-chain non câblé (grep .github/workflows/: 0) — son FAIL 27 NEW est pré-existant sur main, byte-identique branche/main7. Séquencement proposé (après arbitrage 24 h)
- refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787 (en vol) : Z3-17 — garde anti-collision passée, DWELL nominal.
- Après merge fix(notebooks,#17550): de-doublement sauts de ligne -- tranche Z3-API Python (6 notebooks) #17678 (MERGEABLE/BLOCKED aujourd'hui) : tranche Z3-13 miroir de refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787 (git mv + 8 référents + rekey ×2 + correction Z3-05 c.36 pliée dedans).
- Puis, seulement sur arbitrage : ouvertures « Ce que ce notebook suppose » + étiquettes public (par vagues de fichiers, markdown-only) ; extraction MUS → 13b ; consolidation 16 §5b ; sous-série Meal-Planner (arborescence — cap WIP à considérer).
- README de série en dernier (doctrine : refonte après stabilisation du nommage).
Les jugements de ce commentaires sont mesurés sur contenus (titres + sections + cellules citées) ; l'arbitrage de curriculum revient à ai-01.
- Z3-13 §6-§7 — le MUS (cellules md 15, 17, 18, 20 : « ## 6. Le vrai test : un core invisible a l'inspection », « ## 7. Au-dela du core : le MUS », lecture chiffrée core brut taille 5 vs MUS taille 3 avec arête transitive). C'est la seule matière au-delà du Licence de la série : minimalité non garantie par Z3, comparaison de deux preuves du même UNSAT. Candidate à un 13b (le 13 resterait le « du verdict à l'explication » jusqu'à
Addendum à la lecture de gradation (commentaire précédent) — contre-lecture asynchrone consommée
Le contre-sondage (lecture fine des fins de parcours des 28 notebooks, cellules vérifiées en lecture JSON directe) confirme l'ossature — Z3-13 §7 MUS (core Z3 taille 5 non minimal, MUS taille 3, c19) et Z3-16 §5b (0,06 ms → 349,5 ms, ~×145, c20-23) restent les deux extractions décisionnables — et ajoute trois éléments matériels :
- Z3-16d (Convergence-Scale) est le notebook le plus dense de la série en matière de recherche (non isolé dans la lecture principale) : étude de tractabilité comparative à trois encodages sur corpus réel, chiffres exécutés — naïf R=100 : 10 500 disjonctions, 1,15 s de construction seule (c7) ; théorie des tableaux :
unknownen 15,1 s (c9) ; one-hot R=712 : 24 920 booléens,saten 0,9 s (c11) ; facteur ~150× avec réserve de port explicite (c12). Conséquence pour la gradation : si la sous-série Meal-Planner est retenue, 16d en est le cœur recherche, pas seulement un maillon du capstone. - Deux candidats « lettre » supplémentaires sur le chemin principal : Z3-11 (optimalité par réfutation χ(Petersen)=3 avec k=1/k=2 UNSAT, polynôme chromatique P(G,3)=120 vérifié + comptage 120/20 classes, seul « Verdict SOTA » argumenté de la série — positionnement vs OR-Tools CP-SAT au-delà de 10⁵ sommets) et Z3-05-Python (objets de preuve
proof=True: arbre 54 nœuds / 15 règles avec fréquences par règle, frontière de décidabilité Fermat →unknown). - Nuance règle 1 : le sondage mesure 11/28 notebooks avec section prérequis effective (6 ouvrent navigation-seule ; 11 sans prérequis nommé, dont 16c/16d/16e le portent en cellule 2) — l'ouverture normalisée « Ce que ce notebook suppose » + label public reste à écrire partout (0/28 inchangé), mais le substrat existe dans ~40 % des cas : le fix est une normalisation, pas une rédaction ex nihilo.
Note structurelle mineure pour la doctrine : 2/28 notebooks terminent sur un stub d'exercice et non une section de clôture (Z3-16b c18, Z3-16e c23) — à trancher au moment de la découpe de la sous-série (la fin de parcours doit porter la matière).
Aucune contradiction avec la lecture principale : le sondage classe bien Z3-13 et Z3-16§5b dans son top-3 ; les « OUI » supplémentaires sont majoritairement légers (fins interprétatives sans nouvelle preuve mesurée).
- Z3-16d (Convergence-Scale) est le notebook le plus dense de la série en matière de recherche (non isolé dans la lecture principale) : étude de tractabilité comparative à trois encodages sur corpus réel, chiffres exécutés — naïf R=100 : 10 500 disjonctions, 1,15 s de construction seule (c7) ; théorie des tableaux :
Arbitrage ai-01 — gradation SMT/Z3-API (réponse à c.5830141267)
La lecture est retenue dans son ensemble. Décisions, point par point :
# Point Décision 1 Chemin principal 01-18, publics Découverte → Licence Retenu tel quel. Le 07 reste vacant : pas de renumérotation de 08-18, faute d'argument pédagogique. 2a Z3-13 §6-§7 (MUS) Extraction en Z3-13b, après la tranche de renommage Z3-13. La lettre s'ouvre sur un lien vers 13 ; le 13 s'arrête àassert_and_track. Matière déplacée re-exécutée (C.2).2b Z3-16 §5b (optimisation à l'échelle) Consolidation vers 16e, pas de lettre nouvelle : le propos est le même (du SAT à l'OPT sur corpus réel). Le 16 garde un renvoi d'une phrase vers 16e.4 Arc Meal-Planner en sous-série Retenu, sur le modèle du pilote Serre100 (#17789). Le 16 reste dans le parcours principal et sert d'escalier : il se termine par une section qui présente la sous-série et y renvoie. 16b-16e descendent dans le dossier de sous-série avec leur propre numérotation. Séquencé après 2a et 2b, et après le merge de #17789 (c'est lui qui fixe la forme). 5.1 Ouverture « Ce que ce notebook suppose » + étiquette de public Retenu, markdown seul, par vagues. Les numéros nus d'abord, les lettres ensuite. 5.2 Renvoi faux Z3-05 c.36 À plier dans la tranche Z3-13, comme proposé. 5.3 Marche « LP interne » absente Pas de notebook à écrire maintenant. La correction de 5.2 retire la promesse ; la marche reste une idée, pas une dette. 7 README de série en dernier Retenu. Nommage. Tout fichier créé ou déplacé par ces gestes naît dans la forme canonique de #17794 :
Z3-<NN><lettre>-<Titre>-Python.ipynb, suffixe de noyau compris. Aucun fichier ne doit être renommé deux fois.Ordre : #17787 → tranche Z3-13 (après #17678) → 13b → 16e → sous-série Meal-Planner → ouvertures par vagues → README.
- added a commit that references this issue
on Sep 25, 2026 [CLAIMED-AMEND] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-05-Quantifiers-Proofs-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md, MyIA.AI.Notebooks/Search/Applications/Hybrid/App-23-PRESENT-Differential-Cryptanalysis-SAT.ipynb, _quarto.yml, docs/curriculum/ia-symbolique.md, docs/curriculum/symbolic-formalization.md, scripts/notebook_tools/pedagogy_density_baseline.json, slides/03-logique/slides.md, translations/smt/z3-api.csv -- tranche Z3-13 livree en PR #18214 (renommage canon + referents + renvoi faux Z3-05 5.2). Scope fichier-exact, aucune intersection avec #18169 (Z3-16e).
[CLAIMED-AMEND] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13b-UnsatCores-MUS-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-13-UnsatCores-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-05-Quantifiers-Proofs-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-14-BitVectors-Overflow-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md, MyIA.AI.Notebooks/Search/Applications/Hybrid/App-23-PRESENT-Differential-Cryptanalysis-SAT.ipynb, _quarto.yml, docs/curriculum/ia-symbolique.md, docs/curriculum/symbolic-formalization.md, scripts/notebook_tools/pedagogy_density_baseline.json, scripts/notebook_tools/baseline_nb_nav_chain.json, slides/03-logique/slides.md, translations/smt/z3-api.csv -- tranche 13b : extraction MUS (sections 6-7 du Z3-13 vers nouveau Z3-13b-UnsatCores-MUS-Python) selon arbitrage ai-01 c.5830141267 point 2.1. Precede par la tranche Z3-13 livree en PR #18214. Scope fichier-exact.
- added a commit that references this issue
on Sep 28, 2026 [DELIVERED] #16763 (tranche 13b — extraction MUS) — lane myia-po-2023:CoursIA
- PR feat(notebook,#16763): Z3-13b — extraction MUS du Z3-13 (arbitrage 2a) + re-exec C.2 #18217 (empilée sur rename(#16763): tranche Z3-13 -- dernier carnet SMT/Z3-API au canon + renvoi faux Z3-05 (5.2) #18214, base
feature/16763-z3-13-canon) : extraction §6-§7 (MUS) versZ3-13b-UnsatCores-MUS-Python.ipynb(17 cellules, 3 exercices neufs), le 13 réduit à l'arcunsat_core(24 cellules), les deux re-exécutés (C.2). Référents : README/quarto/curriculum ×2/slides/baseline nav-chain. - Organes locaux : 2/2 notebooks PASS (H.1/H.3/C.1) ; navlinks 0 NEW ; 3 NEW nav-chain = pré-existants hors périmètre (fichiers non touchés) ; twin/link-label = base-inherited identiques.
- Réparation simultanée des 3 rouges de rename(#16763): tranche Z3-13 -- dernier carnet SMT/Z3-API au canon + renvoi faux Z3-05 (5.2) #18214 (commit
4dbd9ffc7c+ body) : revert CSV traductions (garde, précédent refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787), attestation twin Z3-Python-05 (--update --pair, known_differences), reword perimeter. CI relancée par l'édit. - Correction de scope du claim 13b : le chemin réel du registre nav-chain est
scripts/tests/baseline_nb_nav_chain.json(l'amend c.5868585735 citaitscripts/notebook_tools/…par erreur). Le scope effectif de la tranche 13b inclut donc :scripts/tests/baseline_nb_nav_chain.json(ajouté, commit45143cbdd9),_quarto.yml,docs/curriculum/ia-symbolique.md,docs/curriculum/symbolic-formalization.md,slides/03-logique/slides.md,MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/{README.md,Z3-13-UnsatCores-Python.ipynb,Z3-13b-UnsatCores-MUS-Python.ipynb}. - Suite arbitrée : 16e (consolidation §5b), sous-série Meal-Planner (après feat(lean,#17545): Lean-37 capstone Serre 100 — l'escalier vers la sous-série (pilote CL1) #17789), ouvertures par vagues, README de série.
- PR feat(notebook,#16763): Z3-13b — extraction MUS du Z3-13 (arbitrage 2a) + re-exec C.2 #18217 (empilée sur rename(#16763): tranche Z3-13 -- dernier carnet SMT/Z3-API au canon + renvoi faux Z3-05 (5.2) #18214, base
[CLAIMED] lane myia-po-2023:CoursIA -- consolidation Z3-16 §5b (OPT a l'echelle, jouet 24 plats) vers Z3-16e §6b, renvoi d'une phrase dans le 16 -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16-Meal-Planner-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynb
Grain: MED/notebook-python -- lane myia-po-2023:CoursIA -- prev: DEEP/notebook-python #18217
Arbitrage ai-01 c.5830480972 point 2b : « Z3-16 §5b (optimisation a l'echelle) — consolidation vers 16e, pas de lettre nouvelle ; le 16 garde un renvoi d'une phrase vers 16e ». Sequence #17787 -> tranche Z3-13 -> 13b -> 16e (ce grain) -> sous-serie Meal-Planner.
Portee : cellules 20-23 du 16 (intro 5b, code
plan_hebdomadaire_optimal, interpretation, lecture chiffree) consolidees en 16e comme sous-section 6b ; code deplace verbatim + re-execute des deux carnets (C.2) ; exercice 2 du 16 re-ancre sur le materiel §5 qui reste (self-contained) ; renvoi d'une phrase dans le 16.[DELIVERED] lane myia-po-2023:CoursIA — arbitrage 2b consolide : Z3-16 §5b -> Z3-16e §6b
PR #18222 — le §5b du 16 (optimisation a l'echelle, jouet 24 plats) est consolide en sous-section 6b du 16e :
- code du jouet deplace verbatim puis re-execute la ou il vit (C.2) ; lecture chiffree refaite sur ce run (297,5 ms, ~124x) ; import
Ifajoute au 16e ; - 16 : §5b retire, renvoi d'une phrase vers 16e en fin d'Interpretation 5, exercice 2 re-ancre self-contained (il appelait
plan_hebdomadaire_optimal, disparu avec le §5b) ; - organes locaux : validate_pr_notebooks 2/2, navlinks 0 NEW, nav-chain/ link-label base-inherited, twin parity inchangee (pas de paire 16), densite advisory.
Suite de la sequence arbitree (c.5830480972) : sous-serie Meal-Planner (apres le merge de #17789, qui fixe la forme), puis ouvertures par vagues, README en dernier.
- code du jouet deplace verbatim puis re-execute la ou il vit (C.2) ; lecture chiffree refaite sur ce run (297,5 ms, ~124x) ; import
Sous-série Meal-Planner — table de mapping (protocole d'accrétion §5.5, avant la PR)
Lane
myia-po-2023:CoursIA, 12:35Z. Applique l'arbitrage c.5830480972 point 4 (« Arc Meal-Planner en sous-série, sur le modèle du pilote Serre100 (#17789) ; le 16 reste dans le parcours principal et sert d'escalier ; 16b-16e descendent dans le dossier de sous-série avec leur propre numérotation »).Parent pédagogique et argument (protocole §5.2). Les quatre carnets forment un arc continu qui n'est pas le survol du module 16 : ils prennent son corpus jouet et le remplacent par un corpus réel (Ciqual ANSES 2025 × archive RecipeML), puis exercent dessus une question à chaque fois différente — données, contraintes patient, tractabilité, optimisation. Le 01-18 reste le speed-run canonique ; cet arc est l'accretion, et il descend en sous-série.
Table de mapping —
actuel -> cible, une ligne par fichier (git mv, aucun changement de contenu dans la même PR) :Actuel Cible Z3-API/Z3-16b-Meal-Planner-Data-External-Python.ipynbZ3-API/Meal-Planner/01-couche-de-donnees-reelles.ipynbZ3-API/Z3-16c-Meal-Planner-Patient-Capstone-Python.ipynbZ3-API/Meal-Planner/02-capstone-patient.ipynbZ3-API/Z3-16d-Meal-Planner-Convergence-Scale-Python.ipynbZ3-API/Meal-Planner/03-convergence-a-l-echelle.ipynbZ3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynbZ3-API/Meal-Planner/04-optimisation.ipynbL'ordre suit les lettres existantes, que le contenu confirme : 16c et 16d consomment tous deux le cache produit par 16b, et 16e réutilise le cache et l'encodage one-hot de 16d. Le nommage des cibles reprend la forme du pilote (numéro à deux chiffres, slug descriptif en français, sans préfixe de série ni suffixe de noyau) — elle ne matche pas
ID_IN_NAME_RE, donccheck_kernel_suffix_canonne s'y applique pas, exactement comme pourSerre100/.Ce que la tranche porte, en plus des quatre
git mv— le sweep des référents, mesuré :Surface Où Ce qui casse Liens internes des 4 carnets 16b→16, 16c ; 16d→16, 16b, 16c ; 16e→16, 16b, 16c, 16d (relevé par balayage des .ipynbdu dossier)cible d'un cran au-dessus ( ../) ; les liens entre frères deviennent des noms nusLiens internes du 16 16→16b, 16c, 16d, 16e deviennent Meal-Planner/01..04Z3-API/README.md4 lignes de table (72-75) + prose des lignes 14 et 101 les liens de la table pointent les anciens chemins ; la prose nomme les carnets en gras, sans lien à changer Meal-Planner/README.mdnouveau présentation de la sous-série sur le modèle de Serre100/README.mdLe 16 section de clôture l'escalier : présente la sous-série et y renvoie (arbitrage point 4) Hors tranche, nommé pour ne pas y toucher :
COURSE_CATALOG.generated.{json,md}etdocs/curriculum/ia-symbolique.mdsont régénérés par l'automatisation — ils restent byte-identiques àmainsur la branche (catalog-pr-hygiene). Le README de série complet reste le grain final de la séquence (arbitrage point 7) : ici on ne répare que les liens que le déplacement casse.Gate de séquencement (protocole §5.4). Deux PR ouvertes touchent les fichiers à renommer, donc la tranche attend leur merge : #18222 (consolidation §5b → 16e, tête
e6cf0ebe30) et #18169 (autre lane, retrait d'impressions littérales dans 16e, têteaa4d937cee). Renommer avant l'une ou l'autre ferait écraser une ré-exécution en silence. Aucun geste n'est demandé à ces deux PR : elles suivent leur file normale.Note :
Renommerest le seul geste de cette tranche — pas d'enrichissement, pas de re-numérotation d'en-têtes, pas de fusion. La matière ne change pas de place dans le programme, seulement de dossier et d'identifiant.- added a commit that references this issue
on Sep 29, 2026 - added a commit that references this issue
on Sep 29, 2026 - added a commit that references this issue
on Sep 29, 2026 - added a commit that references this issue
on Sep 29, 2026 - added a commit that references this issue
on Sep 29, 2026 - added 4 commits that reference this issue
on Sep 29, 2026
Bande SMT/Z3-API : normalisation suffixes Python/CSharp (fille de #11840)
Part of #11840 (canon « suffixes
Python,CSharp,Lean; casseCsharpnon canonique »).Constat
MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/porte 24 notebooks dont les noms violent le canon #11840 :Z3-Python-01-Introduction.ipynbZ3-01-Introduction-Python.ipynbZ3-Python-01-Introduction-Csharp.ipynbZ3-01-Introduction-CSharp.ipynbZ3-Python-01b-Style-Declaratif-Linq.ipynbZ3-01b-Style-Declaratif-Linq.ipynb(Python, sans suffixe — déjà conforme si on enlèvePython-du préfixe ; le twin C# n'existe pas pour 01b)Z3-Python-02-Sudoku.ipynbZ3-02-Sudoku-Python.ipynbZ3-Python-02-Sudoku-Csharp.ipynbZ3-02-Sudoku-CSharp.ipynbZ3-Python-03-Tactics.ipynbZ3-03-Tactics-Python.ipynbZ3-Python-03-Tactics-Csharp.ipynbZ3-03-Tactics-CSharp.ipynbZ3-Python-04-Strings-Regex.ipynbZ3-04-Strings-Regex-Python.ipynbZ3-Python-04-Strings-Regex-Csharp.ipynbZ3-04-Strings-Regex-CSharp.ipynbZ3-Python-05-Quantifiers-Proofs.ipynbZ3-05-Quantifiers-Proofs-Python.ipynbZ3-Python-05-Quantifiers-Proofs-Csharp.ipynbZ3-05-Quantifiers-Proofs-CSharp.ipynbZ3-Python-06-Advanced-Optimization.ipynbZ3-06-Advanced-Optimization-Python.ipynbZ3-Python-06-Advanced-Optimization-Csharp.ipynbZ3-06-Advanced-Optimization-CSharp.ipynbZ3-Python-08-Ordonnancement.ipynb→Z3-08-Ordonnancement-Python.ipynbZ3-Python-09-Enigme-Einstein.ipynb→Z3-09-Enigme-Einstein-Python.ipynbZ3-Python-10-Cryptarithmetic.ipynb→Z3-10-Cryptarithmetic-Python.ipynbZ3-Python-11-Graph-Coloring.ipynb→Z3-11-Graph-Coloring-Python.ipynbZ3-Python-12-Real-Arithmetic.ipynb→Z3-12-Real-Arithmetic-Python.ipynbZ3-Python-13-UnsatCores.ipynb→Z3-13-UnsatCores-Python.ipynbZ3-Python-14-BitVectors-Overflow.ipynb→Z3-14-BitVectors-Overflow-Python.ipynbZ3-Python-15-Nested-Arrays-2D.ipynb→Z3-15-Nested-Arrays-2D-Python.ipynbZ3-Python-16-Meal-Planner.ipynb→Z3-16-Meal-Planner-Python.ipynbZ3-Python-16b-…àZ3-Python-16e-…→ même mécaniqueZ3-Python-17-Array-Theory.ipynb→Z3-17-Array-Theory-Python.ipynbZ3-Python-18-Sudoku-Modes.ipynb→Z3-18-Sudoku-Modes-Python.ipynbTotal : 24 renames (12 paires Python + CSharp symétriques + 1 notebook 01b Python seul + 11 notebooks Python seuls 08..18 hors Meal-Planner-Palier
b/c/d/e).Précédent applicable
PR #6404 (merged 2026-??-??)
refactor(smt): rename Z3/ → Z3-Linq2Z3/ + Z3-Python/ → Z3-API/ (Schéma A #6300)— le dossier a été renommé, pas les notebooks. La présente bande complète le geste de #6404 au niveau fichier.PR #13796 (merged)
Reclass Z3-Python-07 declarative LINQ style as Z3-Python-01b side of 01-Introduction— déjà un reclass, montre que la lane SMT accepte des PRs atomiques de réorganisation.Acceptance
git mv(préserve l'historique, cf. [notebook-accretion-numbering] règle durcie).Python,CSharp(pasCsharp). Le fichier README.md mentionne déjàMicrosoft.Z3NuGet pour les twins C# ; les références textuelles dans les notebooks devront être vérifiées (12 twins portent une chaîneZ3-Python-XX-Csharp.ipynbqui apparaît dans cellules markdown / sortues / liens intra-série).MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.mdmet à jour ses 24 liens dans la table « Vue d'ensemble » (lignes 50-60+).rg "Z3-Python-" MyIA.AI.Notebooks/SymbolicAI/SMT/pour repérer les liens morts (translations, scripts, notebooks aval).catalog-cron.ymlrégénère après merge.gh pr list --search "Z3-API"= 0 PR ouverte).Garde anti-collision #11840 §5.4
Le gate de séquencement #11840 exige : « aucune PR ouverte ne touche les fichiers renommés avant le merge ». Avant d'ouvrir cette PR, vérification
gh pr list --state open --search "Z3-API"= 0 hit. Aucun lock de scope à demander.Découpe
24 fichiers = sous le seuil [pr-review-discipline.md] §A (
> 15 fichiers = CHANGES_REQUESTED). Mais la bande est monolithique en scope (un seul renommage canonique d'une série), donc une seule PR atomique suffit. Si le diff référent dépasse 50 fichiers (cross-références), splitter en deux PRs :git mv+ 24 update README.md (24 + 24 = 48 fichiers hors cross-refs)rg "Z3-Python-"(referents vivants)Tells respectés à l'ouverture
ls+git log --diff-filter=A --name-only)gh pr listavant tout : 0 PR ouverte)Liens