[isabelle-dev] serious performance problems after update?

Steven Obua 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?

Steven



More information about the isabelle-dev mailing list