> 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.


Attachment: smime.p7s
Description: S/MIME cryptographic signature

isabelle-dev mailing list

Reply via email to