makarius at sketis.net
Tue Jan 17 13:42:35 CET 2012
On Fri, 13 Jan 2012, Makarius wrote:
> But there is another problem with JinjaThreads right now:
> 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
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.
More information about the isabelle-dev