Email Gateway (Aug 19 2022 at 10:55): Email Gateway (Aug 19 2022 at 10:55):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I'm working with really large proof states, that may take tens of
seconds only to pretty-print (The pretty-printer seems to scale very
poorly to large terms).
In order to keep interactive proving manageable, I use goals_limit=1,
which drastically reduces the response-time until I see the next proof
state.
However, if a proof method fails, it dumps the whole proof state to the
output buffer, and goals_limit is not applied there. This feature
(introduced newly in Isabelle2013) again renders interactive proving for
big goal states unmanageable: In my case, you have to wait approx. 1
minute only to see that your proof method failed, and this one minute
contains a few milliseconds to find that the method actually fails, and
one minute to pretty print the error message.
Is there a way to deactivate the goal-state being dumped with the error
message?
Email Gateway (Aug 19 2022 at 11:04):From: Makarius <makarius@sketis.net>
On Wed, 17 Apr 2013, Peter Lammich wrote:
I'm working with really large proof states, that may take tens of
seconds only to pretty-print (The pretty-printer seems to scale very
poorly to large terms).
The pretty printer as such is relatively fast, it depends what else you
have in the context to make it slow (e.g. abbreviations). Independently
of that, any system has its range where it works well and breaks down when
stretched too far, as usual.
In order to keep interactive proving manageable, I use goals_limit=1,
which drastically reduces the response-time until I see the next proof
state.However, if a proof method fails, it dumps the whole proof state to the
output buffer, and goals_limit is not applied there. This feature
(introduced newly in Isabelle2013) again renders interactive proving for
big goal states unmanageable: In my case, you have to wait approx. 1
minute only to see that your proof method failed, and this one minute
contains a few milliseconds to find that the method actually fails, and
one minute to pretty print the error message.Is there a way to deactivate the goal-state being dumped with the error
message?
You can edit Isabelle2013/src/Pure/Isar/proof_display.ML to change the
string_of_goal function like this:
fun string_of_goal ctxt goal =
Pretty.string_of (Pretty.chunks
[pretty_goal_header goal,
Goal_Display.pretty_goal
{main = Config.get ctxt Goal_Display.show_main_goal, limit = true} ctxt goal]);
This is mainly for Isar error messages. There are a few more situations
where goal states are printed.
I shall see how to refine that again for the next release, although that
is still far ahead.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC