Bertram Felgenhauer wrote: > Makarius wrote: > > So this is the right time for further testing of applications: > > Isabelle2018 should work as well, but I have not done any testing beyond > > "isabelle build -g main" -- Isabelle development only moves forward in > > one direction on a single branch. > > I have tried this with Isabelle2018 and IsaFoR; I've encountered no > problems and there's a nice speedup (estimated 1.25 times faster). > Heap images are 40% smaller, which is a welcome change as well.
I have gathered some more data (below). There are some curiosities: - Code export (that's the only thing that the 'Code' session does, besides theory merges) seems to be slower with polyml-a444f281ccec compared to polyml 5.7.1, even when sticking to the x86_64 platform. - A similar slowdown seems to affect the IsaFoR_3 session, but I don't know what's special about that one. - While most heap images are about 40% smaller with x86_64_32, this is not always the case; some heap images ended up being even larger in this experiment. Could there be a problem with the sharing pass on x86_64_32? Cheers, Bertram Hardware: i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD Software: GNU/Linux Isabelle2018 afp-2018 @ 400c722462b3 IsaFoR @ acb9096ce08a Common build flags: ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" Configurations: polyml 5.7.1 x86_64 ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6" polyml-a444f281ccec x86_64 ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6" polyml-0a6ebca445fc x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" polyml-a444f281ccec x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" Timings: Finished Pure (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.20) Finished Pure (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.18) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.13) Finished HOL (0:02:46 elapsed time, 0:10:50 cpu time, factor 3.91) Finished HOL (0:02:41 elapsed time, 0:10:05 cpu time, factor 3.75) Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84) Finished HOL (0:02:28 elapsed time, 0:09:20 cpu time, factor 3.78) Finished HOL-Lib (0:05:00 elapsed time, 0:35:54 cpu time, factor 7.18) Finished HOL-Lib (0:05:19 elapsed time, 0:36:41 cpu time, factor 6.88) Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88) Finished HOL-Lib (0:04:57 elapsed time, 0:34:16 cpu time, factor 6.91) Finished HOL-AFP (0:05:59 elapsed time, 0:37:39 cpu time, factor 6.28) Finished HOL-AFP (0:06:15 elapsed time, 0:38:31 cpu time, factor 6.15) Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28) Finished HOL-AFP (0:05:33 elapsed time, 0:35:01 cpu time, factor 6.30) Finished IsaFoR_1 (0:05:46 elapsed time, 0:31:43 cpu time, factor 5.49) Finished IsaFoR_1 (0:05:42 elapsed time, 0:31:06 cpu time, factor 5.46) Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59) Finished IsaFoR_1 (0:05:17 elapsed time, 0:29:15 cpu time, factor 5.54) Finished IsaFoR_2 (0:06:07 elapsed time, 0:29:37 cpu time, factor 4.84) Finished IsaFoR_2 (0:06:04 elapsed time, 0:29:15 cpu time, factor 4.82) Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87) Finished IsaFoR_2 (0:05:59 elapsed time, 0:28:14 cpu time, factor 4.72) Finished IsaFoR_3 (0:07:30 elapsed time, 0:47:56 cpu time, factor 6.38) Finished IsaFoR_3 (0:09:58 elapsed time, 0:55:27 cpu time, factor 5.56) ? Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45) Finished IsaFoR_3 (0:06:49 elapsed time, 0:43:20 cpu time, factor 6.35) Finished IsaFoR_4 (0:09:40 elapsed time, 0:30:25 cpu time, factor 3.15) Finished IsaFoR_4 (0:09:14 elapsed time, 0:29:16 cpu time, factor 3.17) Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17) Finished IsaFoR_4 (0:08:52 elapsed time, 0:27:57 cpu time, factor 3.15) Finished Code (0:05:30 elapsed time, 0:05:42 cpu time, factor 1.03) Finished Code (0:08:34 elapsed time, 0:08:46 cpu time, factor 1.02) ? Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02) Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02) total 00:48:29 total 00:54:02 total 00:48:08 total 00:48:08 Heap image sizes (factor): 28081037 Pure (1.00) 25131549 Pure (0.89) 19271077 Pure (0.68) 19270685 Pure (0.68) 410972244 HOL (1.00) 403934084 HOL (0.98) 249583659 HOL (0.61) 249808871 HOL (0.61) 525949867 HOL-Lib (1.00) 526132427 HOL-Lib (1.00) 308088218 HOL-Lib (0.59) 307456194 HOL-Lib (0.58) 913422879 HOL-AFP (1.00) 915450415 HOL-AFP (1.00) 537947934 HOL-AFP (0.59) 538445922 HOL-AFP (0.59) 724672759 IsaFoR_1 (1.00) 724822231 IsaFoR_1 (1.00) 428960922 IsaFoR_1 (0.59) 429004970 IsaFoR_1 (0.59) 623083120 IsaFoR_2 (1.00) 623291272 IsaFoR_2 (1.00) 367497971 IsaFoR_2 (0.59) 884213127 IsaFoR_2 (1.42) ? 712211696 IsaFoR_3 (1.00) 713133672 IsaFoR_3 (1.00) 419978203 IsaFoR_3 (0.59) 521702015 IsaFoR_3 (0.73) 480209352 IsaFoR_4 (1.00) 481036688 IsaFoR_4 (1.00) 730273567 IsaFoR_4 (1.52) ? 745333063 IsaFoR_4 (1.55) ? _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev