Re: [isabelle] RC5: Ordering of normal output and error output
- To: Tobias Nipkow <nipkow at in.tum.de>
- Subject: Re: [isabelle] RC5: Ordering of normal output and error output
- From: Makarius <makarius at sketis.net>
- Date: Sat, 20 Jun 2015 23:36:12 +0200 (CEST)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <5585CBB6.email@example.com>
- References: <1432210096.24892.48.camel@lapnipkow10> <CAGbqCMyoFeJon19y7=PW9Po-CZ-WKyTha3yzGZdDXEqbYz52kA@mail.gmail.com> <alpine.LNX.firstname.lastname@example.org> <1432508339.21362.10.camel@lapnipkow10> <alpine.LNX.email@example.com> <5585CBB6.firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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.
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.). This is e.g. illustrated in the following example:
apply (tactic ‹fn st => (warning "foo"; all_tac st)›)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and