Re: [isabelle] RC5: Ordering of normal output and error output

On 20/06/2015 23:36, Makarius wrote:
On Sat, 20 Jun 2015, Tobias Nipkow wrote:

On 25/05/2015 11:56, Makarius wrote:
 On Mon, 25 May 2015, Peter Lammich wrote:

>  I have worked for two days with RC5 now, and found it the most annoying
>  difference compared to Isabelle-2014

 More than 5 weeks ago at RC1 this could have been reconsidered for this
 but not at RC5 in the last moment before the lift-off.


We are now past the release but this unpleasant behaviour is still with us.
Please do not fortget about it.

The next release will probably happen next year, so there is plenty of time to
figure out if there is anything to be done here at all.  So far this thread
merely proved a lack of serious testing of release candidates.

The thread proves that there are at least three users who do not like the new behaviour and that you prefer to blame others.

As usual, I need a proper description of what is perceived as "unpleasant",
"broken", "bug" etc. The initial message on this thread was about message order
wrt. different kinds (state vs. non-state, especially warning, errors etc.).

Peter's first email was clear on this, and your replies showed that you understood what he meant. To jog your memory, try this:

lemma A
apply(rule refl)

This is e.g. illustrated in the following example:

lemma A
   apply (tactic ‹fn st => (warning "foo"; all_tac st)›)

No, it is not. You are suddenly dragging in warnings, but this thread is not about them.


Here the ordering is the same in Isabelle2014 and Isabelle2015.

There were other changes in Isabelle2015, to address earlier complaints from
users.  Maybe that had an adverse effect elsewhere.  Or maybe it is just a
matter to get used to certain new behaviour.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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