Isabelle build status for jenkins isabelle-nightly-benchmark, 6 threads

status date:
23-Aug-2019 20:26:08 +0200
build host:
workermta1.mta_big

HOL-Datatype_Benchmark

data:
CSV
timing:
0:08:31 elapsed time, 0:34:09 cpu time, factor 4.01
ML timing:
0:08:29 elapsed time, 0:46:48 cpu time, factor 5.51
stack maximum:
12 M
stack average:
10 M
heap maximum:
8191 M
heap average:
6710 M
Isabelle version:
b85a12c2e2bf

HOL-Analysis

data:
CSV
timing:
0:07:05 elapsed time, 0:32:44 cpu time, factor 4.62
ML timing:
0:05:57 elapsed time, 0:32:07 cpu time, factor 5.39
code maximum:
1 M
stack maximum:
100 M
stack average:
84 M
heap maximum:
8159 M
heap average:
7716 M
Isabelle version:
b85a12c2e2bf

HOL-Proofs

data:
CSV
timing:
0:06:59 elapsed time, 0:12:23 cpu time, factor 1.77
ML timing:
0:05:13 elapsed time, 0:09:52 cpu time, factor 1.89
code maximum:
29 M
code average:
15 M
stack maximum:
79 M
stack average:
52 M
heap maximum:
8155 M
heap average:
6742 M
Isabelle version:
b85a12c2e2bf

HOL-Quickcheck_Benchmark

data:
CSV
timing:
0:05:11 elapsed time, 0:25:32 cpu time, factor 4.93
ML timing:
0:05:09 elapsed time, 0:27:01 cpu time, factor 5.23
code maximum:
182 M
code average:
116 M
stack maximum:
15 M
stack average:
11 M
heap maximum:
3999 M
heap average:
3907 M
Isabelle version:
b85a12c2e2bf

HOL-Decision_Procs

data:
CSV
timing:
0:04:08 elapsed time, 0:18:53 cpu time, factor 4.57
ML timing:
0:04:05 elapsed time, 0:21:18 cpu time, factor 5.20
code maximum:
4 M
stack maximum:
106 M
stack average:
69 M
heap maximum:
8317 M
heap average:
7501 M
Isabelle version:
b85a12c2e2bf

HOL-ex

data:
CSV
timing:
0:04:00 elapsed time, 0:19:40 cpu time, factor 4.92
ML timing:
0:03:58 elapsed time, 0:19:05 cpu time, factor 4.81
code maximum:
5 M
code average:
3 M
stack maximum:
90 M
stack average:
49 M
heap maximum:
8172 M
heap average:
7609 M
Isabelle version:
b85a12c2e2bf

HOL

data:
CSV
timing:
0:03:54 elapsed time, 0:12:36 cpu time, factor 3.23
ML timing:
0:03:15 elapsed time, 0:12:04 cpu time, factor 3.70
code maximum:
32 M
code average:
21 M
stack maximum:
99 M
stack average:
55 M
heap maximum:
3997 M
heap average:
3931 M
Isabelle version:
b85a12c2e2bf

HOL-Nominal-Examples

data:
CSV
timing:
0:03:52 elapsed time, 0:18:12 cpu time, factor 4.71
ML timing:
0:03:50 elapsed time, 0:19:39 cpu time, factor 5.11
stack maximum:
40 M
stack average:
26 M
heap maximum:
8161 M
heap average:
7434 M
Isabelle version:
b85a12c2e2bf

HOL-Data_Structures

data:
CSV
timing:
0:03:03 elapsed time, 0:17:13 cpu time, factor 5.64
ML timing:
0:03:02 elapsed time, 0:18:06 cpu time, factor 5.96
stack maximum:
13 M
stack average:
10 M
heap maximum:
8167 M
heap average:
7324 M
Isabelle version:
b85a12c2e2bf

HOL-Algebra

data:
CSV
timing:
0:02:38 elapsed time, 0:10:40 cpu time, factor 4.05
ML timing:
0:01:58 elapsed time, 0:10:42 cpu time, factor 5.44
stack maximum:
28 M
stack average:
23 M
heap maximum:
6654 M
heap average:
4291 M
Isabelle version:
b85a12c2e2bf

HOL-Corec_Examples

data:
CSV
timing:
0:02:31 elapsed time, 0:08:02 cpu time, factor 3.19
ML timing:
0:02:29 elapsed time, 0:08:49 cpu time, factor 3.53
stack maximum:
3 M
stack average:
2 M
heap maximum:
7935 M
heap average:
6700 M
Isabelle version:
b85a12c2e2bf

HOL-Record_Benchmark

data:
CSV
timing:
0:02:30 elapsed time, 0:03:42 cpu time, factor 1.48
ML timing:
0:02:29 elapsed time, 0:03:50 cpu time, factor 1.55
stack maximum:
9 M
stack average:
5 M
heap maximum:
3996 M
heap average:
3773 M
Isabelle version:
b85a12c2e2bf

HOL-Library

data:
CSV
timing:
0:02:05 elapsed time, 0:09:38 cpu time, factor 4.62
ML timing:
0:01:27 elapsed time, 0:08:19 cpu time, factor 5.74
code maximum:
3 M
code average:
2 M
stack maximum:
43 M
stack average:
32 M
heap maximum:
8151 M
heap average:
6334 M
Isabelle version:
b85a12c2e2bf

HOL-Proofs-Lambda

data:
CSV
timing:
0:01:42 elapsed time, 0:02:02 cpu time, factor 1.20
ML timing:
0:01:40 elapsed time, 0:02:09 cpu time, factor 1.28
stack maximum:
5 M
stack average:
2 M
heap maximum:
5353 M
heap average:
4058 M
Isabelle version:
b85a12c2e2bf

HOL-Probability

data:
CSV
timing:
0:01:30 elapsed time, 0:06:38 cpu time, factor 4.42
ML timing:
0:01:05 elapsed time, 0:05:28 cpu time, factor 4.99
stack maximum:
29 M
stack average:
27 M
heap maximum:
7382 M
heap average:
5527 M
Isabelle version:
b85a12c2e2bf

HOL-Proofs-Extraction

data:
CSV
timing:
0:01:29 elapsed time, 0:02:41 cpu time, factor 1.81
ML timing:
0:01:28 elapsed time, 0:02:50 cpu time, factor 1.93
stack maximum:
14 M
stack average:
9 M
heap maximum:
3999 M
heap average:
3924 M
Isabelle version:
b85a12c2e2bf

HOL-Auth

data:
CSV
timing:
0:01:26 elapsed time, 0:05:57 cpu time, factor 4.15
ML timing:
0:01:08 elapsed time, 0:05:30 cpu time, factor 4.81
stack maximum:
20 M
stack average:
16 M
heap maximum:
3995 M
heap average:
3862 M
Isabelle version:
b85a12c2e2bf

HOL-Homology

data:
CSV
timing:
0:01:22 elapsed time, 0:06:21 cpu time, factor 4.65
ML timing:
0:01:20 elapsed time, 0:06:40 cpu time, factor 4.98
stack maximum:
21 M
stack average:
16 M
heap maximum:
3997 M
heap average:
3940 M
Isabelle version:
b85a12c2e2bf

HOL-Datatype_Examples

data:
CSV
timing:
0:01:17 elapsed time, 0:05:32 cpu time, factor 4.31
ML timing:
0:01:15 elapsed time, 0:06:08 cpu time, factor 4.88
stack maximum:
5 M
stack average:
4 M
heap maximum:
7895 M
heap average:
6077 M
Isabelle version:
b85a12c2e2bf

HOL-Quickcheck_Examples

data:
CSV
timing:
0:01:15 elapsed time, 0:04:36 cpu time, factor 3.68
ML timing:
0:01:14 elapsed time, 0:02:56 cpu time, factor 2.37
code maximum:
14 M
code average:
11 M
stack maximum:
20 M
stack average:
17 M
heap maximum:
3993 M
heap average:
3955 M
Isabelle version:
b85a12c2e2bf

HOL-Number_Theory

data:
CSV
timing:
0:01:11 elapsed time, 0:04:43 cpu time, factor 3.99
ML timing:
0:00:49 elapsed time, 0:04:08 cpu time, factor 5.05
stack maximum:
11 M
stack average:
8 M
heap maximum:
3997 M
heap average:
3896 M
Isabelle version:
b85a12c2e2bf

HOL-MicroJava

data:
CSV
timing:
0:01:05 elapsed time, 0:04:49 cpu time, factor 4.45
ML timing:
0:01:03 elapsed time, 0:04:59 cpu time, factor 4.70
code maximum:
1 M
stack maximum:
22 M
stack average:
16 M
heap maximum:
3997 M
heap average:
3921 M
Isabelle version:
b85a12c2e2bf

HOL-Computational_Algebra

data:
CSV
timing:
0:01:05 elapsed time, 0:03:28 cpu time, factor 3.20
ML timing:
0:00:48 elapsed time, 0:03:00 cpu time, factor 3.74
code maximum:
11 M
code average:
2 M
stack maximum:
35 M
stack average:
21 M
heap maximum:
3994 M
heap average:
3889 M
Isabelle version:
b85a12c2e2bf

HOL-Hoare_Parallel

data:
CSV
timing:
0:01:04 elapsed time, 0:05:35 cpu time, factor 5.23
ML timing:
0:01:03 elapsed time, 0:05:42 cpu time, factor 5.43
stack maximum:
7 M
stack average:
5 M
heap maximum:
3998 M
heap average:
3937 M
Isabelle version:
b85a12c2e2bf

HOL-Bali

data:
CSV
timing:
0:00:59 elapsed time, 0:03:41 cpu time, factor 3.75
ML timing:
0:00:58 elapsed time, 0:03:52 cpu time, factor 3.98
stack maximum:
19 M
stack average:
10 M
heap maximum:
3991 M
heap average:
3757 M
Isabelle version:
b85a12c2e2bf

HOL-IMP

data:
CSV
timing:
0:00:58 elapsed time, 0:04:45 cpu time, factor 4.91
ML timing:
0:00:56 elapsed time, 0:04:59 cpu time, factor 5.30
code maximum:
11 M
code average:
4 M
stack maximum:
34 M
stack average:
14 M
heap maximum:
7977 M
heap average:
6003 M
Isabelle version:
b85a12c2e2bf

HOL-Word-SMT_Examples

data:
CSV
timing:
0:00:57 elapsed time, 0:01:27 cpu time, factor 1.53
ML timing:
0:00:56 elapsed time, 0:01:24 cpu time, factor 1.50
stack maximum:
5 M
stack average:
4 M
heap maximum:
3998 M
heap average:
3927 M
Isabelle version:
b85a12c2e2bf

HOL-Predicate_Compile_Examples

data:
CSV
timing:
0:00:51 elapsed time, 0:06:16 cpu time, factor 7.37
ML timing:
0:00:49 elapsed time, 0:03:37 cpu time, factor 4.39
code maximum:
4 M
code average:
2 M
stack maximum:
21 M
stack average:
16 M
heap maximum:
7511 M
heap average:
6016 M
Isabelle version:
b85a12c2e2bf

HOL-Imperative_HOL

data:
CSV
timing:
0:00:36 elapsed time, 0:05:58 cpu time, factor 9.94
ML timing:
0:00:35 elapsed time, 0:01:24 cpu time, factor 2.38
stack maximum:
8 M
stack average:
6 M
heap maximum:
3991 M
heap average:
3902 M
Isabelle version:
b85a12c2e2bf

HOL-Quotient_Examples

data:
CSV
timing:
0:00:29 elapsed time, 0:01:50 cpu time, factor 3.79
ML timing:
0:00:27 elapsed time, 0:00:48 cpu time, factor 1.75
stack maximum:
5 M
stack average:
4 M
heap maximum:
3972 M
heap average:
3832 M
Isabelle version:
b85a12c2e2bf

HOL-SET_Protocol

data:
CSV
timing:
0:00:25 elapsed time, 0:01:50 cpu time, factor 4.40
ML timing:
0:00:24 elapsed time, 0:01:51 cpu time, factor 4.61
stack maximum:
7 M
stack average:
5 M
heap maximum:
3996 M
heap average:
3605 M
Isabelle version:
b85a12c2e2bf

HOL-UNITY

data:
CSV
timing:
0:00:22 elapsed time, 0:01:49 cpu time, factor 4.95
ML timing:
0:00:21 elapsed time, 0:01:51 cpu time, factor 5.31
stack maximum:
9 M
stack average:
7 M
heap maximum:
3983 M
heap average:
3808 M
Isabelle version:
b85a12c2e2bf

HOLCF

data:
CSV
timing:
0:00:21 elapsed time, 0:00:58 cpu time, factor 2.76
ML timing:
0:00:12 elapsed time, 0:00:43 cpu time, factor 3.46
stack maximum:
7 M
stack average:
4 M
heap maximum:
3942 M
heap average:
3418 M
Isabelle version:
b85a12c2e2bf

HOL-Word

data:
CSV
timing:
0:00:19 elapsed time, 0:01:10 cpu time, factor 3.68
ML timing:
0:00:10 elapsed time, 0:00:54 cpu time, factor 5.48
stack maximum:
15 M
stack average:
12 M
heap maximum:
3972 M
heap average:
3673 M
Isabelle version:
b85a12c2e2bf

HOL-Nonstandard_Analysis

data:
CSV
timing:
0:00:19 elapsed time, 0:00:55 cpu time, factor 2.89
ML timing:
0:00:06 elapsed time, 0:00:32 cpu time, factor 4.67
stack maximum:
7 M
stack average:
3 M
heap maximum:
3978 M
heap average:
2763 M
Isabelle version:
b85a12c2e2bf

HOL-Nominal

data:
CSV
timing:
0:00:17 elapsed time, 0:00:36 cpu time, factor 2.12
ML timing:
0:00:06 elapsed time, 0:00:15 cpu time, factor 2.43
code maximum:
1 M
stack maximum:
5 M
stack average:
4 M
heap maximum:
3964 M
heap average:
2476 M
Isabelle version:
b85a12c2e2bf

HOL-Metis_Examples

data:
CSV
timing:
0:00:14 elapsed time, 0:01:16 cpu time, factor 5.43
ML timing:
0:00:13 elapsed time, 0:01:01 cpu time, factor 4.68
stack maximum:
10 M
stack average:
8 M
heap maximum:
3991 M
heap average:
3795 M
Isabelle version:
b85a12c2e2bf

ZF

data:
CSV
timing:
0:00:14 elapsed time, 0:00:50 cpu time, factor 3.57
ML timing:
0:00:12 elapsed time, 0:00:49 cpu time, factor 3.94
code maximum:
2 M
code average:
1 M
stack maximum:
13 M
stack average:
7 M
heap maximum:
3956 M
heap average:
3136 M
Isabelle version:
b85a12c2e2bf

HOL-Probability-ex

data:
CSV
timing:
0:00:09 elapsed time, 0:00:25 cpu time, factor 2.78
ML timing:
0:00:07 elapsed time, 0:00:24 cpu time, factor 3.44
stack maximum:
11 M
stack average:
4 M
heap maximum:
3978 M
heap average:
3473 M
Isabelle version:
b85a12c2e2bf

HOL-Cardinals

data:
CSV
timing:
0:00:08 elapsed time, 0:00:44 cpu time, factor 5.50
ML timing:
0:00:07 elapsed time, 0:00:45 cpu time, factor 5.91
stack maximum:
11 M
stack average:
9 M
heap maximum:
3981 M
heap average:
3550 M
Isabelle version:
b85a12c2e2bf

IOA

data:
CSV
timing:
0:00:08 elapsed time, 0:00:32 cpu time, factor 4.00
ML timing:
0:00:06 elapsed time, 0:00:32 cpu time, factor 4.70
stack maximum:
5 M
stack average:
3 M
heap maximum:
3979 M
heap average:
3034 M
Isabelle version:
b85a12c2e2bf

ZF-UNITY

data:
CSV
timing:
0:00:06 elapsed time, 0:00:33 cpu time, factor 5.50
ML timing:
0:00:06 elapsed time, 0:00:34 cpu time, factor 5.51
stack maximum:
6 M
stack average:
5 M
heap maximum:
3987 M
heap average:
3412 M
Isabelle version:
b85a12c2e2bf

ZF-Induct

data:
CSV
timing:
0:00:05 elapsed time, 0:00:15 cpu time, factor 3.00
ML timing:
0:00:03 elapsed time, 0:00:13 cpu time, factor 3.71
stack maximum:
4 M
stack average:
3 M
heap maximum:
3976 M
heap average:
2783 M
Isabelle version:
b85a12c2e2bf

HOL-Nonstandard_Analysis-Examples

data:
CSV
timing:
0:00:03 elapsed time, 0:00:05 cpu time, factor 1.67
ML timing:
0:00:01 elapsed time, 0:00:03 cpu time
stack maximum:
1 M
stack average:
1 M
heap maximum:
1377 M
heap average:
1122 M
Isabelle version:
b85a12c2e2bf