[isabelle-dev] HOL-Proofs slow

Makarius makarius at sketis.net
Sun Oct 21 23:32:55 CEST 2012


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


I first thought it would be related to 1167c1157a5b (haftmann on 
src/Pure/Proof/extraction.ML), which is not immediately easy to follow in 
every detail.


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.


 	Makarius


More information about the isabelle-dev mailing list