Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations

2012-10-19 Thread Makarius
On Thu, 18 Oct 2012, Andreas Lochbihler wrote: Does anybody remember a use of the 'apply_end' command? Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they could be fused into the qed. However, I regularly use apply_end when I develop the method call for qed to finish

Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

2012-10-19 Thread Makarius
On Fri, 19 Oct 2012, Lukas Bulwahn wrote: Operations like Simplifier.context, Simplifier.inherit_context should help here. Once that is repaired, I will see if the warning can now be made an error that is more explicit about the reasons. I am certainly in favour of this. First, tool develope

Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

2012-10-19 Thread Lukas Bulwahn
On 10/19/2012 02:22 PM, Makarius wrote: On Wed, 17 Oct 2012, Lukas Bulwahn wrote: If you update to changeset 89b118c0c070, the issue should be resolved. There still seem to be remaining issues: Isabelle/d1ecb3554b25 and AFP/15527cc14202: Girth_Chromatic FAILED (see also /Volumes/Macintosh

[isabelle-dev] isatest stability

2012-10-19 Thread Makarius
We've seen routine isatest dropouts in the past few weeks. With Isabelle/d1ecb3554b25 there is some hope that it will work better again. There have been some actual issues with exceptions, interrupts and parallel evaluation on the Isabelle side. I still have the ambitition to return to routin

Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

2012-10-19 Thread Makarius
On Wed, 17 Oct 2012, Lukas Bulwahn wrote: If you update to changeset 89b118c0c070, the issue should be resolved. There still seem to be remaining issues: Isabelle/d1ecb3554b25 and AFP/15527cc14202: Girth_Chromatic FAILED (see also /Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml