[isabelle-dev] Status of AFP/JinjaThreads

[Lukas Bulwahn]

I fixed the proof in JinjaThreads with changeset 78eb9266adb0.

However, due to the deeper reason that the classical reasoner setup has 
been changed so that the original proof failed, one might have to look 
into this specific subgoal again (understanding how the classical 
reasoner has been changed).
(I am guessing it is due to the Predicate/Relation intro/elim changes.)

Lukas


On 03/19/2012 01:53 PM, Makarius wrote:
> Dear all,
>
> as of Isabelle/1d8601c642cc and AFP/039e21d114f1 the situation with 
> JinjaThreads is better than it used to be, but it still fails.  The 
> critical bit is here:
>
> *** Failed to finish proof
> *** At command "by" (line 1123 of 
> "thys/JinjaThreads/Execute/Scheduler.thy")
>
> It looks like a casualty of recent changes with 'a set, lattice, 
> inductive_set, numerals or similar.
>
> This part of the session can be checked easily with only 2 cores and a 
> few GB of memory.  So maybe someone who feels responsible for recent 
> changes in main HOL could take a look at it.
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>