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/Iptables_Semantics_Examples_Big_heap_chart.png 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 _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
