[isabelle-dev] Status of AFP/JinjaThreads
makarius at sketis.net
Mon Mar 19 13:53:23 CET 2012
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.
More information about the isabelle-dev