[isabelle] Message output in Isabelle2014 and Isabelle2015



(This is a relaunch of a thread that ended up containing mostly rubbish. Here is another attempt to shed some light on the factual situation.)


On Thu, 21 May 2015, Peter Lammich wrote:

The output window shows the normal output (e.g. the current subgoals)
before the error output, (e.g. tactic failed).

This is very inconvenient if the list of goals is longer, and you have
to scroll down every time to see the error message.

In Isabelle2014, it was fine, and it showed
 errors, then normal output, then warnings.

btw: I reported the same issue for some Isabelle2014-RCx, it got fixed
for 2014, and now we have it back again.

Can you explain precisely what you reported for Isabelle2014-RCx? What was the "issue" and what was the "fix".

As far as I can tell, the order of messages in the Output panel changed already before the Isabelle2014 release, to have proof state output first, and everything else after it. The relevant changeset is:

changeset:   57691:9616643a3032
user:        wenzelm
date:        Sat Jul 26 14:52:54 2014 +0200
files:       src/Tools/jEdit/src/rendering.scala
description:
output state first -- avoid fluctuation wrt. warnings, errors, etc.;


Here is an example to see the order (duplication of messages needs to be ignored -- it is an artifact of the example not participating properly in method expression closure):

lemma A
  apply (tactic âfn st => (warning "foo"; Output.error_message "bar"; all_tac st)â)

The result is the same in Isabelle2014 and Isabelle2015.


There is a related mailing list thread from 11-Aug-2014 "RC-3 puts method error after subgoals and warnings in output": https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00115.html

That old thread contains some general explanations that I won't repeat here again. Moreover, there is the following interesting remark:

On Thu, 14 Aug 2014, Peter Lammich wrote:

For this mode of proof development, which is definitely not the only way
to develop a proof, but for my type of developments a very effective
one, it is essential to always see the current subgoals, also while
typing the next apply-command, without having to do some mousing or
other interaction. As there is no dedicated subgoals-panel in PIDE (as
there was in PG), I have to resort to the output panel.

As pointed out in previous mails, this is not an ideal replacement for a
subgoals-panel, but I currently try to live with its features:
Currently, the most annoying one is that the current subgoal vanishes in
favour of a "syntax error"-message while you are typing the next
apply-command.

The latter aspect has actually changed here:

changeset:   59331:4139db32821e
user:        wenzelm
date:        Fri Jan 09 20:39:17 2015 +0100
files:       src/Pure/PIDE/command.ML
description:
non-strict print_state: display old proof state on failure, e.g. unfinished command;

That is from 09-Jan-2015, and it is the new behaviour in Isabelle2015 on this thread that was not articulated so far. Try this example in Isabelle2014 vs. Isabelle2015 to see the difference:

lemma A
  apply fail

Of course, a method application error is also an error, so the old state is printed first and the error message second. Thus the error might get obscured by long proof states, which was the original starting point above.

The deeper problem is cluttering of Output with too many different things, and the lack of a dedicated panel just for proof state output. I was actually thinking about reformed proof state output 1-2 weeks ago, but got distracted again by the noise here on the mailing list.


	Makarius



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