Re: [isabelle] Message output in Isabelle2014 and Isabelle2015



On Tue, 23 Jun 2015, Dmitriy Traytel wrote:

But this would also mean that one does not see the intermediate goal state if something goes wrong in the terminal method slot of by.

lemma "P (xs :: 'a list)"
  by (induct xs) auto

This is more useful when repairing existing proofs, rather than writing new proofs, though.

Dmitriy

On 23.06.2015 15:14, Larry Paulson wrote:
 Yes â this might be OK.
 Larry

>  On 23 Jun 2015, at 13:42, Peter Lammich <lammich at in.tum.de> wrote:
> > One solution that does not involve too much implementation effort might
>  be to not include the goal-state into the error message, and output this
>  shorter error message *before* the goal-state.
> > While the user is typing, he would see a short error message that he
>  could ignore, followed by the goal state.
>  When the user is inspecting the (error-)result of the command, he would
>  see the error message first. Warnings should still be printed after the
>  goal-state

The observation by Dmitriy is correct.

The current printing of goal state errors is the result of various reforms in the past few years. That relatively new behaviour is actually the reason why I usually do many things without ever looking at the Output window, often having it closed over a long stretch of time: the message under the red squiggles usually provides the relevant bits to see what is missing to finish a proof step.


As already explained on earlier instances of the thread, any built-in policies to reorder messages in output don't work. We've had that in Proof General, and it converged to a big mess over the decades. In 2007 that actually caused total existence failure between Proof General 3.x and 4.x. Then I introduced "isabelle tty" as temporary workaround; then "isabelle jedit" a bit later.

On a multi-window GUI there is no point to squeeze everything into a single linear output. The Query panel already provides a different way to view a proof state, independently on Output. Such things are relatively easy to make, and don't require artificial intelligence from the system to guess what the user wants to see.


	Makarius


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