[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:
date: Sat Jul 26 14:52:54 2014 +0200
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):
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":
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
The latter aspect has actually changed here:
date: Fri Jan 09 20:39:17 2015 +0100
non-strict print_state: display old proof state on failure, e.g.
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:
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and