[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