On 03/12/2019 17:34, Manuel Eberl wrote: > > Run out of store - interrupting threads > *** Interrupt > > But if anything, it seems to have made it worse: It seems that > HOL-Analysis now fails almost every time. On my personal machine, > HOL-Analysis never fails to build.
It is also fine on my usual test machines, using --minheap 1500 and unbounded maxheap (thus 16G). > [1]: https://ci.isabelle.systems/jenkins/job/isabelle-all/1553/consoleFull > [2]: https://ci.isabelle.systems/jenkins/job/isabelle-all/1571/consoleFull Here I see --minheap 4G (a bit too much), --maxheap 8G (a bit too little), threads=4 (rather low) and -j10 (rather high). The many parallel processes can easily have a bad influence the special ones with singular resource requirements. I often use a machine for testing elsewhere that is a slightly faster than lxcisa at TUM, and both hardware nodes are available. On this machine the standard quasi-interactive build is rather fast and stable: Isabelle/d411d5c84a4b ML_PLATFORM="x86_64_32-linux" ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8.1-20191124/x86_64_32-linux" ML_SYSTEM="polyml-5.8.1" ML_OPTIONS="--minheap 1500" isabelle build -N -j8 -o threads=8 -a Selective timings: Finished HOL (0:03:05 elapsed time, 0:10:04 cpu time, factor 3.27) Finished HOL-Analysis (0:05:57 elapsed time, 0:31:01 cpu time, factor 5.20) Finished HOL-Complex_Analysis (0:00:30 elapsed time, 0:02:56 cpu time, factor 5.86) Total timing: 0:13:03 elapsed time, 5:14:57 cpu time, factor 24.13 Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
