> Am 12.05.2018 um 00:27 schrieb Makarius <makar...@sketis.net>: > > Isabelle/fad29d2a17a5 > parent: 68072:493b818e8e10 > parent: 68070:8dc792d440b9 > user: immler > date: Thu May 03 15:07:14 2018 +0200 > merged; resolved conflicts manually (esp. lemmas that have been moved > from Linear_Algebra and Cartesian_Euclidean_Space) > > > That merge is a total mess -- as a consequence of disregarding long > established customs from README_REPOSITORY: It is a mess, indeed. But it is "almost" a trivial merge: the conflicts with the other branch isabelle/0a2a1b6507c1 to isabelle/8dc792d440b9 are mostly cosmetic changes, local to proofs.
Now I think that it might have been over-ambitious to get all of these developments into the repository in just two steps (afp/5bbb50b with isabelle/0a2a1b6507c1 and then the move to isabelle/493b818e8e10). For the sake of a cleaner history, it might have been worth re-doing those changes in smaller steps, but I could not spend an arbitrary amount of time on this project. Now the changesets do at least reflect the actual history (it did take me two weeks to complete the parent 493b818e8e10). And I did not want to keep those changes in private drawers for much longer. These changesets are actually the result of reviving (and completing) work that Johannes (Hölzl) started in November 2017. Given this long time span, everything actually worked out reasonably well. I did notice that those changes caused issues with timeouts in some AFP sessions, and simply "fixed" those on the spot (e.g., the ones in afp/85324e3 and afp/2ff575e hinted at problems caused by incorporating syntax for FuncSet into Complex_Main). This was just to keep everything going, but I was well aware that I needed to take a closer look at the problems caused there and resolve them properly (e.g., not exposing FuncSet-syntax in Complex_Main). It is great that we have this detailed history of performance measurements, otherwise I would not have dared to push changes that caused timeouts in some of the sessions, not knowing about degrading performance in others... Makarius, thanks a lot for maintaining this infrastructure and also keeping an eye on the performance figures! > Maybe he can sort that out. I was planning to investigate this in the course of this week. Fabian
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
