On Mon, 22 Oct 2012, Florian Haftmann wrote:
Bijection then produced this:
The first bad revision is:
changeset: 49948:744934b818c7
user: haftmann
date: Sat Oct 20 09:12:16 2012 +0200
summary: moved quite generic material from theory Enum to more
appropriate places
I can't say for sure if this is a correct result of the bijection, but
it fits approximately in the time interval from my last successful
(fast) test of everything.
It is indeed the above changeset, notably the two code_simp invocations
here:
http://isabelle.in.tum.de/repos/isabelle/rev/744934b818c7#l9.7
This matches by offline analysis.
As a first step, cf. the following changeset:
http://isabelle.in.tum.de/reports/Isabelle/rev/8b50286c36d3
Testing this verson manually gives me 0:25:05 elapsed time total, while it
is normally 0:16:30 on this machine with 8 cores and "build -j4 -a".
In fact, one of the advantages of manual testing is that you immediately
suffer from the effect yourself if something is wrong.
I am busy elsewhere (in Orleans) the coming days ...
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
