[isabelle-dev] JinjaThreads

[Makarius]

On Fri, 13 Jan 2012, Makarius wrote:

> But there is another problem with JinjaThreads right now:
>
>  Isabelle/d43ddad41d81
>  AFP/3dcc6b9eae2b
>
>  thys/JinjaThreads/Framework/FWDeadlock.thy line 251:
>  blast does not terminate and fills up memory
>
> It looks like another set vs. pred thing stemming from coinductive_set 
> deadlocked further above.

Problem solved in Isabelle/fcfb4aa8e6e6 and AFP/8b9815ab5022 thanks to 
Stefan (AFP/753771d51961).


For the record, here are some timings on Mac Pro / 8 cores / 32 GB:

Finished HOL-Word-JinjaThreads-Basic (0:01:23 elapsed time, 0:03:16 cpu time, factor 2.36)
Finished HOL-Word-JinjaThreads-Basic-JinjaThreads (0:39:11 elapsed time, 1:37:05 cpu time, factor 2.47)

It probably takes approx. 24 GB to run.


 	Makarius