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
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
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
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
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