Re: [isabelle] goals_limit in error-output

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

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,
        {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.

