[isabelle-dev] Status of AFP/JinjaThreads

[Makarius]

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