Email Gateway (Sep 28 2020 at 15:08): Email Gateway (Sep 28 2020 at 15:08):From: Lawrence Paulson <lp15@cam.ac.uk>
I have recently taken delivery of a 16 inch MacBook Pro, 2.4 GHz 8-core i9 processor and 32 GB of memory. It’s a very expensive machine, but its equally expensive predecessors had serious problems with the keyboard and overheating. I’m happy to report that this model appears to be pretty good as an Isabelle machine. In particular it does not seem to suffer thermal problems; one can do a lot without the fan even kicking in.
I attach some benchmarks run using Isabelle 2020. I see that it's inferior to the 27 inch iMac (see my post dated 29 July 2019) but still impressive.
Larry
Isabelle2020.app/Isabelle: ./bin/isabelle build -g timing
Running HOL-Cardinals ...
Finished HOL-Cardinals (0:00:04 elapsed time, 0:00:26 cpu time, factor 6.27)
Running HOL-Data_Structures ...
Finished HOL-Data_Structures (0:01:53 elapsed time, 0:15:01 cpu time, factor 7.94)
Running HOL-Hoare_Parallel ...
Finished HOL-Hoare_Parallel (0:00:36 elapsed time, 0:04:14 cpu time, factor 6.92)
Running HOL-Homology ...
Finished HOL-Homology (0:06:36 elapsed time, 0:07:46 cpu time, factor 1.18)
Building HOL-Auth ...
Finished HOL-Auth (0:00:49 elapsed time, 0:04:09 cpu time, factor 5.02)
Running HOL-Bali ...
Finished HOL-Bali (0:00:37 elapsed time, 0:02:24 cpu time, factor 3.90)
Building HOL-Algebra ...
Finished HOL-Algebra (0:01:51 elapsed time, 0:07:54 cpu time, factor 4.25)
Running HOL-Corec_Examples ...
Finished HOL-Corec_Examples (0:01:47 elapsed time, 0:05:50 cpu time, factor 3.26)
Running HOL-Datatype_Examples ...
Finished HOL-Datatype_Examples (0:00:54 elapsed time, 0:04:09 cpu time, factor 4.57)
Running HOL-Decision_Procs ...
Finished HOL-Decision_Procs (0:07:34 elapsed time, 0:13:41 cpu time, factor 1.81)
Running HOL-IMP ...
Finished HOL-IMP (0:00:35 elapsed time, 0:03:40 cpu time, factor 6.18)
Running HOL-Imperative_HOL ...
Finished HOL-Imperative_HOL (0:00:39 elapsed time, 0:06:28 cpu time, factor 9.89)
Running HOL-Metis_Examples ...
Finished HOL-Metis_Examples (0:00:10 elapsed time, 0:01:08 cpu time, factor 6.36)
Running HOL-MicroJava ...
Finished HOL-MicroJava (0:00:39 elapsed time, 0:03:09 cpu time, factor 4.82)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:13 elapsed time, 0:00:26 cpu time, factor 1.98)
Running HOL-Nominal-Examples ...
Finished HOL-Nominal-Examples (0:02:43 elapsed time, 0:14:01 cpu time, factor 5.14)
Building HOL-Nonstandard_Analysis ...
Finished HOL-Nonstandard_Analysis (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.73)
Running HOL-Nonstandard_Analysis-Examples ...
Finished HOL-Nonstandard_Analysis-Examples (0:00:02 elapsed time, 0:00:03 cpu time)
Building HOL-Number_Theory ...
Finished HOL-Number_Theory (0:00:48 elapsed time, 0:03:26 cpu time, factor 4.24)
Running HOL-Predicate_Compile_Examples ...
Skipping theories "Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example_Prolog", "Lambda_Example", "List_Examples" (undefined ISABELLE_SWIPL)
Skipping theories "Reg_Exp_Example" (undefined ISABELLE_SWIPL)
Finished HOL-Predicate_Compile_Examples (0:00:37 elapsed time, 0:05:22 cpu time, factor 8.49)
Building HOL-Probability ...
Finished HOL-Probability (0:00:57 elapsed time, 0:05:12 cpu time, factor 5.40)
Running HOL-Probability-ex ...
Finished HOL-Probability-ex (0:00:06 elapsed time, 0:00:19 cpu time, factor 3.29)
Building HOL-Proofs ...
Finished HOL-Proofs (0:04:43 elapsed time, 0:09:53 cpu time, factor 2.09)
Running HOL-Proofs-Extraction ...
Finished HOL-Proofs-Extraction (0:01:16 elapsed time, 0:02:11 cpu time, factor 1.71)
Running HOL-Proofs-Lambda ...
Finished HOL-Proofs-Lambda (0:01:15 elapsed time, 0:01:27 cpu time, factor 1.16)
Running HOL-Quickcheck_Examples ...
Skipping theories "Hotel_Example", "Quickcheck_Narrowing_Examples" (undefined ISABELLE_GHC)
Finished HOL-Quickcheck_Examples (0:00:15 elapsed time, 0:01:47 cpu time, factor 6.80)
Running HOL-Quotient_Examples ...
Finished HOL-Quotient_Examples (0:00:21 elapsed time, 0:01:29 cpu time, factor 4.17)
Running HOL-SET_Protocol ...
Finished HOL-SET_Protocol (0:00:14 elapsed time, 0:01:15 cpu time, factor 5.32)
Running HOL-UNITY ...
Finished HOL-UNITY (0:00:13 elapsed time, 0:01:19 cpu time, factor 5.92)
Building HOL-Word ...
Finished HOL-Word (0:00:14 elapsed time, 0:00:49 cpu time, factor 3.47)
Running HOL-Word-SMT_Examples ...
Finished HOL-Word-SMT_Examples (0:00:41 elapsed time, 0:01:11 cpu time, factor 1.71)
Running HOL-ex ...
Finished HOL-ex (0:02:52 elapsed time, 0:15:07 cpu time, factor 5.26)
Building HOLCF ...
Finished HOLCF (0:00:15 elapsed time, 0:00:38 cpu time, factor 2.58)
Running IOA ...
Finished IOA (0:00:05 elapsed time, 0:00:18 cpu time, factor 3.71)
Building ZF-Induct ...
Finished ZF-Induct (0:00:02 elapsed time, 0:00:08 cpu time)
Running ZF-UNITY ...
Finished ZF-UNITY (0:00:02 elapsed time, 0:00:17 cpu time)
0:43:31 elapsed time, 2:27:35 cpu time, factor 3.39
Email Gateway (Sep 29 2020 at 18:44):From: Lawrence Paulson <lp15@cam.ac.uk>
People noticed that the previous run was incomplete, so here we go again. For some reason, these runtimes beat the previous ones. Though my (inaccessible during lockdown) iMac is still faster.
To repeat: 16 inch MacBook Pro, 2.4 GHz 8-core i9 processor and 32 GB of memory.
Larry
Isabelle/bin: ./isabelle build -g timing -f | tee aless
Building Pure ...
Finished Pure (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.99)
Building HOL ...
Finished HOL (0:03:07 elapsed time, 0:11:30 cpu time, factor 3.68)
Building HOL-Analysis ...
Finished HOL-Analysis (0:03:58 elapsed time, 0:23:31 cpu time, factor 5.91)
Building HOL-Library ...
Finished HOL-Library (0:01:25 elapsed time, 0:08:22 cpu time, factor 5.85)
Building HOL-Computational_Algebra ...
Finished HOL-Computational_Algebra (0:00:50 elapsed time, 0:02:40 cpu time, factor 3.18)
Building HOL-Algebra ...
Finished HOL-Algebra (0:01:43 elapsed time, 0:07:31 cpu time, factor 4.37)
Running HOL-Decision_Procs ...
Finished HOL-Decision_Procs (0:04:16 elapsed time, 0:13:58 cpu time, factor 3.27)
Running HOL-Homology ...
Finished HOL-Homology (0:01:06 elapsed time, 0:05:45 cpu time, factor 5.18)
Building HOL-Proofs ...
Finished HOL-Proofs (0:07:13 elapsed time, 0:10:12 cpu time, factor 1.41)
Building HOL-Number_Theory ...
Finished HOL-Number_Theory (0:00:49 elapsed time, 0:03:30 cpu time, factor 4.25)
Running HOL-ex ...
Finished HOL-ex (0:05:08 elapsed time, 0:16:24 cpu time, factor 3.19)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.01)
Running HOL-Nominal-Examples ...
Finished HOL-Nominal-Examples (0:02:27 elapsed time, 0:12:44 cpu time, factor 5.20)
Running HOL-Data_Structures ...
Finished HOL-Data_Structures (0:01:50 elapsed time, 0:14:53 cpu time, factor 8.06)
Running HOL-Corec_Examples ...
Finished HOL-Corec_Examples (0:01:40 elapsed time, 0:05:19 cpu time, factor 3.18)
Running HOL-Proofs-Extraction ...
Finished HOL-Proofs-Extraction (0:01:12 elapsed time, 0:02:04 cpu time, factor 1.73)
Running HOL-Proofs-Lambda ...
Finished HOL-Proofs-Lambda (0:01:07 elapsed time, 0:01:18 cpu time, factor 1.17)
Running HOL-Datatype_Examples ...
Finished HOL-Datatype_Examples (0:00:53 elapsed time, 0:04:06 cpu time, factor 4.58)
Building HOL-Auth ...
Finished HOL-Auth (0:00:47 elapsed time, 0:03:52 cpu time, factor 4.91)
Building HOL-Word ...
Finished HOL-Word (0:00:13 elapsed time, 0:00:46 cpu time, factor 3.54)
Running HOL-Complex_Analysis ...
Finished HOL-Complex_Analysis (0:00:19 elapsed time, 0:02:03 cpu time, factor 6.33)
Building HOL-Probability ...
Finished HOL-Probability (0:00:55 elapsed time, 0:05:06 cpu time, factor 5.56)
Running HOL-Word-SMT_Examples ...
Finished HOL-Word-SMT_Examples (0:00:38 elapsed time, 0:01:05 cpu time, factor 1.71)
Running HOL-Imperative_HOL ...
Finished HOL-Imperative_HOL (0:00:36 elapsed time, 0:06:09 cpu time, factor 9.99)
Running HOL-MicroJava ...
Finished HOL-MicroJava (0:00:38 elapsed time, 0:03:10 cpu time, factor 4.90)
Running HOL-Predicate_Compile_Examples ...
Skipping theories "Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example_Prolog", "Lambda_Example", "List_Examples" (undefined ISABELLE_SWIPL)
Skipping theories "Reg_Exp_Example" (undefined ISABELLE_SWIPL)
Finished HOL-Predicate_Compile_Examples (0:00:37 elapsed time, 0:05:20 cpu time, factor 8.51)
Running HOL-Hoare_Parallel ...
Finished HOL-Hoare_Parallel (0:00:36 elapsed time, 0:04:12 cpu time, factor 6.94)
Running HOL-Bali ...
Finished HOL-Bali (0:00:34 elapsed time, 0:02:21 cpu time, factor 4.13)
Running HOL-IMP ...
Finished HOL-IMP (0:00:33 elapsed time, 0:03:26 cpu time, factor 6.19)
Running HOL-Quotient_Examples ...
Finished HOL-Quotient_Examples (0:00:19 elapsed time, 0:01:19 cpu time, factor 4.06)
Building ZF ...
Finished ZF (0:00:08 elapsed time, 0:00:30 cpu time, factor 3.48)
Running HOL-Quickcheck_Examples ...
Skipping theories "Hotel_Example", "Quickcheck_Narrowing_Examples" (undefined ISABELLE_GHC)
Finished HOL-Quickcheck_Examples (0:00:14 elapsed time, 0:01:39 cpu time, factor 6.79)
Running HOL-SET_Protocol ...
Finished HOL-SET_Protocol (0:00:12 elapsed time, 0:01:08 cpu time, factor 5.30)
Building HOLCF ...
Finished HOLCF (0:00:15 elapsed time, 0:00:38 cpu time, factor 2.55)
Running HOL-UNITY ...
Finished HOL-UNITY (0:00:12 elapsed time, 0:01:17 cpu time, factor 6.02)
Running HOL-Metis_Examples ...
Finished HOL-Metis_Examples (0:00:10 elapsed time, 0:01:07 cpu time, factor 6.19)
Building HOL-Nonstandard_Analysis ...
Finished HOL-Nonstandard_Analysis (0:00:13 elapsed time, 0:00:38 cpu time, factor 2.75)
Running HOL-Probability-ex ...
Finished HOL-Probability-ex (0:00:05 elapsed time, 0:00:18 cpu time, factor 3.18)
Running IOA ...
Finished IOA (0:00:04 elapsed time, 0:00:17 cpu time, factor 3.67)
Building ZF-Induct ...
Finished ZF-Induct (0:00:02 elapsed time, 0:00:07 cpu time)
Running HOL-Cardinals ...
Finished HOL-Cardinals (0:00:04 elapsed time, 0:00:26 cpu time, factor 6.21)
Running ZF-UNITY ...
Finished ZF-UNITY (0:00:02 elapsed time, 0:00:17 cpu time)
Running HOL-Nonstandard_Analysis-Examples ...
Finished HOL-Nonstandard_Analysis-Examples (0:00:02 elapsed time, 0:00:03 cpu time)
0:48:31 elapsed time, 3:11:58 cpu time, factor 3.96
Last updated: Jul 15 2022 at 23:21 UTC