On 08/11/17 15:23, Lars Hupel wrote:
since Isabelle/8905114fd23b, I'm seeing intermittent problems in the session "Iptables_Semantics_Examples_Big":
The relevant environment settings are:
ML_PLATFORM="x86_64-linux" ML_OPTIONS="-H 4000 --maxheap 10G"
I've been using --minheap 3000 --maxheap 30000 for that recently and it performs quite well (after months of not working at all).
The subsequent chart confirms the use of substantial heap space: http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/Iptabl...
Here are the overall results:
timing: 1:47:37 elapsed time, 8:17:10 cpu time, factor 4.62 ML timing: 1:47:33 elapsed time, 10:16:19 cpu time, factor 5.73 maximum heap: 29997 M average heap: 25795 M Isabelle version: e6a695d6a6b2 AFP version: fee069c9805b
Makarius