[isabelle-dev] HOL-Proofs slow

[Florian Haftmann]

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

With this I get the following quite reasonable figures

> Building HOL ...
> Finished HOL (0:02:51 elapsed time, 0:05:14 cpu time, factor 1.83)
> Building HOL-Main ...
> Finished HOL-Main (0:02:03 elapsed time, 0:03:41 cpu time, factor 1.79)
> Building HOL-Plain ...
> Finished HOL-Plain (0:00:44 elapsed time, 0:01:15 cpu time, factor 1.70)
> Building HOL-Proofs ...
> Finished HOL-Proofs (0:07:52 elapsed time, 0:14:12 cpu time, factor 1.80)

but we should avoid isatest measurements first.

Nevertheless I have been thinking about rephrasing these proofs anyway,
let's see.

> HOL-Proofs has become very slow, see
> http://www4.in.tum.de/~wenzelm/test/stats/mac-poly64-M8/HOL-Proofs.png 

Btw. how do those graphs come into being?  The still official devel
snapshot page does not link there…

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121022/152179ee/attachment.sig>