Email Gateway (Aug 19 2022 at 13:30): Email Gateway (Aug 19 2022 at 13:30):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I am posting this as a reminder for me and other people who get bitten
by some annoying behaviour of Isabelle 2013 which I describe below (and
cannot switch to a more current version of Isabelle).
Due to some external libraries I use, I am currently stuck on Isabelle
2013. As Peter already mentioned a few months ago (here or on
isabelle-dev), when a tactic fails, it prints all subgoals, independent
of the goals_limit option (I tried setting it with "declare" before the
proof and with "using" in the proof).
When the goal is large (in my current example: 41 subgoals, with up to
60-70 lines each), these take very long to print (around 6 minutes on my
8-core i7 machine).
As a work-around, I modified src/Pure/Isar/proof_display.ML, setting
"limit = true" in the function "string_of_goal", thus making it honour
the goal_limit option.
-- Lars
signature.asc
Last updated: Apr 19 2024 at 12:27 UTC