Isabelle build status for macOS 12 Monterey (Intel), 2 threads
- status date:
- 07-Apr-2026 07:34:42 +0200
- build host:
- mini1-monterey
- HOL-Analysis (0:17:59 elapsed time, 0:31:32 cpu time, factor 1.75)
- HOL-Data_Structures (0:09:48 elapsed time, 0:16:17 cpu time, factor 1.66)
- HOL-Proofs (0:07:27 elapsed time, 0:11:21 cpu time, factor 1.52)
- HOL-Nominal-Examples (0:06:47 elapsed time, 0:12:29 cpu time, factor 1.84)
- HOL-Decision_Procs (0:06:08 elapsed time, 0:11:36 cpu time, factor 1.89)
- HOL (0:05:18 elapsed time, 0:09:54 cpu time, factor 1.87)
- HOL-Algebra (0:04:04 elapsed time, 0:07:37 cpu time, factor 1.87)
- HOL-Auth (0:02:23 elapsed time, 0:03:45 cpu time, factor 1.57)
- HOL-Homology (0:02:08 elapsed time, 0:03:50 cpu time, factor 1.80)
- HOL-Real_Asymp (0:02:06 elapsed time, 0:03:59 cpu time, factor 1.90)
- HOL-MicroJava (0:02:05 elapsed time, 0:03:36 cpu time, factor 1.73)
- Codegen (0:01:51 elapsed time, 0:03:24 cpu time, factor 1.84)
- HOL-Quickcheck_Examples (0:01:50 elapsed time, 0:02:02 cpu time, factor 1.11)
- HOL-IMP (0:01:46 elapsed time, 0:02:59 cpu time, factor 1.69)
- HOL-Proofs-Extraction (0:01:44 elapsed time, 0:02:34 cpu time, factor 1.48)
- HOL-Computational_Algebra (0:01:43 elapsed time, 0:03:11 cpu time, factor 1.85)
- HOL-Hoare_Parallel (0:01:42 elapsed time, 0:03:09 cpu time, factor 1.85)
- HOL-Complex_Analysis (0:01:36 elapsed time, 0:02:48 cpu time, factor 1.75)
- HOL-Record_Benchmark (0:01:33 elapsed time, 0:02:11 cpu time, factor 1.41)
- HOL-Number_Theory (0:01:33 elapsed time, 0:02:45 cpu time, factor 1.77)
- HOL-Bali (0:01:30 elapsed time, 0:02:44 cpu time, factor 1.82)
- HOL-Examples (0:01:28 elapsed time, 0:02:36 cpu time, factor 1.77)
- HOL-Proofs-Lambda (0:01:21 elapsed time, 0:01:29 cpu time, factor 1.10)
- HOL-SMT_Examples (0:01:01 elapsed time, 0:01:50 cpu time, factor 1.80)
- HOL-UNITY (0:00:53 elapsed time, 0:01:26 cpu time, factor 1.62)
- HOL-Nitpick_Examples (0:00:50 elapsed time, 0:01:09 cpu time, factor 1.38)
- HOL-SET_Protocol (0:00:49 elapsed time, 0:01:17 cpu time, factor 1.57)
- Datatypes (0:00:45 elapsed time, 0:01:09 cpu time, factor 1.53)
- Corec (0:00:43 elapsed time, 0:00:59 cpu time, factor 1.37)
- HOL-Metis_Examples (0:00:33 elapsed time, 0:00:50 cpu time, factor 1.52)
- HOL-Analysis-ex (0:00:27 elapsed time, 0:00:36 cpu time, factor 1.33)
- HOL-Matrix_LP (0:00:26 elapsed time, 0:00:43 cpu time, factor 1.65)
- HOL-Combinatorics (0:00:24 elapsed time, 0:00:43 cpu time, factor 1.79)
- HOL-SPARK (0:00:23 elapsed time, 0:00:38 cpu time, factor 1.65)
- HOL-Hoare (0:00:23 elapsed time, 0:00:41 cpu time, factor 1.78)
- Tutorial (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.81)
- HOL-Cardinals (0:00:20 elapsed time, 0:00:33 cpu time, factor 1.65)
- HOLCF (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.78)
- ZF (0:00:18 elapsed time, 0:00:29 cpu time, factor 1.61)
- HOLCF-Library (0:00:16 elapsed time, 0:00:27 cpu time, factor 1.69)
- IOA (0:00:16 elapsed time, 0:00:28 cpu time, factor 1.75)
- HOL-Statespace (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.13)
- HOL-Nonstandard_Analysis (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.67)
- Pure (0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07)
- Isar_Ref (0:00:14 elapsed time, 0:00:25 cpu time, factor 1.79)
- HOL-Induct (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.85)
- HOL-Nominal (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.69)
- HOL-SPARK-Examples (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.62)
- HOL-Types_To_Sets (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.58)
- HOL-ZF (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.83)
- HOL-Import (0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00)
- Typeclass_Hierarchy (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.70)
- ZF-UNITY (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.80)
- ZF-Constructible (0:00:10 elapsed time, 0:00:20 cpu time, factor 2.00)
- HOL-Hahn_Banach (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.89)
- HOL-TLA-Memory (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.78)
- System (0:00:08 elapsed time)
- Haskell (0:00:08 elapsed time)
- HOLCF-Tutorial (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.38)
- HOL-Unix (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71)
- ZF-ex (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.43)
- IOA-NTP (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50)
- FOL-ex (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33)
- HOL-Eisbach (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.83)
- HOL-Isar_Examples (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50)
- HOL-NanoJava (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60)
- HOL-TLA (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20)
- IOA-ABP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60)
- HOL-TPTP (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00)
- HOLCF-IMP (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.40)
- ZF-Induct (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75)
- HOL-SPARK-Manual (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50)
- Prog_Prove (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75)
- HOLCF-FOCUS (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75)
- HOLCF-ex (0:00:04 elapsed time, 0:00:08 cpu time, factor 2.00)
- HOL-IMPP (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50)
- ZF-AC (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50)
- CCL (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50)
- HOL-Proofs-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33)
- Tools (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- HOL-IOA (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- FOL (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- Implementation (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33)
- FOLP-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33)
- Functions (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- HOL-Nonstandard_Analysis-Examples (0:00:02 elapsed time, 0:00:03 cpu time)
- HOL-Mutabelle (0:00:02 elapsed time)
- Sequents (0:00:02 elapsed time, 0:00:04 cpu time)
- FOLP (0:00:02 elapsed time)
- IOA-Storage (0:00:02 elapsed time)
- Locales (0:00:02 elapsed time)
- HOL-TLA-Inc (0:00:02 elapsed time, 0:00:03 cpu time)
- HOL-Lattice (0:00:02 elapsed time, 0:00:03 cpu time)
- Eisbach (0:00:02 elapsed time)
- HOL-Mirabelle-ex (0:00:02 elapsed time)
- Sugar (0:00:01 elapsed time)
- ZF-Resid (0:00:01 elapsed time)
- ZF-Coind (0:00:01 elapsed time)
- HOL-TLA-Buffer (0:00:01 elapsed time)
- How_to_Prove_it (0:00:01 elapsed time)
- Classes (0:00:01 elapsed time)
- ZF-IMP (0:00:01 elapsed time)
- CTT (0:00:01 elapsed time)
- Demo_FoilTeX (0:00:01 elapsed time)
- Demo_LLNCS (0:00:01 elapsed time)
- Demo_LIPIcs (0:00:01 elapsed time)
- IOA-ex (0:00:01 elapsed time)
- HOL-Real_Asymp-Manual (0:00:01 elapsed time)
- Demo_Easychair (0:00:01 elapsed time)
- JEdit (0:00:01 elapsed time)
- Main (0:00:01 elapsed time)
- Demo_EPTCS (0:00:01 elapsed time)
- HOL-Prolog (0:00:01 elapsed time)
- HOL-Probability (0:00:00 elapsed time)
- HOL-Predicate_Compile_Examples (0:00:00 elapsed time)
- Logics (0:00:00 elapsed time)
- Logics_ZF (0:00:00 elapsed time)
- SML (0:00:00 elapsed time)
- Sledgehammer (0:00:00 elapsed time)
- Nitpick (0:00:00 elapsed time)
- Pure-ex (0:00:00 elapsed time)
- HOL-Imperative_HOL (0:00:00 elapsed time)
- Cube (0:00:00 elapsed time)
- Intro (0:00:00 elapsed time)
- HOL-Library (0:00:00 elapsed time)
- HOL-Quotient_Examples (0:00:00 elapsed time)
- Pure-Examples (0:00:00 elapsed time)
HOL-Analysis
- data:
- CSV
- timing:
- 0:17:59 elapsed time, 0:31:32 cpu time, factor 1.75
- ML timing:
- 1008.684s elapsed time, 1784.870s cpu time, 127.113s GC time, factor 1.77
- ML code maximum:
- 3.6 MiB
- ML code average:
- 3.5 MiB
- ML stack maximum:
- 35.5 MiB
- ML stack average:
- 30.8 MiB
- ML heap maximum:
- 7.5 GiB
- ML heap average:
- 5.2 GiB
- ML heap stored:
- 264.1 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Data_Structures
- data:
- CSV
- timing:
- 0:09:48 elapsed time, 0:16:17 cpu time, factor 1.66
- ML timing:
- 583.983s elapsed time, 969.927s cpu time, 81.534s GC time, factor 1.66
- ML stack maximum:
- 20 MiB
- ML stack average:
- 11.6 MiB
- ML heap maximum:
- 4.2 GiB
- ML heap average:
- 3.8 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Proofs
- data:
- CSV
- timing:
- 0:07:27 elapsed time, 0:11:21 cpu time, factor 1.52
- ML timing:
- 339.112s elapsed time, 513.245s cpu time, 73.389s GC time, factor 1.51
- ML code maximum:
- 28 MiB
- ML code average:
- 22.1 MiB
- ML stack maximum:
- 60.3 MiB
- ML stack average:
- 34 MiB
- ML heap maximum:
- 10.8 GiB
- ML heap average:
- 5.5 GiB
- ML heap stored:
- 377.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Nominal-Examples
- data:
- CSV
- timing:
- 0:06:47 elapsed time, 0:12:29 cpu time, factor 1.84
- ML timing:
- 402.737s elapsed time, 741.365s cpu time, 47.672s GC time, factor 1.84
- ML stack maximum:
- 39 MiB
- ML stack average:
- 36.8 MiB
- ML heap maximum:
- 6.2 GiB
- ML heap average:
- 5.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Decision_Procs
- data:
- CSV
- timing:
- 0:06:08 elapsed time, 0:11:36 cpu time, factor 1.89
- ML timing:
- 364.737s elapsed time, 691.595s cpu time, 42.821s GC time, factor 1.90
- ML code maximum:
- 4.6 MiB
- ML code average:
- 2.1 MiB
- ML stack maximum:
- 68.8 MiB
- ML stack average:
- 35.4 MiB
- ML heap maximum:
- 13 GiB
- ML heap average:
- 9.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL
- data:
- CSV
- timing:
- 0:05:18 elapsed time, 0:09:54 cpu time, factor 1.87
- ML timing:
- 294.457s elapsed time, 558.523s cpu time, 40.189s GC time, factor 1.90
- ML code maximum:
- 35.1 MiB
- ML code average:
- 27.4 MiB
- ML stack maximum:
- 56.3 MiB
- ML stack average:
- 43.4 MiB
- ML heap maximum:
- 4 GiB
- ML heap average:
- 3.3 GiB
- ML heap stored:
- 208.6 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Algebra
- data:
- CSV
- timing:
- 0:04:04 elapsed time, 0:07:37 cpu time, factor 1.87
- ML timing:
- 224.088s elapsed time, 427.072s cpu time, 68.392s GC time, factor 1.91
- ML stack maximum:
- 8.1 MiB
- ML stack average:
- 6.7 MiB
- ML heap maximum:
- 8 GiB
- ML heap average:
- 3.7 GiB
- ML heap stored:
- 65 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Auth
- data:
- CSV
- timing:
- 0:02:23 elapsed time, 0:03:45 cpu time, factor 1.57
- ML timing:
- 137.450s elapsed time, 217.657s cpu time, 4.138s GC time, factor 1.58
- ML stack maximum:
- 13 MiB
- ML stack average:
- 11.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 31.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Homology
- data:
- CSV
- timing:
- 0:02:08 elapsed time, 0:03:50 cpu time, factor 1.80
- ML timing:
- 125.565s elapsed time, 227.098s cpu time, 16.378s GC time, factor 1.81
- ML stack maximum:
- 17.9 MiB
- ML stack average:
- 14.9 MiB
- ML heap maximum:
- 3.6 GiB
- ML heap average:
- 3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Real_Asymp
- data:
- CSV
- timing:
- 0:02:06 elapsed time, 0:03:59 cpu time, factor 1.90
- ML timing:
- 113.872s elapsed time, 221.594s cpu time, 9.486s GC time, factor 1.95
- ML code maximum:
- 3 MiB
- ML code average:
- 2.7 MiB
- ML stack maximum:
- 26 MiB
- ML stack average:
- 19.4 MiB
- ML heap maximum:
- 3.6 GiB
- ML heap average:
- 2.6 GiB
- ML heap stored:
- 67.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-MicroJava
- data:
- CSV
- timing:
- 0:02:05 elapsed time, 0:03:36 cpu time, factor 1.73
- ML timing:
- 123.645s elapsed time, 215.199s cpu time, 6.513s GC time, factor 1.74
- ML code maximum:
- 1.3 MiB
- ML stack maximum:
- 8.9 MiB
- ML stack average:
- 7 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.6 GiB
- Isabelle version:
- 6b2ac8d13c7a






Codegen
- data:
- CSV
- timing:
- 0:01:51 elapsed time, 0:03:24 cpu time, factor 1.84
- ML timing:
- 109.400s elapsed time, 201.929s cpu time, 5.958s GC time, factor 1.85
- ML stack maximum:
- 12.8 MiB
- ML stack average:
- 10.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Quickcheck_Examples
- data:
- CSV
- timing:
- 0:01:50 elapsed time, 0:02:02 cpu time, factor 1.11
- ML timing:
- 108.995s elapsed time, 120.796s cpu time, 4.607s GC time, factor 1.11
- ML code maximum:
- 12.2 MiB
- ML code average:
- 8.5 MiB
- ML stack maximum:
- 14.8 MiB
- ML stack average:
- 13.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-IMP
- data:
- CSV
- timing:
- 0:01:46 elapsed time, 0:02:59 cpu time, factor 1.69
- ML timing:
- 105.016s elapsed time, 177.740s cpu time, 9.911s GC time, factor 1.69
- ML code maximum:
- 10.8 MiB
- ML code average:
- 4.3 MiB
- ML stack maximum:
- 11.9 MiB
- ML stack average:
- 3.9 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.6 GiB
- Isabelle version:
- 6b2ac8d13c7a






- data:
- CSV
- timing:
- 0:01:44 elapsed time, 0:02:34 cpu time, factor 1.48
- ML timing:
- 101.714s elapsed time, 151.624s cpu time, 11.117s GC time, factor 1.49
- ML stack maximum:
- 13.3 MiB
- ML stack average:
- 11.8 MiB
- ML heap maximum:
- 3.1 GiB
- ML heap average:
- 2 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Computational_Algebra
- data:
- CSV
- timing:
- 0:01:43 elapsed time, 0:03:11 cpu time, factor 1.85
- ML timing:
- 92.475s elapsed time, 176.421s cpu time, 7.502s GC time, factor 1.91
- ML stack maximum:
- 28.5 MiB
- ML stack average:
- 19.3 MiB
- ML heap maximum:
- 2.9 GiB
- ML heap average:
- 2 GiB
- ML heap stored:
- 42.3 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Hoare_Parallel
- data:
- CSV
- timing:
- 0:01:42 elapsed time, 0:03:09 cpu time, factor 1.85
- ML timing:
- 100.618s elapsed time, 187.349s cpu time, 2.976s GC time, factor 1.86
- ML stack maximum:
- 6.5 MiB
- ML stack average:
- 3.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Complex_Analysis
- data:
- CSV
- timing:
- 0:01:36 elapsed time, 0:02:48 cpu time, factor 1.75
- ML timing:
- 93.538s elapsed time, 165.833s cpu time, 3.211s GC time, factor 1.77
- ML stack maximum:
- 17.6 MiB
- ML stack average:
- 16.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Record_Benchmark
- data:
- CSV
- timing:
- 0:01:33 elapsed time, 0:02:11 cpu time, factor 1.41
- ML timing:
- 91.784s elapsed time, 129.480s cpu time, 8.695s GC time, factor 1.41
- ML stack maximum:
- 4.5 MiB
- ML stack average:
- 2.9 MiB
- ML heap maximum:
- 2.2 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Number_Theory
- data:
- CSV
- timing:
- 0:01:33 elapsed time, 0:02:45 cpu time, factor 1.77
- ML timing:
- 91.006s elapsed time, 162.844s cpu time, 11.252s GC time, factor 1.79
- ML stack maximum:
- 8.5 MiB
- ML stack average:
- 7.1 MiB
- ML heap maximum:
- 4.4 GiB
- ML heap average:
- 3.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Bali
- data:
- CSV
- timing:
- 0:01:30 elapsed time, 0:02:44 cpu time, factor 1.82
- ML timing:
- 89.273s elapsed time, 162.051s cpu time, 6.668s GC time, factor 1.82
- ML stack maximum:
- 14.5 MiB
- ML stack average:
- 9.7 MiB
- ML heap maximum:
- 3.1 GiB
- ML heap average:
- 2.6 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Examples
- data:
- CSV
- timing:
- 0:01:28 elapsed time, 0:02:36 cpu time, factor 1.77
- ML timing:
- 86.227s elapsed time, 154.112s cpu time, 9.977s GC time, factor 1.79
- ML stack maximum:
- 12.8 MiB
- ML stack average:
- 11.2 MiB
- ML heap maximum:
- 3.4 GiB
- ML heap average:
- 2.5 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Proofs-Lambda
- data:
- CSV
- timing:
- 0:01:21 elapsed time, 0:01:29 cpu time, factor 1.10
- ML timing:
- 79.440s elapsed time, 87.240s cpu time, 2.990s GC time, factor 1.10
- ML stack maximum:
- 4.1 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-SMT_Examples
- data:
- CSV
- timing:
- 0:01:01 elapsed time, 0:01:50 cpu time, factor 1.80
- ML timing:
- 59.742s elapsed time, 109.067s cpu time, 2.066s GC time, factor 1.83
- ML stack maximum:
- 10.9 MiB
- ML stack average:
- 10.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-UNITY
- data:
- CSV
- timing:
- 0:00:53 elapsed time, 0:01:26 cpu time, factor 1.62
- ML timing:
- 51.586s elapsed time, 84.906s cpu time, 4.058s GC time, factor 1.65
- ML stack maximum:
- 14.3 MiB
- ML stack average:
- 12.3 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Nitpick_Examples
- data:
- CSV
- timing:
- 0:00:50 elapsed time, 0:01:09 cpu time, factor 1.38
- ML timing:
- 49.217s elapsed time, 67.875s cpu time, 1.229s GC time, factor 1.38
- ML stack maximum:
- 5.9 MiB
- ML stack average:
- 4.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-SET_Protocol
- data:
- CSV
- timing:
- 0:00:49 elapsed time, 0:01:17 cpu time, factor 1.57
- ML timing:
- 48.533s elapsed time, 76.202s cpu time, 0.847s GC time, factor 1.57
- ML stack maximum:
- 5.4 MiB
- ML stack average:
- 4.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






Datatypes
- data:
- CSV
- timing:
- 0:00:45 elapsed time, 0:01:09 cpu time, factor 1.53
- ML timing:
- 30.994s elapsed time, 49.226s cpu time, 2.637s GC time, factor 1.59
- ML stack maximum:
- 5.9 MiB
- ML stack average:
- 3.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 73.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






Corec
- data:
- CSV
- timing:
- 0:00:43 elapsed time, 0:00:59 cpu time, factor 1.37
- ML timing:
- 40.955s elapsed time, 56.720s cpu time, 4.538s GC time, factor 1.38
- ML code maximum:
- 2.2 MiB
- ML code average:
- 2 MiB
- ML stack maximum:
- 9.4 MiB
- ML stack average:
- 8.3 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Metis_Examples
- data:
- CSV
- timing:
- 0:00:33 elapsed time, 0:00:50 cpu time, factor 1.52
- ML timing:
- 32.290s elapsed time, 49.102s cpu time, 3.874s GC time, factor 1.52
- ML stack maximum:
- 4.6 MiB
- ML stack average:
- 3.9 MiB
- ML heap maximum:
- 1.7 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Analysis-ex
- data:
- CSV
- timing:
- 0:00:27 elapsed time, 0:00:36 cpu time, factor 1.33
- ML timing:
- 26.139s elapsed time, 35.379s cpu time, 0.244s GC time, factor 1.35
- ML stack maximum:
- 3.3 MiB
- ML stack average:
- 3.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Matrix_LP
- data:
- CSV
- timing:
- 0:00:26 elapsed time, 0:00:43 cpu time, factor 1.65
- ML timing:
- 25.163s elapsed time, 41.932s cpu time, 0.938s GC time, factor 1.67
- ML code maximum:
- 1 MiB
- ML stack maximum:
- 4.4 MiB
- ML stack average:
- 3.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Combinatorics
- data:
- CSV
- timing:
- 0:00:24 elapsed time, 0:00:43 cpu time, factor 1.79
- ML timing:
- 23.227s elapsed time, 41.983s cpu time, 1.384s GC time, factor 1.81
- ML stack maximum:
- 10.8 MiB
- ML stack average:
- 9.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-SPARK
- data:
- CSV
- timing:
- 0:00:23 elapsed time, 0:00:38 cpu time, factor 1.65
- ML timing:
- 17.338s elapsed time, 31.265s cpu time, 0.869s GC time, factor 1.80
- ML stack maximum:
- 9 MiB
- ML stack average:
- 6 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 14.9 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Hoare
- data:
- CSV
- timing:
- 0:00:23 elapsed time, 0:00:41 cpu time, factor 1.78
- ML timing:
- 22.032s elapsed time, 40.900s cpu time, 0.843s GC time, factor 1.86
- ML stack maximum:
- 2.7 MiB
- ML stack average:
- 2.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






Tutorial
- data:
- CSV
- timing:
- 0:00:21 elapsed time, 0:00:38 cpu time, factor 1.81
- ML timing:
- 19.524s elapsed time, 36.603s cpu time, 3.401s GC time, factor 1.87
- ML stack maximum:
- 4.1 MiB
- ML stack average:
- 2.8 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Cardinals
- data:
- CSV
- timing:
- 0:00:20 elapsed time, 0:00:33 cpu time, factor 1.65
- ML timing:
- 18.306s elapsed time, 32.900s cpu time, 0.770s GC time, factor 1.80
- ML stack maximum:
- 7 MiB
- ML stack average:
- 6.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF
- data:
- CSV
- timing:
- 0:00:18 elapsed time, 0:00:32 cpu time, factor 1.78
- ML timing:
- 12.666s elapsed time, 25.547s cpu time, 1.064s GC time, factor 2.02
- ML stack maximum:
- 5.4 MiB
- ML stack average:
- 2.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1 GiB
- ML heap stored:
- 19.4 MiB
- Isabelle version:
- 6b2ac8d13c7a






ZF
- data:
- CSV
- timing:
- 0:00:18 elapsed time, 0:00:29 cpu time, factor 1.61
- ML timing:
- 16.586s elapsed time, 27.411s cpu time, 2.222s GC time, factor 1.65
- ML code maximum:
- 1.8 MiB
- ML code average:
- 1.5 MiB
- ML stack maximum:
- 8.4 MiB
- ML stack average:
- 6.9 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 15.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF-Library
- data:
- CSV
- timing:
- 0:00:16 elapsed time, 0:00:27 cpu time, factor 1.69
- ML timing:
- 11.463s elapsed time, 21.117s cpu time, 0.561s GC time, factor 1.84
- ML stack maximum:
- 4 MiB
- ML stack average:
- 2.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1 GiB
- ML heap stored:
- 9.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






IOA
- data:
- CSV
- timing:
- 0:00:16 elapsed time, 0:00:28 cpu time, factor 1.75
- ML timing:
- 10.943s elapsed time, 20.876s cpu time, 0.632s GC time, factor 1.91
- ML stack maximum:
- 2.9 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 999.1 MiB
- ML heap stored:
- 6.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Statespace
- data:
- CSV
- timing:
- 0:00:15 elapsed time, 0:00:17 cpu time, factor 1.13
- ML timing:
- 14.330s elapsed time, 16.221s cpu time, 0.331s GC time, factor 1.13
- ML stack maximum:
- 1.8 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Nonstandard_Analysis
- data:
- CSV
- timing:
- 0:00:15 elapsed time, 0:00:25 cpu time, factor 1.67
- ML timing:
- 9.665s elapsed time, 18.751s cpu time, 0.612s GC time, factor 1.94
- ML stack maximum:
- 3.9 MiB
- ML stack average:
- 2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 999.1 MiB
- ML heap stored:
- 10.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






Pure
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07
- ML timing:
- 0.696s elapsed time, 0.741s cpu time, 0.016s GC time, factor 1.06
- ML code maximum:
- 17.7 MiB
- ML code average:
- 17.6 MiB
- ML stack maximum:
- 2 MiB
- ML stack average:
- 2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 520.9 MiB
- ML heap stored:
- 23.9 MiB
- Isabelle version:
- 6b2ac8d13c7a






Isar_Ref
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:25 cpu time, factor 1.79
- ML timing:
- 13.517s elapsed time, 24.475s cpu time, 1.044s GC time, factor 1.81
- ML stack maximum:
- 9.1 MiB
- ML stack average:
- 7.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Induct
- data:
- CSV
- timing:
- 0:00:13 elapsed time, 0:00:24 cpu time, factor 1.85
- ML timing:
- 12.373s elapsed time, 23.345s cpu time, 2.415s GC time, factor 1.89
- ML stack maximum:
- 2.2 MiB
- ML stack average:
- 1.9 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Nominal
- data:
- CSV
- timing:
- 0:00:13 elapsed time, 0:00:22 cpu time, factor 1.69
- ML timing:
- 8.748s elapsed time, 16.901s cpu time, 0.601s GC time, factor 1.93
- ML code maximum:
- 1.8 MiB
- ML code average:
- 1.3 MiB
- ML stack maximum:
- 6 MiB
- ML stack average:
- 3.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 997.2 MiB
- ML heap stored:
- 9.4 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-SPARK-Examples
- data:
- CSV
- timing:
- 0:00:13 elapsed time, 0:00:21 cpu time, factor 1.62
- ML timing:
- 12.516s elapsed time, 20.805s cpu time, 0.231s GC time, factor 1.66
- ML stack maximum:
- 4.5 MiB
- ML stack average:
- 3.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Types_To_Sets
- data:
- CSV
- timing:
- 0:00:12 elapsed time, 0:00:19 cpu time, factor 1.58
- ML timing:
- 10.886s elapsed time, 18.106s cpu time, 0.391s GC time, factor 1.66
- ML stack maximum:
- 2.7 MiB
- ML stack average:
- 2.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-ZF
- data:
- CSV
- timing:
- 0:00:12 elapsed time, 0:00:22 cpu time, factor 1.83
- ML timing:
- 11.565s elapsed time, 21.039s cpu time, 0.717s GC time, factor 1.82
- ML stack maximum:
- 10.3 MiB
- ML stack average:
- 8.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Import
- data:
- CSV
- timing:
- 0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00
- ML timing:
- 9.911s elapsed time, 10.433s cpu time, 0.274s GC time, factor 1.05
- ML stack maximum:
- 65.2 MiB
- ML stack average:
- 58.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






Typeclass_Hierarchy
- data:
- CSV
- timing:
- 0:00:10 elapsed time, 0:00:17 cpu time, factor 1.70
- ML timing:
- 9.758s elapsed time, 16.155s cpu time, 0.523s GC time, factor 1.66
- ML stack maximum:
- 10.3 MiB
- ML stack average:
- 8.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-UNITY
- data:
- CSV
- timing:
- 0:00:10 elapsed time, 0:00:18 cpu time, factor 1.80
- ML timing:
- 9.882s elapsed time, 18.127s cpu time, 0.507s GC time, factor 1.83
- ML stack maximum:
- 3.3 MiB
- ML stack average:
- 2.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-Constructible
- data:
- CSV
- timing:
- 0:00:10 elapsed time, 0:00:20 cpu time, factor 2.00
- ML timing:
- 10.197s elapsed time, 19.940s cpu time, 2.357s GC time, factor 1.96
- ML stack maximum:
- 5 MiB
- ML stack average:
- 4 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Hahn_Banach
- data:
- CSV
- timing:
- 0:00:09 elapsed time, 0:00:17 cpu time, factor 1.89
- ML timing:
- 8.425s elapsed time, 16.068s cpu time, 0.502s GC time, factor 1.91
- ML stack maximum:
- 2.5 MiB
- ML stack average:
- 1.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-TLA-Memory
- data:
- CSV
- timing:
- 0:00:09 elapsed time, 0:00:16 cpu time, factor 1.78
- ML timing:
- 8.623s elapsed time, 15.450s cpu time, 0.229s GC time, factor 1.79
- ML stack maximum:
- 3.4 MiB
- ML stack average:
- 2.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






System
- data:
- CSV
- timing:
- 0:00:08 elapsed time
- ML timing:
- 8.392s elapsed time, 1.458s cpu time, 0.000s GC time, factor 0.17
- ML stack maximum:
- 3.3 MiB
- ML stack average:
- 3.2 MiB
- ML heap maximum:
- 627 MiB
- ML heap average:
- 420.5 MiB
- Isabelle version:
- 6b2ac8d13c7a






Haskell
- data:
- CSV
- timing:
- 0:00:08 elapsed time
- ML timing:
- 7.856s elapsed time, 0.481s cpu time, 0.000s GC time, factor 0.06
- ML stack maximum:
- 5.1 MiB
- ML stack average:
- 4.9 MiB
- ML heap maximum:
- 394 MiB
- ML heap average:
- 390.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF-Tutorial
- data:
- CSV
- timing:
- 0:00:08 elapsed time, 0:00:11 cpu time, factor 1.38
- ML timing:
- 7.513s elapsed time, 10.114s cpu time, 0.184s GC time, factor 1.35
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Unix
- data:
- CSV
- timing:
- 0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71
- ML timing:
- 5.955s elapsed time, 11.599s cpu time, 0.476s GC time, factor 1.95
- ML stack maximum:
- 3.3 MiB
- ML stack average:
- 2.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-ex
- data:
- CSV
- timing:
- 0:00:07 elapsed time, 0:00:10 cpu time, factor 1.43
- ML timing:
- 6.551s elapsed time, 9.687s cpu time, 0.271s GC time, factor 1.48
- ML stack maximum:
- 7.1 MiB
- ML stack average:
- 6.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






IOA-NTP
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50
- ML timing:
- 4.952s elapsed time, 8.741s cpu time, 0.272s GC time, factor 1.77
- ML stack maximum:
- 1.2 MiB
- ML stack average:
- 1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






FOL-ex
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33
- ML timing:
- 5.916s elapsed time, 7.972s cpu time, 0.167s GC time, factor 1.35
- ML stack maximum:
- 5.6 MiB
- ML stack average:
- 4.6 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Eisbach
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:11 cpu time, factor 1.83
- ML timing:
- 5.459s elapsed time, 10.659s cpu time, 0.312s GC time, factor 1.95
- ML code maximum:
- 1.9 MiB
- ML code average:
- 1.5 MiB
- ML stack maximum:
- 3.9 MiB
- ML stack average:
- 3.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Isar_Examples
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50
- ML timing:
- 5.096s elapsed time, 8.483s cpu time, 0.234s GC time, factor 1.66
- ML stack maximum:
- 1.9 MiB
- ML stack average:
- 1.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-NanoJava
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60
- ML timing:
- 4.311s elapsed time, 7.547s cpu time, 0.267s GC time, factor 1.75
- ML stack maximum:
- 1.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-TLA
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20
- ML timing:
- 1.267s elapsed time, 2.010s cpu time, 0.049s GC time, factor 1.59
- ML stack maximum:
- 2.6 MiB
- ML heap maximum:
- 841 MiB
- ML heap average:
- 240.9 MiB
- ML heap stored:
- 3 MiB
- Isabelle version:
- 6b2ac8d13c7a






IOA-ABP
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60
- ML timing:
- 4.027s elapsed time, 7.067s cpu time, 0.205s GC time, factor 1.75
- ML stack maximum:
- 1.9 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-TPTP
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00
- ML timing:
- 3.985s elapsed time, 4.885s cpu time, 0.187s GC time, factor 1.23
- ML code maximum:
- 4 MiB
- ML code average:
- 2.8 MiB
- ML stack maximum:
- 21.2 MiB
- ML stack average:
- 19 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF-IMP
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:07 cpu time, factor 1.40
- ML timing:
- 3.855s elapsed time, 6.631s cpu time, 0.179s GC time, factor 1.72
- ML stack maximum:
- 1.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-Induct
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75
- ML timing:
- 3.758s elapsed time, 6.149s cpu time, 0.205s GC time, factor 1.64
- ML stack maximum:
- 3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 4.1 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-SPARK-Manual
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50
- ML timing:
- 2.969s elapsed time, 5.315s cpu time, 0.065s GC time, factor 1.79
- ML stack maximum:
- 1.9 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






Prog_Prove
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75
- ML timing:
- 3.421s elapsed time, 6.742s cpu time, 0.410s GC time, factor 1.97
- ML stack maximum:
- 3.4 MiB
- ML stack average:
- 3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF-FOCUS
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:07 cpu time, factor 1.75
- ML timing:
- 3.230s elapsed time, 6.241s cpu time, 0.149s GC time, factor 1.93
- ML stack maximum:
- 1.5 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOLCF-ex
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:08 cpu time, factor 2.00
- ML timing:
- 3.689s elapsed time, 7.223s cpu time, 0.299s GC time, factor 1.96
- ML stack maximum:
- 3.1 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-IMPP
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50
- ML timing:
- 3.143s elapsed time, 5.146s cpu time, 0.171s GC time, factor 1.64
- ML stack maximum:
- 1.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1003.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-AC
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50
- ML timing:
- 3.587s elapsed time, 6.530s cpu time, 0.267s GC time, factor 1.82
- ML stack maximum:
- 3.1 MiB
- ML stack average:
- 2.6 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- 6b2ac8d13c7a






CCL
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:06 cpu time, factor 1.50
- ML timing:
- 4.097s elapsed time, 5.778s cpu time, 0.281s GC time, factor 1.41
- ML code maximum:
- 1.6 MiB
- ML code average:
- 1.1 MiB
- ML stack maximum:
- 3.8 MiB
- ML stack average:
- 2.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Proofs-ex
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33
- ML timing:
- 2.173s elapsed time, 3.454s cpu time, 0.566s GC time, factor 1.59
- ML stack maximum:
- 6.4 MiB
- ML stack average:
- 3.8 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 818.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 2.779s elapsed time, 2.910s cpu time, 0.086s GC time, factor 1.05
- ML code maximum:
- 1.9 MiB
- ML code average:
- 1.3 MiB
- ML stack maximum:
- 2.6 MiB
- ML stack average:
- 1.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 866 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-IOA
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 1.936s elapsed time, 2.684s cpu time, 0.039s GC time, factor 1.39
- ML stack maximum:
- 1 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 961.3 MiB
- Isabelle version:
- 6b2ac8d13c7a






FOL
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 2.294s elapsed time, 2.532s cpu time, 0.057s GC time, factor 1.10
- ML code maximum:
- 1.4 MiB
- ML stack maximum:
- 2.4 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 850.4 MiB
- ML heap stored:
- 3.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






Implementation
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33
- ML timing:
- 2.396s elapsed time, 3.672s cpu time, 0.037s GC time, factor 1.53
- ML stack maximum:
- 8.6 MiB
- ML stack average:
- 5.8 MiB
- ML heap maximum:
- 1.1 GiB
- ML heap average:
- 825 MiB
- Isabelle version:
- 6b2ac8d13c7a






FOLP-ex
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:04 cpu time, factor 1.33
- ML timing:
- 2.550s elapsed time, 4.647s cpu time, 0.065s GC time, factor 1.82
- ML code maximum:
- 1.3 MiB
- ML stack maximum:
- 1.8 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






Functions
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 1.911s elapsed time, 2.540s cpu time, 0.039s GC time, factor 1.33
- ML stack maximum:
- 2.8 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.2 GiB
- ML heap average:
- 886.2 MiB
- Isabelle version:
- 6b2ac8d13c7a






LCF
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 2.490s elapsed time, 2.808s cpu time, 0.058s GC time, factor 1.13
- ML code maximum:
- 1.4 MiB
- ML stack maximum:
- 2.4 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Nonstandard_Analysis-Examples
- data:
- CSV
- timing:
- 0:00:02 elapsed time, 0:00:03 cpu time
- ML timing:
- 1.629s elapsed time, 2.116s cpu time, 0.037s GC time, factor 1.30
- ML heap maximum:
- 1.1 GiB
- ML heap average:
- 752.3 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Mutabelle
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.212s elapsed time, 1.310s cpu time, 0.096s GC time, factor 1.08
- ML stack maximum:
- 8.6 MiB
- ML stack average:
- 5.8 MiB
- ML heap maximum:
- 775 MiB
- ML heap average:
- 450.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






Sequents
- data:
- CSV
- timing:
- 0:00:02 elapsed time, 0:00:04 cpu time
- ML timing:
- 2.116s elapsed time, 4.193s cpu time, 0.087s GC time, factor 1.98
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 6b2ac8d13c7a






FOLP
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.948s elapsed time, 1.014s cpu time, 0.031s GC time, factor 1.07
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 760 MiB
- ML heap average:
- 320 MiB
- ML heap stored:
- 1.5 MiB
- Isabelle version:
- 6b2ac8d13c7a






IOA-Storage
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.143s elapsed time, 1.593s cpu time, 0.032s GC time, factor 1.39
- ML heap maximum:
- 759 MiB
- ML heap average:
- 612.7 MiB
- Isabelle version:
- 6b2ac8d13c7a






Locales
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.900s elapsed time, 1.632s cpu time, 0.045s GC time, factor 1.81
- ML stack maximum:
- 1.6 MiB
- ML heap maximum:
- 762 MiB
- ML heap average:
- 735.1 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-TLA-Inc
- data:
- CSV
- timing:
- 0:00:02 elapsed time, 0:00:03 cpu time
- ML timing:
- 1.682s elapsed time, 2.851s cpu time, 0.031s GC time, factor 1.70
- ML stack maximum:
- 1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 740.6 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Lattice
- data:
- CSV
- timing:
- 0:00:02 elapsed time, 0:00:03 cpu time
- ML timing:
- 1.646s elapsed time, 2.461s cpu time, 0.054s GC time, factor 1.50
- ML stack maximum:
- 1.5 MiB
- ML heap maximum:
- 843 MiB
- ML heap average:
- 511.3 MiB
- Isabelle version:
- 6b2ac8d13c7a






Eisbach
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.631s elapsed time, 1.978s cpu time, 0.060s GC time, factor 1.21
- ML stack maximum:
- 3.3 MiB
- ML stack average:
- 2.9 MiB
- ML heap maximum:
- 768 MiB
- ML heap average:
- 708.4 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Mirabelle-ex
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.277s elapsed time, 1.838s cpu time, 0.027s GC time, factor 1.44
- ML heap maximum:
- 758 MiB
- ML heap average:
- 366.1 MiB
- Isabelle version:
- 6b2ac8d13c7a






Sugar
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.652s elapsed time, 0.783s cpu time, 0.000s GC time, factor 1.20
- ML stack maximum:
- 1.9 MiB
- ML heap maximum:
- 453 MiB
- ML heap average:
- 235.3 MiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-Resid
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 1.063s elapsed time, 1.790s cpu time, 0.027s GC time, factor 1.68
- ML stack maximum:
- 1 MiB
- ML heap maximum:
- 896 MiB
- ML heap average:
- 788 MiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-Coind
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.519s elapsed time, 1.009s cpu time, 0.027s GC time, factor 1.94
- ML heap maximum:
- 759 MiB
- ML heap average:
- 759 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-TLA-Buffer
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.512s elapsed time, 0.843s cpu time, 0.000s GC time, factor 1.65
- ML heap maximum:
- 621 MiB
- ML heap average:
- 621 MiB
- Isabelle version:
- 6b2ac8d13c7a






How_to_Prove_it
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.217s elapsed time, 0.336s cpu time, 0.000s GC time, factor 1.55
- ML heap maximum:
- 53 MiB
- ML heap average:
- 53 MiB
- Isabelle version:
- 6b2ac8d13c7a






Classes
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.967s elapsed time, 1.390s cpu time, 0.031s GC time, factor 1.44
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 759 MiB
- ML heap average:
- 594 MiB
- Isabelle version:
- 6b2ac8d13c7a






ZF-IMP
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.756s elapsed time, 0.876s cpu time, 0.000s GC time, factor 1.16
- ML heap maximum:
- 537 MiB
- ML heap average:
- 416.5 MiB
- Isabelle version:
- 6b2ac8d13c7a






CTT
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.667s elapsed time, 1.005s cpu time, 0.054s GC time, factor 1.51
- ML stack maximum:
- 1.4 MiB
- ML stack average:
- 1.4 MiB
- ML heap maximum:
- 650 MiB
- ML heap average:
- 650 MiB
- Isabelle version:
- 6b2ac8d13c7a






Demo_FoilTeX
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.122s elapsed time, 0.160s cpu time, 0.000s GC time, factor 1.31
- ML heap maximum:
- 56 MiB
- ML heap average:
- 56 MiB
- Isabelle version:
- 6b2ac8d13c7a






Demo_LLNCS
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.126s elapsed time, 0.163s cpu time, 0.000s GC time, factor 1.29
- ML heap maximum:
- 56 MiB
- ML heap average:
- 56 MiB
- Isabelle version:
- 6b2ac8d13c7a






Demo_LIPIcs
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.124s elapsed time, 0.158s cpu time, 0.000s GC time, factor 1.27
- ML heap maximum:
- 55 MiB
- ML heap average:
- 55 MiB
- Isabelle version:
- 6b2ac8d13c7a






IOA-ex
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.659s elapsed time, 1.248s cpu time, 0.000s GC time, factor 1.89
- ML heap maximum:
- 610 MiB
- ML heap average:
- 351.1 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Real_Asymp-Manual
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.283s elapsed time, 0.399s cpu time, 0.000s GC time, factor 1.41
- ML heap maximum:
- 59 MiB
- ML heap average:
- 24 MiB
- Isabelle version:
- 6b2ac8d13c7a






Demo_Easychair
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.124s elapsed time, 0.158s cpu time, 0.000s GC time, factor 1.27
- ML heap maximum:
- 56 MiB
- ML heap average:
- 56 MiB
- Isabelle version:
- 6b2ac8d13c7a






JEdit
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.523s elapsed time, 0.556s cpu time, 0.000s GC time, factor 1.06
- ML stack maximum:
- 5.4 MiB
- ML stack average:
- 5.4 MiB
- ML heap maximum:
- 436 MiB
- ML heap average:
- 436 MiB
- Isabelle version:
- 6b2ac8d13c7a






Main
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.541s elapsed time, 0.606s cpu time, 0.000s GC time, factor 1.12
- ML stack maximum:
- 2.4 MiB
- ML stack average:
- 2.4 MiB
- ML heap maximum:
- 521 MiB
- ML heap average:
- 521 MiB
- Isabelle version:
- 6b2ac8d13c7a






Demo_EPTCS
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.124s elapsed time, 0.159s cpu time, 0.000s GC time, factor 1.28
- ML heap maximum:
- 58 MiB
- ML heap average:
- 58 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Prolog
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.228s elapsed time, 0.369s cpu time, 0.000s GC time, factor 1.62
- ML heap maximum:
- 64 MiB
- ML heap average:
- 64 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Probability
- data:
- CSV
- Isabelle version:
- 6b2ac8d13c7a
HOL-Predicate_Compile_Examples
- data:
- CSV
- Isabelle version:
- 6b2ac8d13c7a
Logics
- data:
- CSV
- ML heap maximum:
- 12 MiB
- ML heap average:
- 12 MiB
- Isabelle version:
- 6b2ac8d13c7a






Logics_ZF
- data:
- CSV
- ML timing:
- 0.310s elapsed time, 0.435s cpu time, 0.000s GC time, factor 1.40
- ML heap maximum:
- 257 MiB
- ML heap average:
- 257 MiB
- Isabelle version:
- 6b2ac8d13c7a






SML
- data:
- CSV
- ML timing:
- 0.008s elapsed time, 0.011s cpu time, 0.000s GC time, factor 1.38
- ML heap maximum:
- 24 MiB
- ML heap average:
- 24 MiB
- Isabelle version:
- 6b2ac8d13c7a






Sledgehammer
- data:
- CSV
- ML heap maximum:
- 12 MiB
- ML heap average:
- 12 MiB
- Isabelle version:
- 6b2ac8d13c7a






Nitpick
- data:
- CSV
- ML heap maximum:
- 12 MiB
- ML heap average:
- 12 MiB
- Isabelle version:
- 6b2ac8d13c7a






Pure-ex
- data:
- CSV
- ML timing:
- 0.275s elapsed time, 0.426s cpu time, 0.000s GC time, factor 1.55
- ML stack maximum:
- 1.2 MiB
- ML heap maximum:
- 132 MiB
- ML heap average:
- 132 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Imperative_HOL
- data:
- CSV
- Isabelle version:
- 6b2ac8d13c7a
Cube
- data:
- CSV
- ML timing:
- 0.231s elapsed time, 0.255s cpu time, 0.000s GC time, factor 1.10
- ML heap maximum:
- 55 MiB
- ML heap average:
- 47 MiB
- Isabelle version:
- 6b2ac8d13c7a






Intro
- data:
- CSV
- ML heap maximum:
- 12 MiB
- ML heap average:
- 12 MiB
- Isabelle version:
- 6b2ac8d13c7a






HOL-Library
- data:
- CSV
- Isabelle version:
- 6b2ac8d13c7a
HOL-Quotient_Examples
- data:
- CSV
- Isabelle version:
- 6b2ac8d13c7a
Pure-Examples
- data:
- CSV
- ML timing:
- 0.296s elapsed time, 0.324s cpu time, 0.000s GC time, factor 1.09
- ML heap maximum:
- 249 MiB
- ML heap average:
- 249 MiB
- Isabelle version:
- 6b2ac8d13c7a





