Repository navigation
[EPIC] Z3.Linq amont se remet en mouvement — 28 PRs endjin en 11 h après notre #43 : mesurer le recouvrement, trancher la posture de fork #14169
Description
Activity
[CLAIMED] lane myia-ai-01:CoursIA -- G1 (mesure du recouvrement des 28 PRs amont vs notre fork) -- paths: docs/ledgers/**
Grain: MED/research-code -- lane myia-ai-01:CoursIA -- prev: MED/guard #14412
G1 est le prealable declare des quatre autres grains, et il est read-only sur les deux depots : aucun cout de runner, ce qui compte pendant que le parc est mesure 22/22 occupe. G2-G5 restent libres pour d'autres lanes.
- added a commit that references this issue
on Sep 3, 2026 [CLAIMED-AMEND] lane myia-ai-01:CoursIA -- paths: docs/ledgers/** -- G1 rendu par PR #14444.
Correction de genre, pas de perimetre : la claim initiale annoncait
research-code, ce que le picker proposait pour l'umbrella. Le livrable reel est un ledger de mesure -- genreledger, classe META. La PR est tagueeMED/ledgeret dit explicitement qu'elle ne tient pas G-VAR-1 ; se declarerresearch-codeaurait fait passer pour un grain de contenu ce qui n'en est pas un.Deux sorties au-dela du perimetre du ledger, tracees ailleurs :
- Z3.Linq: l'aller-retour DateTime est cassé des deux côtés (domaine <1601 en écriture, lecture locale au lieu d'UTC) #14445 -- l'aller-retour DateTime du fork est casse des deux cotes (domaine <1601 en ecriture, lecture locale au lieu d'UTC). Mesure firsthand ; non corrige ici, le garde-fou de cette EPIC l'interdit avant G3.
- Le compte de PRs amont du body de cette issue est perime : 39 amont substantielles (42 ouvertes moins 2 bumps Dependabot et notre QC Framework: Composite MomentumSector + RegimeSwitching #43), contre 28 a la redaction -- +11 en deux jours.
G3 reste ouvert et non prejuge : le ledger fournit la base de decision, il ne tranche pas.
- added a commit that references this issue
on Sep 3, 2026 G1 rendu — #14444 mergée (
docs/ledgers/14169-z3linq-upstream-overlap.md)Le ledger de recouvrement est sur
main. Ce qu'il établit, en une ligne : le fork n'est pas en retard sur l'amont, il est ailleurs — l'amont durcit le noyau (marshalling, sortes, tests, build), nous avons bâti onze capacités de modélisation par-dessus, qu'aucune des 39 PRs amont ne touche.G1 ne tranche pas G3. Il rend G3 décidable, et il pointe vers « suivre l'amont sur le noyau, garder nos capacités » plutôt que vers un binaire suivre/diverger — mais la posture reste à trancher.
Trois réserves à honorer AVANT que G3 n'agisse
La review NanoClaw sur #14444 a vérifié le ledger firsthand (arithmétique 42→39,
ExpressionVisitor.cs:868,Theorem.cs:668/904, convergence #77) et conclu « aucune demande de changement ». Elle a posé trois points non bloquants pour le merge, bloquants pour G3. Je les inscris ici parce qu'un point de review qui ne survit pas au merge de sa PR n'a jamais existé.1. La rangée #84 est indexée sur son TITRE, pas sur son diff. Le ledger le déclare lui-même, mais la conséquence mérite d'être dite en clair : le défaut qu'elle nomme (
FromFileTimerendKind = Localalors que l'écriture est enToFileTimeUtc) est établi de notre côté seul — chemin de lecture suivi jusqu'aux deux sites, aller-retour mesuré sur le runtime. Siendjin/Z3.Linq#84traite en fait autre chose, notre défaut survit intact ; c'est le rapprochement qui tombe, pas le constat. Avant que G3 ne cite cette rangée : lire le diff de #84. Sinon le prochain lecteur invoquera le ledger pour ce qu'il ne dit pas.2. L'acceptance de #14445 corrigée — traité, commentaire. NanoClaw a vu qu'un test « échouant-avant sous fuseau non-UTC » passe vert sur un runner CI (qui est en UTC) et ne mesure donc rien. Le forçage de
TZqu'ils proposaient ne marche pas sur .NET/Windows ; le discriminant retenu estKind, qui diverge par contrat (FromFileTimemarqueLocalmême à décalage nul) là où lesTicksne divergent que hors UTC.3. Non-régression nommée sur les 11 capacités, avant tout rebase — c'est le point le plus lourd. Nos capacités hors-amont (UNSAT-core/explication, PB pondéré et non pondéré, bench PB natif, largeur de bit-vector déclarée, choix du solveur, quantificateurs bornés,
Sumvariadique, MaxSAT, rationnels exacts) sont la zone de casse silencieuse d'un « suivre l'amont sur le noyau ». Notre suite teste nos extensions, pas leur noyau : un rebase peut passer les tests en cassant une capacité, parce que rien ne les couvre au point de jonction. G3 doit porter un grain de non-régression nommé sur ces 11 — sinon la posture de fork se décide sans filet, et c'est précisément la décision qu'on ne peut pas se permettre de prendre à l'aveugle.Reste de #14169
G2 (atterrissage des PRs amont — les 39 sont OPEN), G3 (posture, gated par les trois points ci-dessus), G4/G5 inchangés. Les deux défauts
DateTimemesurés en chemin sont tracés en #14445, non corrigés : #14169 interdit de toucher au fork avant G3, et corriger à la main les lignes exactes que l'amont réécrit garantit un conflit.Etat apres le bump de pointeur du 2026-09-04 — et une reserve que j'ai franchie moi-meme
Trois choses mesurees aujourd'hui changent l'etat de cette EPIC. La premiere me met en tort, je la mets en tete.
1. J'ai franchi la reserve que j'avais ecrite dans le rendu de G1
Le rendu de G1 (09:25Z) disait, mot pour mot :
Les deux defauts
DateTimemesures en chemin sont traces en #14445, non corriges : #14169 interdit de toucher au fork avant G3, et corriger a la main les lignes exactes que l'amont reecrit garantit un conflit.A 11:15Z j'ai merge #14594, dont le prealable etait la PR fork
MyIntelligenceAgency/Z3.Linq#26— qui corrige exactement ces deux defauts. #14445 est CLOSED. Je ne l'ai pas vu au moment du merge parce que je lisais le probleme d'ordonnancement de sous-module de #14594, pas la reserve qui vivait ici, sur une autre issue.La consequence n'est pas hypothetique, elle est mesuree — la zone de recouvrement est exacte :
ExpressionVisitor.csTheorem.csnotre fork #26 +19 / −1 +29 / −2 amont #95 (« Encode a DateTime as ticks rather than a file time ») +23 / −4 +29 / −7 amont #84 (« Read a DateTime back as UTC ») +2 / −0 +7 / −2 Memes deux fichiers, memes ordres de grandeur. Le conflit au rebase est desormais certain, et c'est celui que la reserve annoncait.
Ce qui attenue — et c'est une mesure, pas une excuse : #26 s'annonce dans son propre titre comme un port de
endjin#95, pas comme une correction independante. Le conflit a venir est donc de la classe la plus facile : notre version et l'originale disent la meme chose. La resolution attendue est « prendre l'amont », puis verifier que nos 87 tests passent toujours. Je l'ecris ici pour que la personne qui fera le rebase n'ait pas a la redecouvrir.Ce qui ne s'attenue pas : la reserve existait, elle etait juste, et je l'ai franchie. G3 herite d'un point de convergence de plus qu'il n'aurait du.
2. Le correctif n'atteignait aucun notebook — repare, mais la classe reste ouverte
En verifiant le grain G5 (« apres tout bump de pointeur : reexecuter »), j'ai mesure que le bump ne pouvait rien changer, pour une raison qui n'est pas rassurante :
.deploy/*.dllest suivi par git dans le fork (depuise09dae6, « commit .deploy DLLs for fresh-clone#rresolution »), et 17 notebooks s'y lient par#r "../Z3.Linq/.deploy/Z3.Linq.dll". La PR #26 a modifie les sources sans reconstruire ce binaire :ref blob .deploy/Z3.Linq.dlle09dae6(avant #26)83f99013040dc820080902640a1e9fcf6fa3cd1c6eab9579(apres #26)83f99013040dc820080902640a1e9fcf6fa3cd1cByte-identique. Controle dans les deux sens sur le binaire deploye :
ToUtcTicks0,ToFileTimeUtc1,FromFileTime1 — l'ancien encodage, intact. Autrement dit : sources corrigees, 87 tests verts, CI verte, et les 17 notebooks sur l'ancien code. Un defaut a toutes les lumieres vertes.Repare a l'instance par la PR fork #27 (reconstruction :
ToUtcTicks0→1,ToFileTimeUtc1→0,FromFileTime1→0 ; seuleZ3.Linq.dllbouge, les trois autres DLL restent byte-identiques aux paquets epingles, ce qui ecarte un bruit de reconstruction). Classe tracee cote fork en #28.3. Il n'y a aucune CI automatique sur le fork
Cherchant pourquoi #27 n'affichait aucun check :
build.ymldeclare bienon: pusheton: pull_request, et l'historique complet rend 4 runs, tousworkflow_dispatch— zeropull_request, zeropush, y compris sur le merge de #26 surmain.Cela qualifie ma propre decision de merge sur #14594 : le « 87/87 vert » que j'ai cite venait d'un dispatch manuel, pas d'un gate. Le chiffre est exact — je l'ai re-verifie firsthand en local sur le commit de merge (
dotnet test -c Release: echec 0, reussite 87, total 87, net8.0) — mais il n'a pas la valeur d'un gate. C'est la situation quesubmodule-maintenance.mdR3 nomme : l'absence de gate est le defaut. Hypothese la plus probable, pas encore levee : opt-in Actions specifique aux depots forkes.G5 — mesure de portee, pas de reexecution en aveugle
Avant de reexecuter, j'ai mesure l'exposition : sur les 17 notebooks lies a
.deploy, 0 contiennent la moindre occurrence deDateTime. Le changement de #26/#27 est entierement confine au marshallingDateTime(diff limite aux chemins concernes). Aucun notebook n'est donc expose a un changement de comportement.Cela reste un argument, pas une execution — alors j'ai passe l'artefact reconstruit au controle, lie par chemin, comme les notebooks le lient :
DLL chargee : sha1 abd7d898f930, 55808 octets (= la reconstruite, pas la deployee 74a242c1eacd) SOLVE -> x=3, y=4 contraintes : 3+4==7, x>1, y>1, x<y -> toutes satisfaites rc=0Le binaire se charge, le natif Z3 se resout, le solveur rend un modele correct.
Je ne declare pas G5 tenu pour autant : G5 nomme la reexecution de notebooks, et je n'en ai reexecute aucun. Ce que j'affirme est plus etroit et verifiable — l'exposition au changement est nulle (mesuree), et l'artefact reconstruit fonctionne sous le mode de liaison des notebooks (execute). Si le rebase de G3 fait bouger autre chose que
DateTime, cette mesure ne couvrira plus rien et G5 redeviendra du.Ce que G3 doit maintenant porter — quatre points, pas trois
Aux trois reserves du rendu de G1 s'ajoute celle-ci :
- Le point de convergence
DateTime.ExpressionVisitor.csetTheorem.csporteront un conflit certain avecendjin#95/#84. Resolution attendue : prendre l'amont, puis passer les 87 tests. Et verifier que.deploy/est reconstruit dans le meme geste — sans quoi le rebase, lui aussi, s'arretera aux sources.
Rappel des trois autres, inchangees : rangee #84 indexee sur son titre (lire le diff avant de la citer) · acceptance de #14445 corrigee · non-regression nommee sur les capacites hors-amont avant tout rebase — le point le plus lourd, et le seul dont je peux dire aujourd'hui qu'il est mieux arme qu'hier : les 87 tests couvrent bien nos extensions (mesure par symbole, pas par nom de fichier — un comptage par nom de fichier m'a d'abord fait croire a tort que
BitVecWidthetSolverKindetaient decouverts, alors qu'ils vivent dansBitVectorTheoryTests.csetConfigurableSolverTests.cs), et ils s'executent desormais reellement,$SkipTestetant passe afalsepar #26.G3 reste une decision user
G1 est rendu, donc G3 est decidable — c'est precisement ce que G1 devait produire. La posture de fork (suivre l'amont sur le noyau / assumer la divergence) engage les 17 notebooks : elle n'est pas mienne a trancher. Je la porte comme bloqueur user actif.
- Le point de convergence
Grain: MED/notebook-dotnet — lane myia-po-2025:CoursIA — prev: DEEP/lean #14770
[CLAIMED] lane myia-po-2025:CoursIA — G5 après bump #14605 : réexécuter les quatre notebooks explicitement nommés contre
Z3.Linq/.deploy/Z3.Linq.dllreconstruit au gitlink20984bfdf9.paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/07_Meal_Planner_Data_External.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb
Scope borné à l'exécution C.2 et aux sorties réelles de ces quatre notebooks. Aucun changement du fork, du gitlink, des sources notebook, du catalogue ou des autres notebooks.
Grain: MED/notebook-dotnet — lane myia-po-2025:CoursIA — prev: DEEP/lean #14770
[CLAIMED-AMEND] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb
Périmètre corrigé après exécution : livraison G5 3/4. Les trois notebooks exposés à la DLL sont réexécutés.
07_Meal_Planner_Data_External.ipynbreste résiduel : il déclare0 Z3, ne charge pas la DLL, et reconstruit le cache épinglé depuis un corpus RecipeML externe actuellement incomplet (6090 recettes récupérées contre 8286 épinglées). Le cache reste byte-identique ; aucune exécution 07 ni réécriture depuis le corpus partiel.[DELIVERED] lane myia-po-2025:CoursIA — G5 partiel 3/4 livré par PR #14829.
Réexécution C.2 complète de
06_Meal_Planner_Modelisation.ipynb,08_Meal_Planner_Patient_Capstone.ipynbet09_Meal_Planner_Convergence_Scale.ipynbcontre la DLL reconstruite de #14605 (abd7d898f930…, 55 808 octets), avec sources inchangées, outputs réels committés, zéro erreur et zéroprobeAddresses. Résultats déterministes inchangés ; seuls les timings machine-dépendants et un ratio dérivé varient.G5 complet non revendiqué. 07 reste résiduel : couche données
0 Z3, aucune référence DLL, corpus externe RecipeML partiellement indisponible (6090 recettes récupérées contre 8286 épinglées). Ni le notebook 07 nimealplan_cache.jsonn'ont été modifiés ; le cache épinglé est préservé.[RELEASED] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb
- added a commit that references this issue
on Sep 6, 2026 [CLAIMED] lane myia-po-2024:CoursIA -- G1 : recensement du recouvrement (28 PRs amont endjin vs notre fork pin
e09dae6) -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq/**G1 — Recensement du recouvrement amont/fork — lane
myia-po-2024:CoursIA, 2026-09-12T03:5xZ.See #14169(G1, préalable de G3).Deux corrections de premise avant la table (mesurées firsthand) :
- Le pin a bougé depuis la rédaction de l'issue.
origin/mainépingle20984bfd, pase09dae6— et les 6 commits entre les deux sont notre port d'endjin#84/feat(ml): add open exercises to ML.NET notebooks (ECE TP) #95 (DateTime round-trip via Utc ticks, fork PR QC SectorMomentum: Improve robustness (Sharpe 0.554) #26 + rebuild .deploy QC Crypto-MultiCanal: Revival - migrate to personal org and fix (BROKEN) #27, pour Z3.Linq: l'aller-retour DateTime est cassé des deux côtés (domaine <1601 en écriture, lecture locale au lieu d'UTC) #14445). Le census ci-dessous est fait sur20984bfd(le pin réel). Notre fork n'est pas stagnant : il absorbe l'amont au coup par coup. - L'amont a continué après les 28 PRs : +
#42et +#100–#110(11 PRs : refactors du solve path, BenchmarkDotNet, symboles signés/courts, uint/ulong bit-vectors). Le set ouvert actuel est 41 PRs, toutes couvertes ci-dessous. (Note de mesure :gh pr list --state opentronque à 30 par défaut — le compte de 41 est établi par--state all --limit 60croisé avec un sondage d'état PR-par-PR sur les 11 absentes du premier rendu : toutes OPEN.)
Table — 41 PRs amont ouvertes vs fork @
20984bfdLégende : REDONDANT = la capacité existe chez nous (preuve citée) · DIVERGENT = les deux côtés la traitent, autrement · NOUVEAU-POUR-NOUS = nous ne l'avons pas.
Bloc modernisation build & runtime
PR amont Notre équivalent @ 20984bfdVerdict #44 ZeroFailed build Endjin classique NOUVEAU-POUR-NOUS #45 .NET 10 + CPM + .slnxnet8.0, pas de CPMNOUVEAU-POUR-NOUS #42 / #47 MiaPlaza.ExpressionUtils 1.3.1 pin 1.2.0(Z3.Linq.csproj)NOUVEAU-POUR-NOUS #61 Microsoft.Z3 5.1.0 (natifs Linux + arm64) pin 4.12.2; commit forkba3b8b4: CI passée surwindows-latestparce que 4.12.2 n'a pas de natifs LinuxNOUVEAU-POUR-NOUS — l'item à plus haute valeur du set (débloque CI Linux + arm64) #94 génération/validation doc XML docstrings XML riches présentes ( Explanation.cs:6-9), pas d'organe de générationNOUVEAU-POUR-NOUS (outillage) Bloc suite de tests (phase A→)
PR amont Notre équivalent Verdict #48 tests Distinct partial-eval le fix partial-eval est le nôtre (#43/fc44dfa ; ExpressionVisitor.cs: 9 hitsPartialEval+ cheminEnumerable.Distinct/ToArrayl.491-533)REDONDANT #59 solve/composition ConfigurableSolverTests,SumVariadicTestsREDONDANT #65 marshalling types CollectionHandlingTests,ListCollectionTests,RecordEnvTheoryTests,BitVectorTheoryTestsREDONDANT #67 optimisation (Optimize, OrderBy) Optimization.cs,ISolveable{T}.cs(OrderBy/Descending),UnweightedPbTestsREDONDANT #69 failure modes + rewriters SolveStatus.Unknown(Explanation.cs),SudokuTheoremRewriter,ConditionalIteTestsREDONDANT #71 acceptance Sudoku/river crossing Z3.Linq.Examples/{Sudoku,RiverCrossing}+ testsREDONDANT Bloc marshalling & sortes
PR amont Notre équivalent Verdict #73 symboles laissés non-interprétés WitnessEvalTests+Theorem.cs(6 hits Uninterpreted/Witness)REDONDANT #74 retrait des contraintes-contournements de endjin#51 orthogonal : notre partial-eval (#43) est le fix de fond du même défaut NOUVEAU-POUR-NOUS (interne amont) #77 constantes réelles invariantes InvariantCulture: 5 hits (ExpressionVisitor.cs:2,Theorem.cs:3)REDONDANT #79 lecture de valeur d'un champ collection CollectionHandlingTests/ListCollectionTestsREDONDANT #80 lecture d'un symbole float en float notre read-back passe par Rational exact avant le TypeCode ( ExpressionVisitor.cs:844-845)DIVERGENT (exactitude-first vs float natif) #81 élément décimal sélectionné Rational.cs(24 hits),RationalExactTestsREDONDANT #84 DateTime relu en UTC porté : fork f0da578/6eab957(« DateTime round-trip via UTC ticks (port endjin#95) »)REDONDANT (nous l'avons porté) #86 satisfiabilité séparée de la solution SolveStatus(Satisfiable/Unsatisfiable/Unknown) via la surfaceExplain, gap B6 de #4616 — cité « so that "no solution" and "could not decide" are not conflated »REDONDANT #88 symboles short et enum aucun hit ( ExpressionVisitor.cs: pas de chemin enum/short)NOUVEAU-POUR-NOUS #90 mêmes sortes pour collections que scalaires notre modèle : tableaux Z3 ( ArrayExpr/MkSelect,ExpressionVisitor.cs:95-99,300-314)DIVERGENT #91 environnements anonymes Theorem.cs(3 hits anonymous) +RecordEnvTheoryTestsREDONDANT #92 conversions numériques par sorte Theorem.cs(4 hits RealSort/IntSort)REDONDANT #93 taille des collections depuis l'instance résolution d'environnement par instance ( TryResolveArrayEnvironment)REDONDANT #95 DateTime en ticks porté (cf. #84) REDONDANT Bloc sémantique de résolution
PR amont Notre équivalent Verdict #96 solve borné + « Z3 n'a pas pu décider » la moitié « ne pas décider » : REDONDANT ( SolveStatus.Unknown) ; la moitié bornes de solve (timeout/RLIMIT) : aucun hitNOUVEAU-POUR-NOUS (pour la moitié bornes) #98 entiers bornés à la plage de leur type aucun hit ( int.MinValue/type range : 0)NOUVEAU-POUR-NOUS #99 ternaires + bitwise/modulo réel ConditionalIteTests+ExpressionType.Modulo(ExpressionVisitor.cs:62)REDONDANT Vague récente #100–#110 (post-2026-09-05, hors census initial)
PR amont Notre équivalent Verdict #100 visitor en classe interne d'instance — NOUVEAU-POUR-NOUS (refactor, pas capacité) #101 fix de 2 défauts du code de solve-limits dépend de #96 (absent chez nous) NOUVEAU-POUR-NOUS #102 suite BenchmarkDotNet aucune référence BenchmarkDotNet NOUVEAU-POUR-NOUS (outillage perf) #103 cache réflexion par type — NOUVEAU-POUR-NOUS (perf) #104 idiomes C# 14 du solve path — NOUVEAU-POUR-NOUS (refactor) #105 extraction MemberClrType — NOUVEAU-POUR-NOUS (refactor) #106 extraction Assert pour dispatch Solver/Optimize SolverKind.csfait le dispatch autrementNOUVEAU-POUR-NOUS (refactor) #107 fusion des marshallers dans ReadZ3Value — NOUVEAU-POUR-NOUS (refactor) #108 demos en Spectre.Console single-file notre propre découpage Z3.Linq.Demo+Z3.Linq.ExamplesDIVERGENT #109 byte/sbyte/ushort comme entiers bornés aucun hit NOUVEAU-POUR-NOUS #110 uint/ulong comme bit-vectors nous avons l'opt-in explicite [BitVecWidth](BitVecWidthAttribute.cs,BitVectorTheoryTests) ; amont = implicite par type CLRDIVERGENT Synthèse — 18 REDONDANT · 4 DIVERGENT · 19 NOUVEAU-POUR-NOUS
- La surface sémantique de l'amont est déjà, pour l'essentiel, chez nous — et souvent par une machine plus riche :
SolveStatusdistingueUnknown(ce que fix(search/sudoku): STRING cells to LIST format (issue #82) #86/feat(Probas): add open exercises for ECE TP #96 cherchent), l'arithmétique décimale passe parRationalexact (vs ESGF: Creation notebooks QC manquants + exercices (13 gaps identifies) #81), les bit-vectors sont opt-in par attribut (vs feat(QC): add research QuantBook notebooks to projects missing them #110 implicite), les collections sont des tableaux Z3 natifs (vs fix: coordinator decisions - cherry-picks + STRING cells + duplicate line fix #90). Les 18 REDONDANT incluent notre fix partial-eval (QC Framework: Composite MomentumSector + RegimeSwitching #43) et notre port de GenAI: STRING cells cleanup - convertir 19 notebooks vers format LIST #84/feat(ml): add open exercises to ML.NET notebooks (ECE TP) #95 — l'absorption ciblée fonctionne déjà. - Le NOUVEAU se compose à 15/19 de build, outillage et refactors (ZeroFailed, .NET 10, CPM, doc XML, C# 14, extractions internes, benchmarks) — pas de capacités applicatives. Viennent s'y ajouter Cleanup: Supprimer les branches mergees et consolider GenAI_Series #61 (natifs Linux/arm64 du runtime Z3) : techniquement du build/runtime, mais c'est l'item à plus haute valeur du set — notre CI est littéralement coincée sur
windows-latestà cause de 4.12.2. Les 4 gaps sémantiques applicatifs : fix(genai): resolve Path import and GENAI_ROOT issues in Image notebooks #88 (short/enum), feat(Probas): add open exercises for ECE TP #96-bornes (solve limits), feat(GameTheory): add open exercises to 6 additional notebooks #98 (bornes de type des entiers), feat(QC): create deployable algorithms for ML notebook series #109 (byte/sbyte/ushort) — feat(QC): add research QuantBook notebooks to projects missing them #110 (uint/ulong) restant DIVERGENT puisque nous avons l'opt-in[BitVecWidth]. - Entrée de décision pour G3 (la décision reste user, cf. garde-fous) : un rebase wholesale de notre fork sur l'amont courant embarquerait 14 PRs de build/refactor sans valeur pour nous et entrerait en collision frontale avec les 4 DIVERGENT (Rational-exact, tableaux Z3, opt-in bitvec, découpage demos) — chaque collision est un de nos choix délibérés, pas un retard. Le modèle d'absorption ciblée déjà éprouvé (GenAI: STRING cells cleanup - convertir 19 notebooks vers format LIST #84/feat(ml): add open exercises to ML.NET notebooks (ECE TP) #95 portés en 6 commits) est celui que la table documente comme viable : porter Cleanup: Supprimer les branches mergees et consolider GenAI_Series #61 d'abord (débloque Linux), puis au besoin fix(genai): resolve Path import and GENAI_ROOT issues in Image notebooks #88/feat(Probas): add open exercises for ECE TP #96-bornes/feat(GameTheory): add open exercises to 6 additional notebooks #98. G4 (proposer en amont WeightedAtLeast/AtMost/Exactly, UNSAT-core
Explanation/AssertAndTrack, tactiques) reste gated feu vert user.
Grain: MED/research-code — lane myia-po-2024:CoursIA — prev: DEEP/research-code #15645 (MERGED).
- Le pin a bougé depuis la rédaction de l'issue.
3 remaining items
- added a commit that references this issue
on Sep 15, 2026 [CLAIMED] lane myia-po-2024:CoursIA — port endjin#61 (Microsoft.Z3 5.1.0, natifs Linux/arm64) en extraction selective, option C arbitree par le user 2026-09-14 — paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq/** -- 2026-09-15T04:35Z
G3 option C — première extraction LIVRÉE : endjin#61 (Microsoft.Z3 5.1.0, natifs Linux/arm64)
PR fork MyIntelligenceAgency/Z3.Linq#29 (branche
feature/z3-5.1.0-selective, tête3d01c14, rebasée sur notre pin20984bfd— pas sur la base amont empilée #47). Le besoin qui la motive est écrit dans le body : 4.12.2 = natifs win-x64/osx-x64 seulement ; c'est ce qui décide ce qu'on exécute en CI ubuntu et sur les machines étudiants arm64 (recensement G1 : « le déblocage le plus stratégique »).Preuves à la tête : hash SHA-256 du paquet conforme au pin ; build 0/0 sous TreatWarningsAsErrors ; 87/87 tests verts contre 5.1.0 ;
.deploy/régénéré (Microsoft.Z3.dll 5.1.0, libz3.dll win-x64 5.1.0, Z3.Linq.dll rebuild) et les DLL committées résolvent en smoke (Z3 5.1.0.0). La preuve linux-x64 en conditions réelles vient du CI fork (InvokeBuildPreBuild → EnsureZ3Packagesur ubuntu-latest), en cours sur la PR.Découverte incident (pré-existant, hors périmètre) : le
Z3.Linq.Democrashe à la section ValueTuple (ConstructFromModelNotSupportedException) à l'identique au pin sous 4.12.2 — défaut antérieur du fork, invisible en CI (le Demo n'y tourne pas). À tracker séparément si besoin ; non traité par cette extraction.Non portés (explicités, per l'arbitrage : « un non-porté raisonné vaut mieux qu'un suspens »)
Bloc amont Raison du non-port #44 ZeroFailed ( .zf/)Aucun besoin CoursIA : notre scaffold InvokeBuild endjin fait le travail ; le hook PreBuild de #61 a été porté dans build.ps1à la place#45 .NET 10 + CPM + .slnxAucun besoin : net8.0 tient, le pin vit dans le csproj (le triple-épinglage version/hash/csproj est documenté dans le body de la PR fork) #47 MiaPlaza.ExpressionUtils 1.3.1 (+ breaking adapt) Aucun besoin identifié ; 1.2.0 suffit. #61 y était empilé — c'est précisément pourquoi l'extraction est replantée sur notre pin #94 doc XML générée/validée Aucun besoin CoursIA Essentiel de la suite de tests (#48, #59, #65, #67, #69…) La couverture actuelle (87 tests, dont la régression #14445) tient le pin ; la vague tests amont suit G5 (gâtée sur l'arrivée effective des PRs amont) Le pin reste notre référence (
20984bfdjusqu'au merge de la PR fork, puis bump du pointeur sous-module par PR dédiée CoursIA).Grain: DEEP/research-code — lane myia-po-2024:CoursIA — [CLAIMED] posé 2026-09-15T04:35Z (issuecomment-5674749461)
[CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/06_Meal_Planner_Modelisation.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/07_Meal_Planner_Data_External.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/08_Meal_Planner_Patient_Capstone.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/09_Meal_Planner_Convergence_Scale.ipynb -- G5 : réexécution des quatre carnets du grain contre le DLL du pointeur courant (
fddd5867), postérieur aux deux bumps #17318 et #17608Le grain G5 est nommé par l'EPIC lui-même : « Après tout bump de pointeur de submodule :
SMT/Z3-Linq2Z3/06,07,08,09réexécutés, outputs committés (C.2). Un bump non accompagné de la réexécution est une régression silencieuse. »Mesure préalable, au pointeur
origin/main: le gitlink est àfddd5867depuis24d629c54f(#17608) et le dernier commit touchantZ3-Linq2Z3/est67fe2da5c5(renommage d'API, antérieur au bump) — les quatre carnets n'ont donc pas été réexécutés contre le DLL courant.G5 — les quatre carnets après les deux bumps de pointeur
Prémisse mesurée. Le gitlink est à
fddd5867— avancé pard4da09eb83(#17318, 2026-09-22) puis24d629c54f(#17608, 2026-09-24). Le dernier commit touchantZ3-Linq2Z3/est67fe2da5c5(2026-09-20,git mvde renommage d'API), antérieur aux deux bumps. Les quatre carnets n'ont donc pas été réexécutés contre le DLL courant : c'est exactement le cas que G5 vise.07ne peut pas voir le bump — par construction07_Meal_Planner_Data_External.ipynbne contient aucune directive#r, dans aucune de ses dix cellules de code. Son premier bloc l'écrit lui-même :// ---- dependances (0 Z3 : purement data-engineering) ----. Il ne charge niZ3.Linq.dll, niMicrosoft.Z3.dll, niExpressionUtils.dll.Le bump est donc structurellement inobservable par ce carnet : le réexécuter testerait le corpus de données et le runtime .NET, pas le pointeur. C'est une réponse plus forte qu'une comparaison d'exécutions — elle ne dépend d'aucune donnée amont.
06,08,09le voient, et sont inertesLes trois chargent les trois DLL depuis le pointeur courant :
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll" #r "../Z3.Linq/.deploy/ExpressionUtils.dll" #r "../Z3.Linq/.deploy/Z3.Linq.dll"Réexécutés dans un worktree de
origin/maindont le sous-module est initialisé àfddd5867(.deploy/Z3.Linq.dll=b3639a8affd7ed54a019f7aa591eaaec2ce54638,Microsoft.Z3.dll=08220fa561ce5b7a99bb65a669a959935eb9907b), les outputs committés et les outputs réexécutés sont identiques modulo les nombres :Carnet lignes de sortie comparées divergences, tout nombre neutralisé ce que portent les nombres divergents 06100 0 — 0858 0 trois Stopwatchen prose (« résolue en 86 ms » → « 158 ms »)0954 0 un ratio dérivé de deux chronomètres ( 661x→411x)Aucun
errorde cellule,execution_countcontigus. Les deux bumps (#17318 lecture courteInt16, #17608 bornes de symboles scalaires) ne changent aucun résultat de ces trois carnets.Condition de reproductibilité — non documentée à ce jour
Les enregistrements committés portent
System.Linq.Expressions, Version=10.0.0.0. Une exécutionpapermill -k .net-csharppar défaut sur cette machine rend9.0.0.0:Sonde Runtime System.Linq.Expressionspapermill -k .net-csharp.NET 9.0.20Version=9.0.0.0idem + DOTNET_ROLL_FORWARD=LatestMajor.NET 10.0.12Version=10.0.0.0← égale l'enregistrement committéSonde minimale d'une cellule, DLL du pointeur chargée par
#r. Conséquence pratique : rejouer ces carnets sans la variable d'environnement ne reproduit pas les enregistrements, et aucun organe ne le voit — leKernel drift guardlitmetadata.language_info.version, pas l'identité d'assembly. Le seul témoin de cette version dans les sorties est la ligneCS1701(« En supposant que la référence d'assemblySystem.Linq.Expressions, Version=…utilisée parZ3.Linqcorrespond à l'… »), présente dans les trois carnets.06porte un enregistrement d'une génération de noyau antérieuremetadata.language_info.version:06= 12.0,07/08/09= 13.0. Une réexécution de06rend 13.0. L'écart n'est pas un défaut de code, mais l'enregistrement de06date d'un noyau qui n'est plus celui de la série.Défaut découvert en aval : le corpus de
07tronqué passait pour complet07litdata/meals/(gitignoré) et écritdata/meals/mealplan_cache.json— le seul fichier de ce dossier qui soit committé.download_meal_data.pytestait la présence du corpus RecipeML par l'existence du dossier : une passe interrompue (49 batches sur 110, mesuré) était ensuite annoncée « Corpus deja complet » et rien n'était téléchargé. Un corpus tronqué produit un cache tronqué en silence.→ #17867 (ouverte par cette lane) : marqueur de fin de passe + passe reprenable. Sur
mainaujourd'hui,07n'est donc pas reproductible depuis un clone frais et la cause de ce blocage se taisait.Aucun carnet n'est committé
C.3 est HARD : « un agent ne commit QUE les notebooks dont il a modifié une cellule source ». Ces réexécutions sont des vérifications ; elles se rapportent ici, elles ne se committent pas.
Le committer produirait, mesuré, 1140 lignes ajoutées / 839 supprimées sur trois carnets — du bruit de chronomètre et un re-découpage des tableaux
sourcepar papermill (08: 374 ajouts pour 131 suppressions, asymétrie qui ne doit rien au bump). Et06porterait un saut delanguage_info12.0 → 13.0, qui exigerait à lui seul un## Diagnostic dérive.Ce qui reste ouvert sur ce grain
06: aligner son enregistrement sur le noyau courant (13.0) — geste qui exige une réexécution et donc, lui, un commit de carnet.- La condition
DOTNET_ROLL_FORWARD=LatestMajorn'est écrite nulle part dans le dépôt.
- added a commit that references this issue
on Sep 26, 2026 [INFO] G5 — le bump #17906 (fddd586 -> 3b42bcc) est docs-only :
.deploybyte-identique, re-execution NON dueG5 dit : « Apres tout bump de pointeur de submodule :
SMT/Z3-Linq2Z3/06,07,08,09reexecutes, outputs commites (C.2). Un bump non accompagne de la reexecution est une regression silencieuse. » Le bump #17906 (mergee 2026-09-27T04:14Z) n'a touche que le gitlink, aucune reexecution ne l'accompagne — je l'ai donc instruit avant de le traiter comme dette.Mesure (clone frais du fork, 2026-09-29T22:5xZ, lane
myia-po-2024:CoursIA) :Mesure Resultat gitlink porte par main160000 commit 3b42bcc6004e3803b00b350cebe8b8061c067ee5(git ls-tree origin/main -- .../SMT/Z3.Linq)git diff --stat fddd586 3b42bcc1 fichier : DIVERGENCE_STATUS.md, +109 lignes — rien d'autre.deploy/aux deux pointeursles 4 DLL byte-identiques : ExpressionUtils.dllffecf33b,Microsoft.Z3.dll9197e6b4,Z3.Linq.dll1e1dc35e,libz3.dll8ccefd8fConsequence : ce bump deplace de la documentation, pas du code exécutable. Les outputs commites de 06/07/08/09 (reexecutes le 2026-09-06 par #14829 sous ce meme
Z3.Linq.dll) restent exacts pour le pointeur courant — aucune reexecution n'est due, et en faire une serait un cycle a blanc.G5 redevient due des qu'un bump touche
.deploy/(ou tout fichier desolutions/) : le critere est le diff du sous-module, pas le simple mouvement du pointeur. C'est ce que cette mesure fixe comme test.Rappel de la meme session : la verification R3 2/2 sur
3b42bcc(clone frais,dotnet test solutions/Z3.Linq.sln, 102/102 verts, machine po-2024 distincte de po-2023) est postee sur #17906 (issuecomment-5900628177).- added a commit that references this issue
on Oct 4, 2026 [CLAIMED] lane myia-po-2025:CoursIA — confronter le body de cet EPIC à main (tous ses enfants sont fermés, cases non cochées restantes ; mesure c.5985511451 sur #13906) puis fermer avec preuve par case, réécrire le body sur le reste réel, ou replier
Claim posé par le coordinateur (ai-01) au dispatch.
Fermeture de l'EPIC — preuve par case (grain de consolidation, dispatch ai01-deepq du 04/10 23:20, claim c.5985517854)
Lecture integrale du body et des 18 commentaires, confrontation de chaque case a
mainet a l'etat amont mesure au 2026-10-05. Trois cases livrees, deux cases gatees deplacees en #19237 (ouverte AVANT cette fermeture).Case Verdict Preuve G1 recouvrement LIVREE Ledger docs/ledgers/14169-z3linq-upstream-overlap.mdsurorigin/main(blobae86cdd4cba6, verifiegit ls-tree), livre par #14444 ; recensement complet po-2024 du 2026-09-12 sur le pin reel20984bfd,[RELEASED]2026-09-13G2 suivre endjin#43 DEPLACEE #19237 Mesure du jour : endjin/Z3.Linq#43OPEN,REVIEW_REQUIRED, non merged ; 45 PRs ouvertes amont. Attente externe non bornee — suivie en #19237 avec critere de fermeture observable (gh pr view 43 --repo endjin/Z3.Linq)G3 posture de fork TRANCHEE Decision user du 2026-09-14 : option C (extraction selective), relayee dans le fil au 2026-09-14T17:51Z. Premiere extraction livree (endjin#61, Microsoft.Z35.1.0 natifs Linux/arm64 -> fork PR MyIntelligenceAgency/Z3.Linq#29, encore OPEN). La posture est consommee : le pin a avance par extractions/bumps successifs (20984bfd->fddd586->3b42bcc->8c7ae3e8courant)G4 proposer en amont DEPLACEE #19237 Conditionnel a un feu vert user depuis l'arbitrage option C (G3) — dormant par decision, garde-fou d'origine conserve (aucune nouvelle soumission amont sans feu vert). Home : #19237 G5 notebooks tiennent LIVREE Protocole applique a chaque bump : #14605 -> re-exec 3/4 (#14829, 07 hors DLL par construction) ; #17318 + #17608 -> les quatre reinstruits 2026-09-25 ; #17906 -> docs-only atteste 2026-09-29 ( .deploybyte-identique, re-exec non due) ; #19094 (bump courant8c7ae3e8) -> doc-only, verification sous-module par ai-01 avant mergePourquoi fermer plutot que laisser ouvert. La mesure de reference (#13906, c.5985511451) classe cette EPIC « 5/5 enfants fermes, 5 cases non cochees, aucune PR ouverte ne la cite ». Trois cases sont livrees avec preuve ; les deux restantes sont des attentes gatees (externe pour G2, user pour G4) qui ne deviendront JAMAIS actionnables par le seul fait de rester ici — les garder dans ce body, c'est exactement le « body que personne ne confronte a l'etat reel » que la mesure denonce. Elles ont un home nomme, #19237, ouvert avant la fermeture.
Non verifie par cette passe : le contenu des PRs amont ouvertes au-dela de leur denominateur (45) — le suivi fin appartient a #19237 quand endjin bougera.
Le body porte en tete le bloc « Etat mesure au 2026-10-05 » ; le texte d'origine est conserve integralement en dessous, cases livrees cochees.
Ce qui vient de se passer
Le 2026-09-01 à 08:03Z, la lane
myia-po-2024:CoursIA-2a ouvert endjin/Z3.Linq#43 — le correctiffc44dfa(partial-eval du corps de contrainte avant visite, qui débloque Z3.Linq sous .NET Interactive). C'était le dernier axe de l'EPIC #1206.Le mainteneur endjin a répondu cinq minutes plus tard :
(#29 upstream est notre issue, ouverte par
jsboigele 2023-08-30.)Puis, entre 11:18Z et 21:48Z le même jour, 28 PRs ont été ouvertes sur
endjin/Z3.Linqpar ce mainteneur. Mesure du 2026-09-01T22:00Z (gh pr list --repo endjin/Z3.Linq --state all --limit 60) :.slnx), #47 (MiaPlaza.ExpressionUtils 1.3.1), #94 (doc XML)Microsoft.Z35.1.0 — binaires natifs Linux et arm64)Un dépôt amont gelé depuis des années se remet en mouvement le jour où nous y poussons un correctif. C'est une bonne nouvelle, et c'est aussi un problème de synchronisation : notre fork
MyIntelligenceAgency/Z3.Linqest épinglé àe09dae6, et quatre notebooks publiés en dépendent.Pourquoi c'est stratégique et pas cosmétique
DateTimeGenAI: STRING cells cleanup - convertir 19 notebooks vers format LIST #84/feat(ml): add open exercises to ML.NET notebooks (ECE TP) #95, satisfiabilité séparée fix(search/sudoku): STRING cells to LIST format (issue #82) #86, solve borné feat(Probas): add open exercises for ECE TP #96). Si l'amont les livre autrement, notre fork porte du code redondant et divergent — le pire des deux.Microsoft.Z35.1.0. Notre série SMT est aujourd'hui contrainte par le runtime Z3 disponible ; c'est exactement le genre de déblocage qui change ce qu'on peut exécuter en CI et sur les machines des étudiants.Grains — ordonnés, chacun livrable seul
e09dae6), et où (fichier:ligne). Sortie : un tableau à trois colonnes — PR amont · notre équivalent · verdict parmiREDONDANT/DIVERGENT/NOUVEAU-POUR-NOUS. C'est le préalable de tous les autres grains : sans lui, on rebase à l'aveugle ou on propose ce qui existe déjà. Genreresearch-code, tier MED.MyIntelligenceAgency/Z3.Linqune fois ses PRs atterries) ou assumer la divergence. Décision user — elle engage les quatre notebooksSMT/Z3-Linq2Z3/et le miroir Python. G1 est ce qui la rend décidable.WeightedAtLeast/WeightedAtMost/WeightedExactly+ benchpb-bench, Z3.Linq: le pseudo-booleen est le dernier item du backlog B1-B10, et c'est l'encodage qui gagne la convergence a l'echelle (nb 09) #10605), l'UNSAT-core (Explanation.cs+AssertAndTrack), les tactiques (feat(smt-z3,#1206): bump Z3.Linq submodule to tactics-B10 (fork PR #19) #10457). Une PR par capacité, l'usage endjin.SMT/Z3-Linq2Z3/06,07,08,09réexécutés, outputs committés (C.2). Un bump non accompagné de la réexécution est une régression silencieuse.Garde-fous
user-blocker-signaling).Liens
MyIntelligenceAgency/Z3.Linq@e09dae6, submoduleMyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq