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



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
 release,
 but not at RC5 in the last moment before the lift-off.


      Makarius

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:

lemma A
  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.


	Makarius


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