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

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: Jan 25 2022 at 02:35 UTC