[isabelle-dev] HOL-Proofs slow
florian.haftmann at informatik.tu-muenchen.de
Mon Oct 22 19:10:09 CEST 2012
>> 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:
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,
> HOL-Proofs has become very slow, see
Btw. how do those graphs come into being? The still official devel
snapshot page does not link there…
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 259 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev