[isabelle] Isabelle Slowdown


thanks for all the answers to my last question. Now I have made up an
ML-tactic to address my problem, that looks tail-recursive, but I
managed to run into the problem that after about 25k subgoals of a proof
with more than 50k subgoals Isabelle gets very slow and needs about
1.2Gb of RAM. It gets that slow that it needs about 10mins to solve a
subgoal that can be solved in 10secs if you copy it out of the context
and solve it alone. Is there a way to minimize Isabelle's bookkeeping
during a proof even further? I mean all subgoals of a proof are somehow
independent from each other as are the theorems. I will probably not use
a theorem to prove another one, so all I am interested in is the fact
that Isabelle can prove all subgoals of a goals and not more. I am not
really interested in a proof tree, since it will be far too big to
inspect, I rather log the subgoals to a file, so that one can inspect
them and verify their proofs. 

Maybe the tactic has some kind of "memory leak", I can post it here if
you want to analyze it, but it is a little lengthy. 


Dominik Luecke                 Phone +49-421-218-64265
Dept. of Computer Science      Fax   +49-421-218-9864265
University of Bremen           luecke at tzi.de           
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x2D82571B

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.