Email Gateway (Aug 18 2022 at 10:44): Email Gateway (Aug 18 2022 at 10:44):From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,
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.
Regards,
Dominik
Last updated: May 03 2024 at 04:19 UTC