fix(deploy,#14445): reconstruire .deploy/Z3.Linq.dll — le correctif DateTime n'atteignait aucun notebook - #27
Merged
Conversation
…eaches the notebooks The round-trip fix landed in the sources and its 87 tests, but not in the artifact the notebooks actually load. `.deploy/*.dll` is git-tracked (e09dae6, "commit .deploy DLLs for fresh-clone #r resolution") and 17 CoursIA notebooks bind to it via `#r "../Z3.Linq/.deploy/Z3.Linq.dll"`. PR #26 changed ExpressionVisitor.cs and Theorem.cs but did not rebuild that binary, so the blob was byte-identical across the fix (83f9901 both sides) and every notebook kept running the old file-time encoding. Measured, with the control in both directions: symbol deployed(old) rebuilt(new) ToUtcTicks 0 1 ToFileTimeUtc 1 0 FromFileTime 1 0 Only Z3.Linq.dll changes: ExpressionUtils.dll, Microsoft.Z3.dll and libz3.dll are byte-identical to what the pinned packages restore, which also rules out spurious rebuild noise. dotnet test Release: 87/87 passed, 0 failed (local, net8.0). See #14445, jsboige/CoursIA#14169 (G5).
4 tasks
jsboige
added a commit
to jsboige/CoursIA
that referenced
this pull request
Sep 4, 2026
…DateTime atteint enfin les 17 notebooks (#14605) Le bump precedent (#14594, gitlink 6eab9579) a porte le correctif d'aller-retour DateTime dans les sources de Z3.Linq et leurs 87 tests, mais pas dans l'artefact que les notebooks chargent : `.deploy/Z3.Linq.dll` est suivi par git et 17 notebooks s'y lient par `#r "../Z3.Linq/.deploy/Z3.Linq.dll"`. Le blob etait byte-identique de part et d'autre du correctif (83f99013), donc les 17 notebooks tournaient encore sur l'ancien encodage file-time. Controle positif sur le blob `.deploy/Z3.Linq.dll` a travers les trois refs du fork : e09dae6 (avant correctif) -> 83f99013040d 6eab9579 (bump precedent) -> 83f99013040d IDENTIQUE : reproduit l'echec 20984bfdf9 (ce bump) -> 552613aae72d DIFFERENT : binaire reconstruit La ligne du milieu est ce qui donne sa valeur aux deux autres : elle mesure l'echec exact que cette PR corrige, sur l'objet exact qu'elle corrige. Symboles dans la DLL reconstruite : ToUtcTicks 1, ToFileTimeUtc 0, FromFileTime 0 (avant : 0 / 1 / 1). 55808 octets contre 52736. Reconstruit par la PR fork MyIntelligenceAgency/Z3.Linq#27, mergee ; le commit 20984bfdf9 est atteint depuis `origin/main` du fork (il en est la tete), donc l'ordre sous-module puis parent de submodule-maintenance.md est respecte. Exposition mesuree : 0 des 17 notebooks n'utilise DateTime, donc aucun changement de comportement attendu. Artefact verifie sous le mode de liaison par chemin des notebooks : SOLVE -> x=3, y=4, contraintes satisfaites, rc=0. Classe du defaut tracee cote fork : MyIntelligenceAgency/Z3.Linq#28. See #14169 (G5), #14445.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Le defaut
Le correctif d'aller-retour
DateTime(#26) a atterri dans les sources et leurs 87 tests, mais pas dans l'artefact que les notebooks chargent..deploy/*.dllest suivi par git depuise09dae6(« commit .deploy DLLs for fresh-clone#rresolution »), et 17 notebooks dejsboige/CoursIAs'y lient par#r "../Z3.Linq/.deploy/Z3.Linq.dll". La PR #26 a modifieExpressionVisitor.csetTheorem.cssans reconstruire ce binaire.Consequence mesuree : le blob
.deploy/Z3.Linq.dllest byte-identique de part et d'autre du correctif..deploy/Z3.Linq.dlle09dae6(avant)83f99013040dc820080902640a1e9fcf6fa3cd1c6eab9579(apres #26)83f99013040dc820080902640a1e9fcf6fa3cd1cLes 17 notebooks continuent donc d'executer l'ancien encodage file-time — c'est-a-dire exactement les deux defauts que #26 declare corriges.
Le controle, dans les deux sens
Un symbole qui apparait ne prouve rien seul ; ce qui discrimine, c'est que l'ancien disparaisse en meme temps.
ToUtcTicksToFileTimeUtcFromFileTimeFromFileTimeUtcPortee minimale — et pourquoi c'est aussi un controle
Des quatre DLL deployees, une seule change :
.deployvs paquet epingle restaureExpressionUtils.dll72e022da33e1)Microsoft.Z3.dll08220fa561ce)libz3.dll1cf7c29aae8a)Z3.Linq.dll74a242c1eacd->abd7d898f930)Les trois inchangees ecartent l'hypothese d'un bruit de reconstruction : si la chaine produisait des binaires non deterministes, elles auraient bouge aussi. Seul le projet dont la source a change bouge.
Verification
Execute localement sur .NET 10.0.111, sur le commit de cette branche.
Ce que cette PR ne fait pas
Elle repare l'instance, pas la classe. Rien ne relie aujourd'hui une modification de
solutions/Z3.Linq/**a une reconstruction de.deploy/**: le meme ecart peut se reproduire au prochain correctif, avec la meme signature silencieuse (sources vertes, tests verts, notebooks sur l'ancien binaire). Un garde dedie est a ouvrir cote fork ; je le trace separement plutot que de l'melanger a une reparation qui doit rester lisible.Ref : #26, #14445,
jsboige/CoursIA#14169(grain G5).