On 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" > > It requires the usual "isabelle components -a" incantation afterwards.
Here are some performance measurements on the best hardware that I have presently access to (not at TUM): Intel Xeon Gold 6148 CPU @ 2.40GHz 20 CPU cores * 2 hyperthreads * 2 nodes 64 GB memory SSD Isabelle/2633e166136a + AFP/ba82c831e5c2 isabelle build -N -j2 -o threads=8 x86-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL-Analysis (0:03:49 elapsed time, 0:21:11 cpu time, factor 5.55) Finished HOL-Analysis (0:03:50 elapsed time, 0:21:19 cpu time, factor 5.55) Finished HOL-Data_Structures (0:01:39 elapsed time, 0:11:30 cpu time, factor 6.91) Finished HOL-Data_Structures (0:01:43 elapsed time, 0:11:52 cpu time, factor 6.87) Finished HOL-Nominal (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.34) Finished HOL-Nominal (0:00:29 elapsed time, 0:01:08 cpu time, factor 2.33) Finished HOL-Nominal-Examples (0:02:57 elapsed time, 0:14:11 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:03:09 elapsed time, 0:14:55 cpu time, factor 4.73) Finished HOL-Proofs (0:09:52 elapsed time, 0:23:45 cpu time, factor 2.41) Finished HOL-Proofs (0:09:52 elapsed time, 0:24:04 cpu time, factor 2.44) x86_64_32-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.49) Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.48) Finished HOL-Analysis (0:03:41 elapsed time, 0:20:56 cpu time, factor 5.67) Finished HOL-Analysis (0:03:39 elapsed time, 0:20:50 cpu time, factor 5.70) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:33 cpu time, factor 7.16) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:35 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:24 cpu time, factor 2.07) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.06) Finished HOL-Nominal-Examples (0:02:53 elapsed time, 0:13:54 cpu time, factor 4.82) Finished HOL-Nominal-Examples (0:02:51 elapsed time, 0:13:51 cpu time, factor 4.83) Finished HOL-Proofs (0:09:55 elapsed time, 0:23:48 cpu time, factor 2.40) Finished HOL-Proofs (0:09:48 elapsed time, 0:23:35 cpu time, factor 2.40) x86_64_32-linux --minheap 3000 --maxheap 7000 Finished HOL (0:02:32 elapsed time, 0:08:53 cpu time, factor 3.50) Finished HOL (0:02:32 elapsed time, 0:08:51 cpu time, factor 3.49) Finished HOL-Analysis (0:03:26 elapsed time, 0:20:06 cpu time, factor 5.84) Finished HOL-Analysis (0:03:45 elapsed time, 0:21:20 cpu time, factor 5.67) Finished HOL-Data_Structures (0:01:35 elapsed time, 0:11:32 cpu time, factor 7.26) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:36 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.08) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.10) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.88) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.87) Finished HOL-Proofs (0:08:10 elapsed time, 0:19:17 cpu time, factor 2.36) Finished HOL-Proofs (0:08:23 elapsed time, 0:19:13 cpu time, factor 2.29) x86_64-linux --minheap 1500 --maxheap 7000 Finished HOL (0:02:48 elapsed time, 0:09:46 cpu time, factor 3.48) Finished HOL (0:02:46 elapsed time, 0:09:34 cpu time, factor 3.45) Finished HOL-Analysis (0:04:01 elapsed time, 0:22:39 cpu time, factor 5.64) Finished HOL-Analysis (0:04:00 elapsed time, 0:22:27 cpu time, factor 5.60) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:49 cpu time, factor 6.47) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:42 cpu time, factor 6.46) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.05) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04) Finished HOL-Nominal-Examples (0:03:03 elapsed time, 0:14:39 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:02:58 elapsed time, 0:14:29 cpu time, factor 4.88) Finished HOL-Proofs (0:10:16 elapsed time, 0:25:24 cpu time, factor 2.47) Finished HOL-Proofs (0:10:21 elapsed time, 0:25:35 cpu time, factor 2.47) x86_64-linux --minheap 3000 --maxheap 14000 Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.46) Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.47) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:40 cpu time, factor 5.51) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:54 cpu time, factor 5.57) Finished HOL-Data_Structures (0:01:44 elapsed time, 0:12:28 cpu time, factor 7.14) Finished HOL-Data_Structures (0:01:43 elapsed time, 0:12:21 cpu time, factor 7.14) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.03) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04) Finished HOL-Nominal-Examples (0:02:56 elapsed time, 0:14:18 cpu time, factor 4.87) Finished HOL-Nominal-Examples (0:02:56 elapsed time, 0:14:21 cpu time, factor 4.88) Finished HOL-Proofs (0:08:48 elapsed time, 0:20:31 cpu time, factor 2.33) Finished HOL-Proofs (0:08:55 elapsed time, 0:20:43 cpu time, factor 2.32) Interpretation of the data: * There is no penalty for x86_64_32 with its unusual heap indexing model, instead of native addressing of x86. * x86_64_32 is slightly faster than x86 for the same heap size, presumably due to the improved programming model of x86_64 and extra memory outside the heap (virtual address space is not limited to 4 GB). * x86_64_32 is significantly faster than x86 (or x86_64) for applications that require a lot of memory, such as HOL-Proofs above. The latter is further supported by AFP "slow" sessions, especially JinjaThreads: x86_64_32-linux --minheap 3000 --maxheap 7000 Finished AODV (0:50:24 elapsed time, 5:08:27 cpu time, factor 6.12) Finished AODV (0:48:47 elapsed time, 5:03:17 cpu time, factor 6.22) Finished ConcurrentGC (0:33:45 elapsed time, 3:19:18 cpu time, factor 5.90) Finished ConcurrentGC (0:35:55 elapsed time, 3:23:29 cpu time, factor 5.67) Finished JinjaThreads (0:28:23 elapsed time, 2:35:52 cpu time, factor 5.49) Finished JinjaThreads (0:34:08 elapsed time, 3:08:09 cpu time, factor 5.51) x86_64_32-linux --minheap 3000 --maxheap 14000 Finished AODV (0:49:12 elapsed time, 5:05:57 cpu time, factor 6.22) Finished AODV (0:49:23 elapsed time, 5:07:28 cpu time, factor 6.23) Finished ConcurrentGC (0:36:08 elapsed time, 3:24:55 cpu time, factor 5.67) Finished ConcurrentGC (0:34:21 elapsed time, 3:19:38 cpu time, factor 5.81) Finished JinjaThreads (0:16:30 elapsed time, 1:38:22 cpu time, factor 5.96) Finished JinjaThreads (0:16:31 elapsed time, 1:40:33 cpu time, factor 6.08) x86_64-linux --minheap 3000 --maxheap 7000 Finished AODV (0:56:08 elapsed time, 5:28:05 cpu time, factor 5.84) Finished AODV (0:58:24 elapsed time, 5:36:58 cpu time, factor 5.77) Finished ConcurrentGC (0:43:40 elapsed time, 3:52:08 cpu time, factor 5.32) Finished ConcurrentGC (0:42:53 elapsed time, 3:50:21 cpu time, factor 5.37) Finished JinjaThreads (1:05:27 elapsed time, 5:37:53 cpu time, factor 5.16) Finished JinjaThreads (1:16:26 elapsed time, 6:34:49 cpu time, factor 5.16) x86_64-linux --minheap 3000 --maxheap 14000 Finished AODV (0:58:41 elapsed time, 5:27:48 cpu time, factor 5.59) Finished AODV (0:55:00 elapsed time, 5:31:09 cpu time, factor 6.02) Finished ConcurrentGC (0:40:42 elapsed time, 3:46:33 cpu time, factor 5.57) Finished ConcurrentGC (0:41:58 elapsed time, 3:47:12 cpu time, factor 5.41) Finished JinjaThreads (0:24:16 elapsed time, 2:11:52 cpu time, factor 5.43) Finished JinjaThreads (0:28:04 elapsed time, 2:30:09 cpu time, factor 5.35) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev