[isabelle-dev] HOL-Proofs slow
makarius at sketis.net
Mon Oct 22 21:52:11 CEST 2012
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
> This matches by offline analysis.
> As a first step, cf. the following changeset:
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 ...
More information about the isabelle-dev