[isabelle-dev] serious performance problems after update?
obua at in.tum.de
Sun Oct 28 00:15:19 CEST 2007
I am experiencing a major breakdown of performance after updating my
Isabelle system. I am using large records and locales, could this be
the reason? Oddly, while it takes longer than expected to parse a
record declaration, the real problem seems to be the statement of
lemmas after it (not even their proofs?). In one theory, stuff that used
to run through in about 5 seconds is now taking more than 30 minutes
(and counting, I am stopping the process now). And stuff that used to
run through in 12 minutes, now takes more than 3 hours (and counting, I
am stopping that one also).
Is noone else experiencing problems like this?? Could it have
something to do with the new type inference algorithms?
More information about the isabelle-dev