[isabelle] Apple benchmarks



For the benefit of people who prefer Apple equipment, I thought I’d share some benchmarks for my new iMac. This is the 27 inch model upgraded with i9 processors and with 32 GB of memory.

Cheaper alternatives within the Apple world include the Mac Mini (the latest incarnation is remarkably powerful) and the 2013 Mac Pro, which I see selling on eBay for quite a reasonable price.

Larry Paulson


ML_PLATFORM="x86_64_32-darwin"
ML_HOME="/Users/lp15/Applications/Isabelle2019.app/Contents/Resources/Isabelle2019/contrib/polyml-5.8/x86_64_32-darwin"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="--minheap 500"

Building Pure ...
Timing Pure (1 threads, 0.562s elapsed time, 0.563s cpu time, 0.018s GC time, factor 1.00)
Finished Pure (0:00:11 elapsed time, 0:00:11 cpu time, factor 0.99)
Building HOL ...
Timing HOL (8 threads, 94.669s elapsed time, 330.843s cpu time, 36.647s GC time, factor 3.49)
Finished HOL (0:01:49 elapsed time, 0:06:04 cpu time, factor 3.33)
Building HOL-Analysis ...
Timing HOL-Analysis (8 threads, 154.116s elapsed time, 931.731s cpu time, 88.924s GC time, factor 6.05)
Finished HOL-Analysis (0:02:47 elapsed time, 0:16:00 cpu time, factor 5.74)
Running HOL-Cardinals ...
Timing HOL-Cardinals (8 threads, 2.741s elapsed time, 18.835s cpu time, 0.924s GC time, factor 6.87)
Finished HOL-Cardinals (0:00:03 elapsed time, 0:00:19 cpu time, factor 5.92)
Running HOL-Data_Structures ...
Timing HOL-Data_Structures (8 threads, 82.585s elapsed time, 572.507s cpu time, 55.072s GC time, factor 6.93)
Finished HOL-Data_Structures (0:01:23 elapsed time, 0:09:33 cpu time, factor 6.89)
Running HOL-Hoare_Parallel ...
Timing HOL-Hoare_Parallel (8 threads, 30.798s elapsed time, 183.599s cpu time, 11.555s GC time, factor 5.96)
Finished HOL-Hoare_Parallel (0:00:31 elapsed time, 0:03:04 cpu time, factor 5.88)
Running HOL-Homology ...
Timing HOL-Homology (8 threads, 37.390s elapsed time, 180.552s cpu time, 18.638s GC time, factor 4.83)
Finished HOL-Homology (0:00:38 elapsed time, 0:03:01 cpu time, factor 4.75)
Building HOL-Library ...
Timing HOL-Library (8 threads, 35.936s elapsed time, 242.852s cpu time, 19.700s GC time, factor 6.76)
Finished HOL-Library (0:00:51 elapsed time, 0:04:51 cpu time, factor 5.66)
Building HOL-Auth ...
Timing HOL-Auth (8 threads, 31.946s elapsed time, 178.931s cpu time, 18.443s GC time, factor 5.60)
Finished HOL-Auth (0:00:40 elapsed time, 0:03:15 cpu time, factor 4.85)
Running HOL-Bali ...
Timing HOL-Bali (8 threads, 30.826s elapsed time, 111.601s cpu time, 15.096s GC time, factor 3.62)
Finished HOL-Bali (0:00:31 elapsed time, 0:01:52 cpu time, factor 3.55)
Building HOL-Computational_Algebra ...
Timing HOL-Computational_Algebra (8 threads, 25.080s elapsed time, 82.997s cpu time, 8.169s GC time, factor 3.31)
Finished HOL-Computational_Algebra (0:00:32 elapsed time, 0:01:36 cpu time, factor 2.98)
Building HOL-Algebra ...
Timing HOL-Algebra (8 threads, 63.953s elapsed time, 297.468s cpu time, 67.898s GC time, factor 4.65)
Finished HOL-Algebra (0:01:20 elapsed time, 0:05:32 cpu time, factor 4.14)
Running HOL-Corec_Examples ...
Timing HOL-Corec_Examples (8 threads, 90.834s elapsed time, 277.995s cpu time, 44.336s GC time, factor 3.06)
Finished HOL-Corec_Examples (0:01:31 elapsed time, 0:04:38 cpu time, factor 3.04)
Running HOL-Datatype_Benchmark ...
Timing HOL-Datatype_Benchmark (8 threads, 218.009s elapsed time, 840.799s cpu time, 169.199s GC time, factor 3.86)
Finished HOL-Datatype_Benchmark (0:03:39 elapsed time, 0:14:01 cpu time, factor 3.84)
Running HOL-Datatype_Examples ...
Timing HOL-Datatype_Examples (8 threads, 43.216s elapsed time, 173.367s cpu time, 27.072s GC time, factor 4.01)
Finished HOL-Datatype_Examples (0:00:44 elapsed time, 0:02:54 cpu time, factor 3.95)
Running HOL-Decision_Procs ...
Timing HOL-Decision_Procs (8 threads, 130.446s elapsed time, 616.451s cpu time, 72.004s GC time, factor 4.73)
Finished HOL-Decision_Procs (0:02:11 elapsed time, 0:10:17 cpu time, factor 4.69)
Running HOL-IMP ...
Timing HOL-IMP (8 threads, 27.109s elapsed time, 165.618s cpu time, 16.766s GC time, factor 6.11)
Finished HOL-IMP (0:00:27 elapsed time, 0:02:47 cpu time, factor 6.01)
Running HOL-Imperative_HOL ...
Timing HOL-Imperative_HOL (8 threads, 28.878s elapsed time, 43.317s cpu time, 1.929s GC time, factor 1.50)
Finished HOL-Imperative_HOL (0:00:29 elapsed time, 0:04:50 cpu time, factor 9.80)
Running HOL-Metis_Examples ...
Timing HOL-Metis_Examples (8 threads, 8.537s elapsed time, 40.309s cpu time, 7.172s GC time, factor 4.72)
Finished HOL-Metis_Examples (0:00:09 elapsed time, 0:00:59 cpu time, factor 6.38)
Running HOL-MicroJava ...
Timing HOL-MicroJava (8 threads, 40.276s elapsed time, 173.190s cpu time, 14.398s GC time, factor 4.30)
Finished HOL-MicroJava (0:00:41 elapsed time, 0:02:53 cpu time, factor 4.23)
Building HOL-Nominal ...
Timing HOL-Nominal (8 threads, 3.081s elapsed time, 6.078s cpu time, 0.490s GC time, factor 1.97)
Finished HOL-Nominal (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.81)
Running HOL-Nominal-Examples ...
Timing HOL-Nominal-Examples (8 threads, 126.870s elapsed time, 605.265s cpu time, 58.311s GC time, factor 4.77)
Finished HOL-Nominal-Examples (0:02:07 elapsed time, 0:10:06 cpu time, factor 4.74)
Building HOL-Nonstandard_Analysis ...
Timing HOL-Nonstandard_Analysis (8 threads, 3.497s elapsed time, 12.555s cpu time, 0.768s GC time, factor 3.59)
Finished HOL-Nonstandard_Analysis (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.41)
Running HOL-Nonstandard_Analysis-Examples ...
Timing HOL-Nonstandard_Analysis-Examples (8 threads, 1.341s elapsed time, 1.977s cpu time, 0.090s GC time, factor 1.47)
Finished HOL-Nonstandard_Analysis-Examples (0:00:02 elapsed time)
Building HOL-Number_Theory ...
Timing HOL-Number_Theory (8 threads, 25.502s elapsed time, 117.884s cpu time, 13.334s GC time, factor 4.62)
Finished HOL-Number_Theory (0:00:35 elapsed time, 0:02:16 cpu time, factor 3.88)
Running HOL-Predicate_Compile_Examples ...
Timing HOL-Predicate_Compile_Examples (8 threads, 35.894s elapsed time, 147.668s cpu time, 12.228s GC time, factor 4.11)
Finished HOL-Predicate_Compile_Examples (0:00:36 elapsed time, 0:04:59 cpu time, factor 8.18)
Building HOL-Probability ...
Timing HOL-Probability (8 threads, 30.987s elapsed time, 175.874s cpu time, 20.525s GC time, factor 5.68)
Finished HOL-Probability (0:00:40 elapsed time, 0:03:43 cpu time, factor 5.51)
Running HOL-Probability-ex ...
Timing HOL-Probability-ex (8 threads, 3.463s elapsed time, 9.349s cpu time, 0.503s GC time, factor 2.70)
Finished HOL-Probability-ex (0:00:04 elapsed time, 0:00:10 cpu time, factor 2.35)
Building HOL-Proofs ...
Timing HOL-Proofs (8 threads, 335.059s elapsed time, 759.147s cpu time, 84.760s GC time, factor 2.27)
Finished HOL-Proofs (0:06:07 elapsed time, 0:14:00 cpu time, factor 2.28)
Running HOL-Proofs-Extraction ...
Timing HOL-Proofs-Extraction (8 threads, 48.709s elapsed time, 105.896s cpu time, 10.372s GC time, factor 2.17)
Finished HOL-Proofs-Extraction (0:00:49 elapsed time, 0:01:46 cpu time, factor 2.16)
Running HOL-Proofs-Lambda ...
Timing HOL-Proofs-Lambda (8 threads, 63.598s elapsed time, 78.846s cpu time, 3.712s GC time, factor 1.24)
Finished HOL-Proofs-Lambda (0:01:04 elapsed time, 0:01:19 cpu time, factor 1.24)
Running HOL-Quickcheck_Benchmark ...
Timing HOL-Quickcheck_Benchmark (8 threads, 195.380s elapsed time, 928.200s cpu time, 84.607s GC time, factor 4.75)
Finished HOL-Quickcheck_Benchmark (0:03:16 elapsed time, 0:15:28 cpu time, factor 4.74)
Running HOL-Quickcheck_Examples ...
Timing HOL-Quickcheck_Examples (8 threads, 12.658s elapsed time, 88.491s cpu time, 9.543s GC time, factor 6.99)
Finished HOL-Quickcheck_Examples (0:00:13 elapsed time, 0:01:29 cpu time, factor 6.63)
Running HOL-Quotient_Examples ...
Timing HOL-Quotient_Examples (8 threads, 14.723s elapsed time, 21.115s cpu time, 1.781s GC time, factor 1.43)
Finished HOL-Quotient_Examples (0:00:15 elapsed time, 0:00:40 cpu time, factor 2.57)
Running HOL-Record_Benchmark ...
Timing HOL-Record_Benchmark (8 threads, 104.397s elapsed time, 149.974s cpu time, 11.378s GC time, factor 1.44)
Finished HOL-Record_Benchmark (0:01:44 elapsed time, 0:02:30 cpu time, factor 1.43)
Running HOL-SET_Protocol ...
Timing HOL-SET_Protocol (8 threads, 10.576s elapsed time, 56.670s cpu time, 2.355s GC time, factor 5.36)
Finished HOL-SET_Protocol (0:00:11 elapsed time, 0:00:57 cpu time, factor 5.05)
Running HOL-UNITY ...
Timing HOL-UNITY (8 threads, 10.434s elapsed time, 54.409s cpu time, 5.614s GC time, factor 5.21)
Finished HOL-UNITY (0:00:11 elapsed time, 0:00:55 cpu time, factor 4.90)
Building HOL-Word ...
Timing HOL-Word (8 threads, 4.798s elapsed time, 23.684s cpu time, 1.202s GC time, factor 4.94)
Finished HOL-Word (0:00:09 elapsed time, 0:00:31 cpu time, factor 3.44)
Running HOL-Word-SMT_Examples ...
Timing HOL-Word-SMT_Examples (8 threads, 36.779s elapsed time, 50.467s cpu time, 0.723s GC time, factor 1.37)
Finished HOL-Word-SMT_Examples (0:00:37 elapsed time, 0:00:56 cpu time, factor 1.53)
Running HOL-ex ...
Timing HOL-ex (8 threads, 125.961s elapsed time, 613.364s cpu time, 57.526s GC time, factor 4.87)
Finished HOL-ex (0:02:07 elapsed time, 0:11:22 cpu time, factor 5.38)
Building HOLCF ...
Timing HOLCF (8 threads, 6.192s elapsed time, 16.688s cpu time, 1.081s GC time, factor 2.70)
Finished HOLCF (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.29)
Running IOA ...
Timing IOA (8 threads, 3.576s elapsed time, 14.246s cpu time, 0.627s GC time, factor 3.98)
Finished IOA (0:00:04 elapsed time, 0:00:14 cpu time, factor 3.55)
Building ZF ...
Timing ZF (8 threads, 6.038s elapsed time, 21.053s cpu time, 1.675s GC time, factor 3.49)
Finished ZF (0:00:07 elapsed time, 0:00:22 cpu time, factor 3.26)
Building ZF-Induct ...
Timing ZF-Induct (8 threads, 1.075s elapsed time, 5.399s cpu time, 0.273s GC time, factor 5.02)
Finished ZF-Induct (0:00:01 elapsed time, 0:00:06 cpu time)
Running ZF-UNITY ...
Timing ZF-UNITY (8 threads, 2.207s elapsed time, 14.589s cpu time, 0.650s GC time, factor 6.61)
Finished ZF-UNITY (0:00:02 elapsed time, 0:00:14 cpu time)

Finished at Wed Jul 17 15:58:22 GMT+1 2019
0:43:21 elapsed time, 2:54:06 cpu time, factor 4.02


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.