[isabelle] goals_limit in error-output



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?


--
  Peter

p.s. I'm currently using Proof-General.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.