Isabelle build status for Linux (ARM)
- status date:
- 16-Aug-2026 08:39:57 +0200
- build host:
- linux-arm
- HOL-Quickcheck_Benchmark (0:40:57 elapsed time, 0:41:00 cpu time, factor 1.00)
- HOL-Data_Structures (0:31:52 elapsed time, 0:31:57 cpu time, factor 1.00)
- HOL-Codegenerator_Test (0:25:23 elapsed time, 0:20:07 cpu time, factor 0.79)
- HOL-Nominal-Examples (0:24:10 elapsed time, 0:24:10 cpu time, factor 1.00)
- HOL-ex (0:23:24 elapsed time, 0:23:01 cpu time, factor 0.98)
- HOL-Decision_Procs (0:20:52 elapsed time, 0:21:00 cpu time, factor 1.01)
- HOL-Library (0:20:09 elapsed time, 0:20:08 cpu time, factor 1.00)
- HOL-Corec_Examples (0:15:30 elapsed time, 0:15:32 cpu time, factor 1.00)
- HOL-Imperative_HOL (0:09:22 elapsed time, 0:08:18 cpu time, factor 0.89)
- HOL-Datatype_Examples (0:08:12 elapsed time, 0:08:14 cpu time, factor 1.00)
- HOL-Real_Asymp (0:07:36 elapsed time, 0:07:40 cpu time, factor 1.01)
- HOL-Auth (0:07:31 elapsed time, 0:07:34 cpu time, factor 1.01)
- Codegen (0:07:01 elapsed time, 0:07:00 cpu time, factor 1.00)
- HOL-MicroJava (0:06:50 elapsed time, 0:06:54 cpu time, factor 1.01)
- HOL-Hoare_Parallel (0:06:17 elapsed time, 0:06:19 cpu time, factor 1.01)
- HOL-Computational_Algebra (0:06:16 elapsed time, 0:06:22 cpu time, factor 1.02)
- HOL-Predicate_Compile_Examples (0:05:44 elapsed time, 0:04:42 cpu time, factor 0.82)
- HOL-Bali (0:05:44 elapsed time, 0:05:49 cpu time, factor 1.01)
- HOL-IMP (0:05:33 elapsed time, 0:05:34 cpu time, factor 1.00)
- HOL-Number_Theory (0:05:23 elapsed time, 0:05:28 cpu time, factor 1.02)
- HOL-Examples (0:05:01 elapsed time, 0:05:03 cpu time, factor 1.01)
- HOL-SMT_Examples (0:03:14 elapsed time, 0:03:06 cpu time, factor 0.96)
- HOL-Quickcheck_Examples (0:03:10 elapsed time, 0:03:11 cpu time, factor 1.01)
- HOL-Nitpick_Examples (0:03:05 elapsed time, 0:02:20 cpu time, factor 0.76)
- HOL-SET_Protocol (0:02:37 elapsed time, 0:02:38 cpu time, factor 1.01)
- HOL-UNITY (0:02:30 elapsed time, 0:02:33 cpu time, factor 1.02)
- HOL-Record_Benchmark (0:02:28 elapsed time, 0:02:28 cpu time, factor 1.00)
- Datatypes (0:02:19 elapsed time, 0:02:17 cpu time, factor 0.99)
- Corec (0:01:50 elapsed time, 0:01:49 cpu time, factor 0.99)
- HOL-Metis_Examples (0:01:48 elapsed time, 0:01:30 cpu time, factor 0.83)
- HOL-Matrix_LP (0:01:21 elapsed time, 0:01:21 cpu time, factor 1.00)
- HOL-Combinatorics (0:01:21 elapsed time, 0:01:23 cpu time, factor 1.02)
- HOL-Hoare (0:01:19 elapsed time, 0:01:20 cpu time, factor 1.01)
- HOL-SPARK (0:01:16 elapsed time, 0:01:17 cpu time, factor 1.01)
- Tutorial (0:01:08 elapsed time, 0:01:05 cpu time, factor 0.96)
- HOL-Quotient_Examples (0:01:05 elapsed time, 0:00:52 cpu time, factor 0.80)
- Isar_Ref (0:01:04 elapsed time, 0:00:47 cpu time, factor 0.73)
- HOL-Cardinals (0:01:02 elapsed time, 0:01:03 cpu time, factor 1.02)
- HOLCF (0:01:01 elapsed time, 0:01:03 cpu time, factor 1.03)
- HOLCF-Library (0:00:51 elapsed time, 0:00:52 cpu time, factor 1.02)
- IOA (0:00:51 elapsed time, 0:00:52 cpu time, factor 1.02)
- HOL-Nonstandard_Analysis (0:00:48 elapsed time, 0:00:49 cpu time, factor 1.02)
- ZF (0:00:45 elapsed time, 0:00:48 cpu time, factor 1.07)
- HOL-Induct (0:00:40 elapsed time, 0:00:40 cpu time, factor 1.00)
- HOL-ZF (0:00:40 elapsed time, 0:00:41 cpu time, factor 1.03)
- HOL-Nominal (0:00:40 elapsed time, 0:00:40 cpu time, factor 1.00)
- HOL-SPARK-Examples (0:00:40 elapsed time, 0:00:41 cpu time, factor 1.03)
- ZF-Constructible (0:00:35 elapsed time, 0:00:37 cpu time, factor 1.06)
- HOL-Types_To_Sets (0:00:34 elapsed time, 0:00:34 cpu time, factor 1.00)
- System (0:00:34 elapsed time)
- Typeclass_Hierarchy (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00)
- HOL-Hahn_Banach (0:00:31 elapsed time, 0:00:30 cpu time, factor 0.97)
- HOL-TLA-Memory (0:00:31 elapsed time, 0:00:31 cpu time, factor 1.00)
- Pure (0:00:30 elapsed time, 0:00:30 cpu time, factor 1.00)
- ZF-UNITY (0:00:30 elapsed time, 0:00:31 cpu time, factor 1.03)
- HOL-Import (0:00:23 elapsed time, 0:00:23 cpu time, factor 1.00)
- HOL-Unix (0:00:23 elapsed time, 0:00:23 cpu time, factor 1.00)
- HOL-Eisbach (0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00)
- HOL-Statespace (0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00)
- HOLCF-Tutorial (0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00)
- HOL-Isar_Examples (0:00:18 elapsed time, 0:00:18 cpu time, factor 1.00)
- IOA-NTP (0:00:17 elapsed time, 0:00:17 cpu time, factor 1.00)
- ZF-ex (0:00:16 elapsed time, 0:00:17 cpu time, factor 1.06)
- HOL-NanoJava (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00)
- IOA-ABP (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.93)
- Implementation (0:00:15 elapsed time, 0:00:08 cpu time, factor 0.53)
- HOL-TLA (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)
- FOL-ex (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)
- Prog_Prove (0:00:14 elapsed time, 0:00:13 cpu time, factor 0.93)
- HOLCF-ex (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)
- CCL (0:00:14 elapsed time, 0:00:12 cpu time, factor 0.86)
- HOLCF-IMP (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)
- HOLCF-FOCUS (0:00:13 elapsed time, 0:00:13 cpu time, factor 1.00)
- ZF-Induct (0:00:12 elapsed time, 0:00:12 cpu time, factor 1.00)
- HOL-SPARK-Manual (0:00:12 elapsed time, 0:00:11 cpu time, factor 0.92)
- HOL-IMPP (0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00)
- HOL-TPTP (0:00:10 elapsed time, 0:00:10 cpu time, factor 1.00)
- JEdit (0:00:10 elapsed time)
- ZF-AC (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.10)
- FOLP-ex (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.00)
- FOL (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00)
- HOL-TLA-Inc (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00)
- Functions (0:00:07 elapsed time, 0:00:06 cpu time, factor 0.86)
- HOL-IOA (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00)
- HOL-Nonstandard_Analysis-Examples (0:00:06 elapsed time, 0:00:05 cpu time, factor 0.83)
- Sequents (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00)
- HOL-Lattice (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00)
- Tools (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00)
- Classes (0:00:05 elapsed time, 0:00:03 cpu time, factor 0.60)
- Locales (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.80)
- Eisbach (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00)
- HOL-Mirabelle-ex (0:00:05 elapsed time, 0:00:04 cpu time, factor 0.80)
- LCF (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00)
- ZF-Resid (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00)
- HOL-Mutabelle (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.75)
- CTT (0:00:04 elapsed time)
- IOA-ex (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.75)
- IOA-Storage (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00)
- Sugar (0:00:03 elapsed time)
- HOL-TLA-Buffer (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
- FOLP (0:00:03 elapsed time)
- ZF-Coind (0:00:02 elapsed time)
- Logics_ZF (0:00:02 elapsed time)
- How_to_Prove_it (0:00:02 elapsed time)
- ZF-IMP (0:00:02 elapsed time)
- HOL-Real_Asymp-Manual (0:00:02 elapsed time)
- Haskell (0:00:02 elapsed time)
- Main (0:00:02 elapsed time)
- HOL-Prolog (0:00:02 elapsed time)
- Demo_FoilTeX (0:00:01 elapsed time)
- Demo_LLNCS (0:00:01 elapsed time)
- Demo_LIPIcs (0:00:01 elapsed time)
- Pure-ex (0:00:01 elapsed time)
- Demo_Easychair (0:00:01 elapsed time)
- Cube (0:00:01 elapsed time)
- Demo_EPTCS (0:00:01 elapsed time)
- Pure-Examples (0:00:01 elapsed time)
- Logics (0:00:00 elapsed time)
- HOL (0:00:00 elapsed time)
- SML (0:00:00 elapsed time)
- Sledgehammer (0:00:00 elapsed time)
- HOL-Proofs (0:00:00 elapsed time)
- Nitpick (0:00:00 elapsed time)
- Intro (0:00:00 elapsed time)
- HOL-Datatype_Benchmark (0:00:00 elapsed time)
- HOL-Analysis (0:00:00 elapsed time)
- HOL-Algebra (0:00:00 elapsed time)
HOL-Quickcheck_Benchmark
- data:
- CSV
- timing:
- 0:40:57 elapsed time, 0:41:00 cpu time, factor 1.00
- ML timing:
- 2454.313s elapsed time, 2457.488s cpu time, 66.308s GC time, factor 1.00
- ML code maximum:
- 229.8 MiB
- ML code average:
- 167.2 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 1.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- c5131880e0a2




HOL-Data_Structures
- data:
- CSV
- timing:
- 0:31:52 elapsed time, 0:31:57 cpu time, factor 1.00
- ML timing:
- 1897.980s elapsed time, 1903.677s cpu time, 161.219s GC time, factor 1.00
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 5.6 MiB
- ML heap maximum:
- 3.6 GiB
- ML heap average:
- 2.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Codegenerator_Test
- data:
- CSV
- timing:
- 0:25:23 elapsed time, 0:20:07 cpu time, factor 0.79
- ML timing:
- 1515.055s elapsed time, 1198.747s cpu time, 181.934s GC time, factor 0.79
- ML code maximum:
- 3.6 MiB
- ML code average:
- 3.2 MiB
- ML stack maximum:
- 17 MiB
- ML stack average:
- 14.8 MiB
- ML heap maximum:
- 2 GiB
- ML heap average:
- 1.7 GiB
- Isabelle version:
- c5131880e0a2




HOL-Nominal-Examples
- data:
- CSV
- timing:
- 0:24:10 elapsed time, 0:24:10 cpu time, factor 1.00
- ML timing:
- 1439.477s elapsed time, 1439.118s cpu time, 155.198s GC time, factor 1.00
- ML stack maximum:
- 32.3 MiB
- ML stack average:
- 31.5 MiB
- ML heap maximum:
- 2.6 GiB
- ML heap average:
- 1.8 GiB
- Isabelle version:
- c5131880e0a2




HOL-ex
- data:
- CSV
- timing:
- 0:23:24 elapsed time, 0:23:01 cpu time, factor 0.98
- ML timing:
- 1396.560s elapsed time, 1373.802s cpu time, 108.199s GC time, factor 0.98
- ML code maximum:
- 4.2 MiB
- ML code average:
- 2.8 MiB
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.5 MiB
- ML heap maximum:
- 1.7 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- c5131880e0a2




HOL-Decision_Procs
- data:
- CSV
- timing:
- 0:20:52 elapsed time, 0:21:00 cpu time, factor 1.01
- ML timing:
- 1245.078s elapsed time, 1253.850s cpu time, 154.279s GC time, factor 1.01
- ML code maximum:
- 5.3 MiB
- ML code average:
- 3.2 MiB
- ML stack maximum:
- 32.3 MiB
- ML stack average:
- 17.1 MiB
- ML heap maximum:
- 2.9 GiB
- ML heap average:
- 2.1 GiB
- Isabelle version:
- c5131880e0a2




HOL-Library
- data:
- CSV
- timing:
- 0:20:09 elapsed time, 0:20:08 cpu time, factor 1.00
- ML timing:
- 1116.669s elapsed time, 1116.139s cpu time, 101.974s GC time, factor 1.00
- ML code maximum:
- 6 MiB
- ML code average:
- 4.1 MiB
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.7 MiB
- ML heap maximum:
- 2.6 GiB
- ML heap average:
- 1.9 GiB
- ML heap stored:
- 198.2 MiB
- Isabelle version:
- c5131880e0a2




HOL-Corec_Examples
- data:
- CSV
- timing:
- 0:15:30 elapsed time, 0:15:32 cpu time, factor 1.00
- ML timing:
- 906.460s elapsed time, 908.732s cpu time, 243.003s GC time, factor 1.00
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 3.5 GiB
- ML heap average:
- 2.2 GiB
- Isabelle version:
- c5131880e0a2




HOL-Imperative_HOL
- data:
- CSV
- timing:
- 0:09:22 elapsed time, 0:08:18 cpu time, factor 0.89
- ML timing:
- 557.862s elapsed time, 493.567s cpu time, 31.987s GC time, factor 0.88
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.2 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- c5131880e0a2




HOL-Datatype_Examples
- data:
- CSV
- timing:
- 0:08:12 elapsed time, 0:08:14 cpu time, factor 1.00
- ML timing:
- 478.260s elapsed time, 480.777s cpu time, 95.598s GC time, factor 1.01
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.2 MiB
- ML heap maximum:
- 2.7 GiB
- ML heap average:
- 1.7 GiB
- Isabelle version:
- c5131880e0a2




HOL-Real_Asymp
- data:
- CSV
- timing:
- 0:07:36 elapsed time, 0:07:40 cpu time, factor 1.01
- ML timing:
- 419.358s elapsed time, 423.841s cpu time, 24.428s GC time, factor 1.01
- ML code maximum:
- 3.8 MiB
- ML code average:
- 3.5 MiB
- ML stack maximum:
- 16.3 MiB
- ML stack average:
- 11.3 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 88.9 MiB
- Isabelle version:
- c5131880e0a2




HOL-Auth
- data:
- CSV
- timing:
- 0:07:31 elapsed time, 0:07:34 cpu time, factor 1.01
- ML timing:
- 433.992s elapsed time, 437.740s cpu time, 22.028s GC time, factor 1.01
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 41.8 MiB
- Isabelle version:
- bede03f6dc58




Codegen
- data:
- CSV
- timing:
- 0:07:01 elapsed time, 0:07:00 cpu time, factor 1.00
- ML timing:
- 416.794s elapsed time, 416.019s cpu time, 24.978s GC time, factor 1.00
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- bede03f6dc58




HOL-MicroJava
- data:
- CSV
- timing:
- 0:06:50 elapsed time, 0:06:54 cpu time, factor 1.01
- ML timing:
- 407.423s elapsed time, 411.315s cpu time, 11.936s GC time, factor 1.01
- ML code maximum:
- 1.5 MiB
- ML code average:
- 1.4 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 2.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Hoare_Parallel
- data:
- CSV
- timing:
- 0:06:17 elapsed time, 0:06:19 cpu time, factor 1.01
- ML timing:
- 374.040s elapsed time, 375.942s cpu time, 9.531s GC time, factor 1.01
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Computational_Algebra
- data:
- CSV
- timing:
- 0:06:16 elapsed time, 0:06:22 cpu time, factor 1.02
- ML timing:
- 349.181s elapsed time, 355.665s cpu time, 17.993s GC time, factor 1.02
- ML code maximum:
- 1.1 MiB
- ML stack maximum:
- 16.3 MiB
- ML stack average:
- 11.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 56.3 MiB
- Isabelle version:
- bede03f6dc58




HOL-Predicate_Compile_Examples
- data:
- CSV
- timing:
- 0:05:44 elapsed time, 0:04:42 cpu time, factor 0.82
- ML timing:
- 340.663s elapsed time, 278.579s cpu time, 10.680s GC time, factor 0.82
- ML code maximum:
- 7.7 MiB
- ML code average:
- 2.8 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Bali
- data:
- CSV
- timing:
- 0:05:44 elapsed time, 0:05:49 cpu time, factor 1.01
- ML timing:
- 339.959s elapsed time, 345.837s cpu time, 23.397s GC time, factor 1.02
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 5.4 MiB
- ML heap maximum:
- 2.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- bede03f6dc58




HOL-IMP
- data:
- CSV
- timing:
- 0:05:33 elapsed time, 0:05:34 cpu time, factor 1.00
- ML timing:
- 329.517s elapsed time, 330.570s cpu time, 16.700s GC time, factor 1.00
- ML code maximum:
- 12.4 MiB
- ML code average:
- 4.3 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 1.4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Number_Theory
- data:
- CSV
- timing:
- 0:05:23 elapsed time, 0:05:28 cpu time, factor 1.02
- ML timing:
- 319.850s elapsed time, 324.616s cpu time, 33.890s GC time, factor 1.01
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4.1 MiB
- ML heap maximum:
- 1.9 GiB
- ML heap average:
- 1.7 GiB
- Isabelle version:
- c5131880e0a2




HOL-Examples
- data:
- CSV
- timing:
- 0:05:01 elapsed time, 0:05:03 cpu time, factor 1.01
- ML timing:
- 296.633s elapsed time, 299.178s cpu time, 27.370s GC time, factor 1.01
- ML code maximum:
- 1.2 MiB
- ML stack maximum:
- 8.8 MiB
- ML stack average:
- 7.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- c5131880e0a2




HOL-SMT_Examples
- data:
- CSV
- timing:
- 0:03:14 elapsed time, 0:03:06 cpu time, factor 0.96
- ML timing:
- 192.146s elapsed time, 183.667s cpu time, 5.957s GC time, factor 0.96
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Quickcheck_Examples
- data:
- CSV
- timing:
- 0:03:10 elapsed time, 0:03:11 cpu time, factor 1.01
- ML timing:
- 187.358s elapsed time, 189.022s cpu time, 11.793s GC time, factor 1.01
- ML code maximum:
- 13.3 MiB
- ML code average:
- 6.1 MiB
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Nitpick_Examples
- data:
- CSV
- timing:
- 0:03:05 elapsed time, 0:02:20 cpu time, factor 0.76
- ML timing:
- 182.192s elapsed time, 137.123s cpu time, 2.727s GC time, factor 0.75
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-SET_Protocol
- data:
- CSV
- timing:
- 0:02:37 elapsed time, 0:02:38 cpu time, factor 1.01
- ML timing:
- 155.636s elapsed time, 156.433s cpu time, 3.868s GC time, factor 1.01
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-UNITY
- data:
- CSV
- timing:
- 0:02:30 elapsed time, 0:02:33 cpu time, factor 1.02
- ML timing:
- 147.509s elapsed time, 150.603s cpu time, 6.269s GC time, factor 1.02
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Record_Benchmark
- data:
- CSV
- timing:
- 0:02:28 elapsed time, 0:02:28 cpu time, factor 1.00
- ML timing:
- 144.405s elapsed time, 144.615s cpu time, 14.635s GC time, factor 1.00
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




Datatypes
- data:
- CSV
- timing:
- 0:02:19 elapsed time, 0:02:17 cpu time, factor 0.99
- ML timing:
- 102.297s elapsed time, 99.845s cpu time, 10.557s GC time, factor 0.98
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 5.6 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 95.5 MiB
- Isabelle version:
- bede03f6dc58




Corec
- data:
- CSV
- timing:
- 0:01:50 elapsed time, 0:01:49 cpu time, factor 0.99
- ML timing:
- 105.787s elapsed time, 104.095s cpu time, 8.677s GC time, factor 0.98
- ML code maximum:
- 2.9 MiB
- ML code average:
- 2.8 MiB
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- bede03f6dc58




HOL-Metis_Examples
- data:
- CSV
- timing:
- 0:01:48 elapsed time, 0:01:30 cpu time, factor 0.83
- ML timing:
- 105.962s elapsed time, 88.482s cpu time, 6.305s GC time, factor 0.84
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.5 GiB
- Isabelle version:
- c5131880e0a2




HOL-Matrix_LP
- data:
- CSV
- timing:
- 0:01:21 elapsed time, 0:01:21 cpu time, factor 1.00
- ML timing:
- 78.754s elapsed time, 79.095s cpu time, 3.782s GC time, factor 1.00
- ML code maximum:
- 1.3 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Combinatorics
- data:
- CSV
- timing:
- 0:01:21 elapsed time, 0:01:23 cpu time, factor 1.02
- ML timing:
- 78.753s elapsed time, 80.940s cpu time, 3.392s GC time, factor 1.03
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.6 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- bede03f6dc58




HOL-Hoare
- data:
- CSV
- timing:
- 0:01:19 elapsed time, 0:01:20 cpu time, factor 1.01
- ML timing:
- 77.488s elapsed time, 78.076s cpu time, 1.700s GC time, factor 1.01
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-SPARK
- data:
- CSV
- timing:
- 0:01:16 elapsed time, 0:01:17 cpu time, factor 1.01
- ML timing:
- 61.782s elapsed time, 62.780s cpu time, 2.346s GC time, factor 1.02
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 6.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- ML heap stored:
- 20.9 MiB
- Isabelle version:
- c5131880e0a2




Tutorial
- data:
- CSV
- timing:
- 0:01:08 elapsed time, 0:01:05 cpu time, factor 0.96
- ML timing:
- 65.065s elapsed time, 62.181s cpu time, 3.117s GC time, factor 0.96
- ML stack maximum:
- 2.5 MiB
- ML stack average:
- 2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Quotient_Examples
- data:
- CSV
- timing:
- 0:01:05 elapsed time, 0:00:52 cpu time, factor 0.80
- ML timing:
- 62.169s elapsed time, 49.569s cpu time, 2.058s GC time, factor 0.80
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




Isar_Ref
- data:
- CSV
- timing:
- 0:01:04 elapsed time, 0:00:47 cpu time, factor 0.73
- ML timing:
- 61.609s elapsed time, 45.342s cpu time, 3.438s GC time, factor 0.74
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 7.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Cardinals
- data:
- CSV
- timing:
- 0:01:02 elapsed time, 0:01:03 cpu time, factor 1.02
- ML timing:
- 60.701s elapsed time, 62.020s cpu time, 1.913s GC time, factor 1.02
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- bede03f6dc58




HOLCF
- data:
- CSV
- timing:
- 0:01:01 elapsed time, 0:01:03 cpu time, factor 1.03
- ML timing:
- 46.579s elapsed time, 48.507s cpu time, 3.889s GC time, factor 1.04
- ML code maximum:
- 1.3 MiB
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 26.1 MiB
- Isabelle version:
- c5131880e0a2




HOLCF-Library
- data:
- CSV
- timing:
- 0:00:51 elapsed time, 0:00:52 cpu time, factor 1.02
- ML timing:
- 37.489s elapsed time, 38.599s cpu time, 1.397s GC time, factor 1.03
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 13.9 MiB
- Isabelle version:
- c5131880e0a2




IOA
- data:
- CSV
- timing:
- 0:00:51 elapsed time, 0:00:52 cpu time, factor 1.02
- ML timing:
- 37.171s elapsed time, 38.145s cpu time, 1.360s GC time, factor 1.03
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 10 MiB
- Isabelle version:
- c5131880e0a2




HOL-Nonstandard_Analysis
- data:
- CSV
- timing:
- 0:00:48 elapsed time, 0:00:49 cpu time, factor 1.02
- ML timing:
- 32.623s elapsed time, 34.012s cpu time, 1.314s GC time, factor 1.04
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 2.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1008.7 MiB
- ML heap stored:
- 14.2 MiB
- Isabelle version:
- c5131880e0a2




ZF
- data:
- CSV
- timing:
- 0:00:45 elapsed time, 0:00:48 cpu time, factor 1.07
- ML timing:
- 42.907s elapsed time, 45.941s cpu time, 3.974s GC time, factor 1.07
- ML code maximum:
- 2.6 MiB
- ML code average:
- 2.1 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4.1 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.4 GiB
- ML heap stored:
- 18.4 MiB
- Isabelle version:
- c5131880e0a2




HOL-Induct
- data:
- CSV
- timing:
- 0:00:40 elapsed time, 0:00:40 cpu time, factor 1.00
- ML timing:
- 37.188s elapsed time, 37.756s cpu time, 2.097s GC time, factor 1.02
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-ZF
- data:
- CSV
- timing:
- 0:00:40 elapsed time, 0:00:41 cpu time, factor 1.03
- ML timing:
- 38.453s elapsed time, 39.812s cpu time, 1.725s GC time, factor 1.04
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Nominal
- data:
- CSV
- timing:
- 0:00:40 elapsed time, 0:00:40 cpu time, factor 1.00
- ML timing:
- 28.107s elapsed time, 28.524s cpu time, 1.144s GC time, factor 1.01
- ML code maximum:
- 2.5 MiB
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1 GiB
- ML heap stored:
- 13.6 MiB
- Isabelle version:
- c5131880e0a2




HOL-SPARK-Examples
- data:
- CSV
- timing:
- 0:00:40 elapsed time, 0:00:41 cpu time, factor 1.03
- ML timing:
- 38.591s elapsed time, 38.912s cpu time, 0.531s GC time, factor 1.01
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




ZF-Constructible
- data:
- CSV
- timing:
- 0:00:35 elapsed time, 0:00:37 cpu time, factor 1.06
- ML timing:
- 34.631s elapsed time, 36.379s cpu time, 6.658s GC time, factor 1.05
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.6 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Types_To_Sets
- data:
- CSV
- timing:
- 0:00:34 elapsed time, 0:00:34 cpu time, factor 1.00
- ML timing:
- 32.439s elapsed time, 32.945s cpu time, 1.178s GC time, factor 1.02
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.9 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




System
- data:
- CSV
- timing:
- 0:00:34 elapsed time
- ML timing:
- 33.572s elapsed time, 1.690s cpu time, 0.000s GC time, factor 0.05
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 700 MiB
- ML heap average:
- 378.7 MiB
- Isabelle version:
- c5131880e0a2




Typeclass_Hierarchy
- data:
- CSV
- timing:
- 0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00
- ML timing:
- 31.677s elapsed time, 31.529s cpu time, 1.375s GC time, factor 1.00
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Hahn_Banach
- data:
- CSV
- timing:
- 0:00:31 elapsed time, 0:00:30 cpu time, factor 0.97
- ML timing:
- 29.067s elapsed time, 28.694s cpu time, 1.240s GC time, factor 0.99
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-TLA-Memory
- data:
- CSV
- timing:
- 0:00:31 elapsed time, 0:00:31 cpu time, factor 1.00
- ML timing:
- 29.209s elapsed time, 29.523s cpu time, 0.549s GC time, factor 1.01
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




Pure
- data:
- CSV
- timing:
- 0:00:30 elapsed time, 0:00:30 cpu time, factor 1.00
- ML timing:
- 1.261s elapsed time, 1.274s cpu time, 0.000s GC time, factor 1.01
- ML code maximum:
- 24.6 MiB
- ML code average:
- 24.5 MiB
- ML stack maximum:
- 4 MiB
- ML stack average:
- 4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 668.5 MiB
- ML heap stored:
- 32.3 MiB
- Isabelle version:
- 35c8e7b00f71




ZF-UNITY
- data:
- CSV
- timing:
- 0:00:30 elapsed time, 0:00:31 cpu time, factor 1.03
- ML timing:
- 29.210s elapsed time, 30.339s cpu time, 1.098s GC time, factor 1.04
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Import
- data:
- CSV
- timing:
- 0:00:23 elapsed time, 0:00:23 cpu time, factor 1.00
- ML timing:
- 21.678s elapsed time, 21.764s cpu time, 0.696s GC time, factor 1.00
- ML stack maximum:
- 64.3 MiB
- ML stack average:
- 58.5 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Unix
- data:
- CSV
- timing:
- 0:00:23 elapsed time, 0:00:23 cpu time, factor 1.00
- ML timing:
- 21.023s elapsed time, 21.111s cpu time, 1.075s GC time, factor 1.00
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-Eisbach
- data:
- CSV
- timing:
- 0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00
- ML timing:
- 19.718s elapsed time, 20.171s cpu time, 0.511s GC time, factor 1.02
- ML code maximum:
- 2.6 MiB
- ML code average:
- 2.2 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.4 GiB
- Isabelle version:
- c5131880e0a2




HOL-Statespace
- data:
- CSV
- timing:
- 0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00
- ML timing:
- 19.270s elapsed time, 19.529s cpu time, 0.784s GC time, factor 1.01
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOLCF-Tutorial
- data:
- CSV
- timing:
- 0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00
- ML timing:
- 18.815s elapsed time, 19.037s cpu time, 0.593s GC time, factor 1.01
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




HOL-Isar_Examples
- data:
- CSV
- timing:
- 0:00:18 elapsed time, 0:00:18 cpu time, factor 1.00
- ML timing:
- 16.133s elapsed time, 15.994s cpu time, 0.602s GC time, factor 0.99
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




IOA-NTP
- data:
- CSV
- timing:
- 0:00:17 elapsed time, 0:00:17 cpu time, factor 1.00
- ML timing:
- 15.500s elapsed time, 15.699s cpu time, 0.638s GC time, factor 1.01
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




ZF-ex
- data:
- CSV
- timing:
- 0:00:16 elapsed time, 0:00:17 cpu time, factor 1.06
- ML timing:
- 15.550s elapsed time, 16.227s cpu time, 0.703s GC time, factor 1.04
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.3 GiB
- Isabelle version:
- c5131880e0a2




HOL-NanoJava
- data:
- CSV
- timing:
- 0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00
- ML timing:
- 13.734s elapsed time, 13.963s cpu time, 0.655s GC time, factor 1.02
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




IOA-ABP
- data:
- CSV
- timing:
- 0:00:15 elapsed time, 0:00:14 cpu time, factor 0.93
- ML timing:
- 12.797s elapsed time, 12.932s cpu time, 0.484s GC time, factor 1.01
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




Implementation
- data:
- CSV
- timing:
- 0:00:15 elapsed time, 0:00:08 cpu time, factor 0.53
- ML timing:
- 13.800s elapsed time, 7.024s cpu time, 0.047s GC time, factor 0.51
- ML code maximum:
- 1 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.7 MiB
- ML heap maximum:
- 1.3 GiB
- ML heap average:
- 749 MiB
- Isabelle version:
- c5131880e0a2




HOL-TLA
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00
- ML timing:
- 3.913s elapsed time, 4.178s cpu time, 0.117s GC time, factor 1.07
- ML stack maximum:
- 2.3 MiB
- ML heap maximum:
- 1 GiB
- ML heap average:
- 229.5 MiB
- ML heap stored:
- 5.1 MiB
- Isabelle version:
- c5131880e0a2




FOL-ex
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00
- ML timing:
- 13.424s elapsed time, 13.651s cpu time, 0.326s GC time, factor 1.02
- ML code maximum:
- 1.3 MiB
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- 35c8e7b00f71




Prog_Prove
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:13 cpu time, factor 0.93
- ML timing:
- 11.843s elapsed time, 11.765s cpu time, 0.611s GC time, factor 0.99
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




HOLCF-ex
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00
- ML timing:
- 12.178s elapsed time, 12.559s cpu time, 0.561s GC time, factor 1.03
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




CCL
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:12 cpu time, factor 0.86
- ML timing:
- 11.249s elapsed time, 11.217s cpu time, 0.886s GC time, factor 1.00
- ML code maximum:
- 2.2 MiB
- ML code average:
- 1.7 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1 GiB
- Isabelle version:
- 35c8e7b00f71




HOLCF-IMP
- data:
- CSV
- timing:
- 0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00
- ML timing:
- 12.294s elapsed time, 12.367s cpu time, 0.441s GC time, factor 1.01
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




HOLCF-FOCUS
- data:
- CSV
- timing:
- 0:00:13 elapsed time, 0:00:13 cpu time, factor 1.00
- ML timing:
- 11.364s elapsed time, 11.648s cpu time, 0.350s GC time, factor 1.02
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




ZF-Induct
- data:
- CSV
- timing:
- 0:00:12 elapsed time, 0:00:12 cpu time, factor 1.00
- ML timing:
- 10.543s elapsed time, 10.758s cpu time, 0.404s GC time, factor 1.02
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.8 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- ML heap stored:
- 5.6 MiB
- Isabelle version:
- c5131880e0a2




HOL-SPARK-Manual
- data:
- CSV
- timing:
- 0:00:12 elapsed time, 0:00:11 cpu time, factor 0.92
- ML timing:
- 10.124s elapsed time, 9.997s cpu time, 0.152s GC time, factor 0.99
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




HOL-IMPP
- data:
- CSV
- timing:
- 0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00
- ML timing:
- 9.361s elapsed time, 9.557s cpu time, 0.393s GC time, factor 1.02
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




HOL-TPTP
- data:
- CSV
- timing:
- 0:00:10 elapsed time, 0:00:10 cpu time, factor 1.00
- ML timing:
- 8.538s elapsed time, 8.802s cpu time, 0.655s GC time, factor 1.03
- ML code maximum:
- 6.2 MiB
- ML code average:
- 4.5 MiB
- ML stack maximum:
- 16.3 MiB
- ML stack average:
- 14.7 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




JEdit
- data:
- CSV
- timing:
- 0:00:10 elapsed time
- ML timing:
- 9.080s elapsed time, 1.083s cpu time, 0.000s GC time, factor 0.12
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.3 MiB
- ML heap maximum:
- 496 MiB
- ML heap average:
- 322.7 MiB
- Isabelle version:
- c5131880e0a2




ZF-AC
- data:
- CSV
- timing:
- 0:00:10 elapsed time, 0:00:11 cpu time, factor 1.10
- ML timing:
- 9.789s elapsed time, 10.403s cpu time, 0.547s GC time, factor 1.06
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.2 GiB
- Isabelle version:
- c5131880e0a2




FOLP-ex
- data:
- CSV
- timing:
- 0:00:08 elapsed time, 0:00:08 cpu time, factor 1.00
- ML timing:
- 7.781s elapsed time, 7.921s cpu time, 0.107s GC time, factor 1.02
- ML code maximum:
- 2 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- 35c8e7b00f71




FOL
- data:
- CSV
- timing:
- 0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00
- ML timing:
- 5.849s elapsed time, 5.471s cpu time, 0.175s GC time, factor 0.94
- ML code maximum:
- 1.9 MiB
- ML code average:
- 1.1 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 890.2 MiB
- ML heap stored:
- 5.1 MiB
- Isabelle version:
- 35c8e7b00f71




HOL-TLA-Inc
- data:
- CSV
- timing:
- 0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00
- ML timing:
- 5.286s elapsed time, 5.333s cpu time, 0.070s GC time, factor 1.01
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1016.7 MiB
- Isabelle version:
- c5131880e0a2




Functions
- data:
- CSV
- timing:
- 0:00:07 elapsed time, 0:00:06 cpu time, factor 0.86
- ML timing:
- 5.484s elapsed time, 5.277s cpu time, 0.269s GC time, factor 0.96
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 815.7 MiB
- Isabelle version:
- bede03f6dc58




HOL-IOA
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00
- ML timing:
- 5.053s elapsed time, 5.159s cpu time, 0.122s GC time, factor 1.02
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 840.2 MiB
- Isabelle version:
- c5131880e0a2




HOL-Nonstandard_Analysis-Examples
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:05 cpu time, factor 0.83
- ML timing:
- 3.635s elapsed time, 3.676s cpu time, 0.099s GC time, factor 1.01
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 1.4 GiB
- ML heap average:
- 869 MiB
- Isabelle version:
- c5131880e0a2




Sequents
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00
- ML timing:
- 5.747s elapsed time, 5.998s cpu time, 0.107s GC time, factor 1.04
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




HOL-Lattice
- data:
- CSV
- timing:
- 0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00
- ML timing:
- 4.570s elapsed time, 4.845s cpu time, 0.119s GC time, factor 1.06
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.1 MiB
- ML heap maximum:
- 1 GiB
- ML heap average:
- 700.5 MiB
- Isabelle version:
- c5131880e0a2




- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00
- ML timing:
- 4.730s elapsed time, 4.842s cpu time, 0.229s GC time, factor 1.02
- ML code maximum:
- 2.7 MiB
- ML code average:
- 1.5 MiB
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.1 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 1.1 GiB
- Isabelle version:
- c5131880e0a2




Classes
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:03 cpu time, factor 0.60
- ML timing:
- 3.780s elapsed time, 2.306s cpu time, 0.077s GC time, factor 0.61
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.1 MiB
- ML heap maximum:
- 758 MiB
- ML heap average:
- 352 MiB
- Isabelle version:
- bede03f6dc58




Locales
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:04 cpu time, factor 0.80
- ML timing:
- 3.747s elapsed time, 3.207s cpu time, 0.112s GC time, factor 0.86
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 761 MiB
- ML heap average:
- 616.7 MiB
- Isabelle version:
- c5131880e0a2




Eisbach
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00
- ML timing:
- 3.710s elapsed time, 3.426s cpu time, 0.017s GC time, factor 0.92
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 2.3 MiB
- ML heap maximum:
- 956 MiB
- ML heap average:
- 763.1 MiB
- Isabelle version:
- bede03f6dc58




HOL-Mirabelle-ex
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:04 cpu time, factor 0.80
- ML timing:
- 3.266s elapsed time, 3.347s cpu time, 0.065s GC time, factor 1.02
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.3 MiB
- ML heap maximum:
- 756 MiB
- ML heap average:
- 569 MiB
- Isabelle version:
- c5131880e0a2




LCF
- data:
- CSV
- timing:
- 0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00
- ML timing:
- 4.579s elapsed time, 4.847s cpu time, 0.150s GC time, factor 1.06
- ML code maximum:
- 1.9 MiB
- ML code average:
- 1 MiB
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 3 MiB
- ML heap maximum:
- 1.5 GiB
- ML heap average:
- 989.4 MiB
- Isabelle version:
- c5131880e0a2




ZF-Resid
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00
- ML timing:
- 3.127s elapsed time, 3.272s cpu time, 0.063s GC time, factor 1.05
- ML heap maximum:
- 1.1 GiB
- ML heap average:
- 736.7 MiB
- Isabelle version:
- c5131880e0a2




HOL-Mutabelle
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:03 cpu time, factor 0.75
- ML timing:
- 2.208s elapsed time, 2.265s cpu time, 0.124s GC time, factor 1.03
- ML stack maximum:
- 8.3 MiB
- ML stack average:
- 8.3 MiB
- ML heap maximum:
- 763 MiB
- ML heap average:
- 619.5 MiB
- Isabelle version:
- c5131880e0a2




CTT
- data:
- CSV
- timing:
- 0:00:04 elapsed time
- ML timing:
- 2.293s elapsed time, 2.318s cpu time, 0.114s GC time, factor 1.01
- ML stack maximum:
- 2.3 MiB
- ML stack average:
- 1.5 MiB
- ML heap maximum:
- 763 MiB
- ML heap average:
- 312.6 MiB
- Isabelle version:
- 35c8e7b00f71




IOA-ex
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:03 cpu time, factor 0.75
- ML timing:
- 2.321s elapsed time, 2.352s cpu time, 0.090s GC time, factor 1.01
- ML heap maximum:
- 739 MiB
- ML heap average:
- 392.7 MiB
- Isabelle version:
- c5131880e0a2




IOA-Storage
- data:
- CSV
- timing:
- 0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00
- ML timing:
- 2.842s elapsed time, 2.868s cpu time, 0.083s GC time, factor 1.01
- ML heap maximum:
- 757 MiB
- ML heap average:
- 547.9 MiB
- Isabelle version:
- c5131880e0a2




Sugar
- data:
- CSV
- timing:
- 0:00:03 elapsed time
- ML timing:
- 1.486s elapsed time, 1.425s cpu time, 0.000s GC time, factor 0.96
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1 MiB
- ML heap maximum:
- 609 MiB
- ML heap average:
- 449.5 MiB
- Isabelle version:
- c5131880e0a2




HOL-TLA-Buffer
- data:
- CSV
- timing:
- 0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00
- ML timing:
- 1.563s elapsed time, 1.593s cpu time, 0.000s GC time, factor 1.02
- ML heap maximum:
- 718 MiB
- ML heap average:
- 365.6 MiB
- Isabelle version:
- c5131880e0a2




FOLP
- data:
- CSV
- timing:
- 0:00:03 elapsed time
- ML timing:
- 1.925s elapsed time, 2.000s cpu time, 0.100s GC time, factor 1.04
- ML stack maximum:
- 1.3 MiB
- ML stack average:
- 1.1 MiB
- ML heap maximum:
- 762 MiB
- ML heap average:
- 413.6 MiB
- ML heap stored:
- 2.4 MiB
- Isabelle version:
- 35c8e7b00f71




ZF-Coind
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.566s elapsed time, 1.646s cpu time, 0.066s GC time, factor 1.05
- ML heap maximum:
- 757 MiB
- ML heap average:
- 556.3 MiB
- Isabelle version:
- c5131880e0a2




Logics_ZF
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.900s elapsed time, 0.767s cpu time, 0.000s GC time, factor 0.85
- ML heap maximum:
- 462 MiB
- ML heap average:
- 184.2 MiB
- Isabelle version:
- c5131880e0a2




How_to_Prove_it
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.633s elapsed time, 0.643s cpu time, 0.000s GC time, factor 1.02
- ML heap maximum:
- 295 MiB
- ML heap average:
- 295 MiB
- Isabelle version:
- c5131880e0a2




ZF-IMP
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.673s elapsed time, 1.718s cpu time, 0.052s GC time, factor 1.03
- ML heap maximum:
- 756 MiB
- ML heap average:
- 552.2 MiB
- Isabelle version:
- c5131880e0a2




HOL-Real_Asymp-Manual
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.742s elapsed time, 0.761s cpu time, 0.000s GC time, factor 1.03
- ML heap maximum:
- 336 MiB
- ML heap average:
- 336 MiB
- Isabelle version:
- c5131880e0a2




Haskell
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.683s elapsed time, 0.700s cpu time, 0.000s GC time, factor 1.02
- ML stack maximum:
- 4.3 MiB
- ML stack average:
- 4.3 MiB
- ML heap maximum:
- 361 MiB
- ML heap average:
- 361 MiB
- Isabelle version:
- c5131880e0a2




Main
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 1.183s elapsed time, 1.286s cpu time, 0.000s GC time, factor 1.09
- ML stack maximum:
- 1.3 MiB
- ML heap maximum:
- 547 MiB
- ML heap average:
- 287.3 MiB
- Isabelle version:
- c5131880e0a2




HOL-Prolog
- data:
- CSV
- timing:
- 0:00:02 elapsed time
- ML timing:
- 0.648s elapsed time, 0.697s cpu time, 0.000s GC time, factor 1.08
- ML heap maximum:
- 380 MiB
- ML heap average:
- 380 MiB
- Isabelle version:
- c5131880e0a2




Demo_FoilTeX
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.313s elapsed time, 0.321s cpu time, 0.000s GC time, factor 1.03
- ML heap maximum:
- 45 MiB
- ML heap average:
- 3 MiB
- Isabelle version:
- bede03f6dc58




Demo_LLNCS
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.329s elapsed time, 0.294s cpu time, 0.000s GC time, factor 0.89
- ML heap maximum:
- 59 MiB
- ML heap average:
- 59 MiB
- Isabelle version:
- bede03f6dc58




Demo_LIPIcs
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.342s elapsed time, 0.303s cpu time, 0.000s GC time, factor 0.89
- ML heap maximum:
- 54 MiB
- ML heap average:
- 54 MiB
- Isabelle version:
- bede03f6dc58




Pure-ex
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.948s elapsed time, 0.899s cpu time, 0.000s GC time, factor 0.95
- ML heap maximum:
- 407 MiB
- ML heap average:
- 296.4 MiB
- Isabelle version:
- c5131880e0a2




Demo_Easychair
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.344s elapsed time, 0.299s cpu time, 0.000s GC time, factor 0.87
- ML heap maximum:
- 51 MiB
- ML heap average:
- 51 MiB
- Isabelle version:
- bede03f6dc58




Cube
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.726s elapsed time, 0.669s cpu time, 0.000s GC time, factor 0.92
- ML heap maximum:
- 236 MiB
- ML heap average:
- 236 MiB
- Isabelle version:
- 35c8e7b00f71




Demo_EPTCS
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.355s elapsed time, 0.315s cpu time, 0.000s GC time, factor 0.89
- ML heap maximum:
- 43 MiB
- ML heap average:
- 3 MiB
- Isabelle version:
- bede03f6dc58




Pure-Examples
- data:
- CSV
- timing:
- 0:00:01 elapsed time
- ML timing:
- 0.782s elapsed time, 0.756s cpu time, 0.000s GC time, factor 0.97
- ML heap maximum:
- 194 MiB
- ML heap average:
- 98.5 MiB
- Isabelle version:
- c5131880e0a2




Logics
- data:
- CSV
- Isabelle version:
- c5131880e0a2

HOL
- data:
- CSV
- Isabelle version:
- 35c8e7b00f71


SML
- data:
- CSV
- ML timing:
- 0.020s elapsed time, 0.023s cpu time, 0.000s GC time, factor 1.15
- ML heap maximum:
- 24 MiB
- ML heap average:
- 24 MiB
- Isabelle version:
- c5131880e0a2




Sledgehammer
- data:
- CSV
- ML heap maximum:
- 3 MiB
- ML heap average:
- 3 MiB
- Isabelle version:
- c5131880e0a2



HOL-Proofs
- data:
- CSV
- Isabelle version:
- 35c8e7b00f71
Nitpick
- data:
- CSV
- ML heap maximum:
- 3 MiB
- ML heap average:
- 3 MiB
- Isabelle version:
- c5131880e0a2



Intro
- data:
- CSV
- Isabelle version:
- c5131880e0a2

HOL-Datatype_Benchmark
- data:
- CSV
- Isabelle version:
- c5131880e0a2
HOL-Analysis
- data:
- CSV
- Isabelle version:
- bede03f6dc58
HOL-Algebra
- data:
- CSV
- Isabelle version:
- bede03f6dc58

