[isabelle] goals_limit in error-output
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
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
p.s. I'm currently using Proof-General.
This archive was generated by a fusion of
Pipermail (Mailman edition) and