[isabelle-dev] HOL-Proofs slow

[Makarius]

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