Job 2352

CakeML:161705be9f34e5350a0c86b92b50e2b36d9cabf0
  Merge pull request #987 from CakeML/rup [Mar 21 10:13:15]
HOL:671b4b712f9e860a558393b4b0c6a15e3a52a754
  Updated HOL Description with higher mathematics contents promoted to  [Mar 18 23:15:32]
Machine:lammmington
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Mar 22 15:00:16 Claimed job
Mar 22 15:00:21 Building HOL
Mar 22 15:14:29 Starting developers
Mar 22 15:14:33 Finished developers                                               2s 219MB
Mar 22 15:14:34 Starting developers/bin
Mar 22 15:14:52 Finished developers/bin                                          17s   1GB
Mar 22 15:14:53 Starting compiler/proofs
Mar 22 17:05:14 Finished compiler/proofs                                    1h50m19s  41GB
Mar 22 17:05:15 Starting compiler/bootstrap/translation
Mar 23 01:08:50 Finished compiler/bootstrap/translation                     8h03m33s  84GB
Mar 23 01:08:51 Starting semantics/ffi
Mar 23 01:08:59 Finished semantics/ffi                                            7s 674MB
Mar 23 01:09:00 Starting semantics
Mar 23 01:09:01 Finished semantics                                                0s  66MB
Mar 23 01:09:02 Starting semantics/proofs
Mar 23 01:09:37 Finished semantics/proofs                                        33s   2GB
Mar 23 01:09:38 Starting semantics/alt_semantics
Mar 23 01:10:16 Finished semantics/alt_semantics                                 37s   1GB
Mar 23 01:10:17 Starting semantics/alt_semantics/proofs
Mar 23 01:21:20 Finished semantics/alt_semantics/proofs                       11m01s   5GB
Mar 23 01:21:20 Starting basis/pure
Mar 23 01:21:22 Finished basis/pure                                               0s  68MB
Mar 23 01:21:23 Starting translator
Mar 23 01:23:04 Finished translator                                            1m40s   3GB
Mar 23 01:23:05 Starting compiler/parsing
Mar 23 01:23:06 Finished compiler/parsing                                         0s  73MB
Mar 23 01:23:07 Starting characteristic
Mar 23 01:23:09 Finished characteristic                                           0s  88MB
Mar 23 01:23:10 Starting translator/monadic
Mar 23 01:23:11 Finished translator/monadic                                       0s  98MB
Mar 23 01:23:12 Starting basis
Mar 23 01:26:50 Finished basis                                                 3m37s   5GB
Mar 23 01:26:51 Starting compiler/inference
Mar 23 01:26:53 Finished compiler/inference                                       0s  83MB
Mar 23 01:26:54 Starting compiler/backend/reg_alloc
Mar 23 01:26:55 Finished compiler/backend/reg_alloc                               0s  65MB
Mar 23 01:26:56 Starting compiler/backend/gc
Mar 23 01:26:58 Finished compiler/backend/gc                                      0s 133MB
Mar 23 01:26:59 Starting compiler/backend
Mar 23 01:27:16 Finished compiler/backend                                        16s   1GB
Mar 23 01:27:17 Starting compiler/encoders/asm
Mar 23 01:27:19 Finished compiler/encoders/asm                                    0s  95MB
Mar 23 01:27:20 Starting compiler/encoders/x64
Mar 23 01:27:21 Finished compiler/encoders/x64                                    0s  93MB
Mar 23 01:27:22 Starting compiler/encoders/arm7
Mar 23 01:27:24 Finished compiler/encoders/arm7                                   0s  98MB
Mar 23 01:27:24 Starting compiler/encoders/arm8
Mar 23 01:27:26 Finished compiler/encoders/arm8                                   0s  94MB
Mar 23 01:27:27 Starting compiler/encoders/arm8_asl
Mar 23 03:37:47 Finished compiler/encoders/arm8_asl                         2h10m19s  44GB
Mar 23 03:37:48 Starting compiler/encoders/mips
Mar 23 03:37:49 Finished compiler/encoders/mips                                   0s  93MB
Mar 23 03:37:50 Starting compiler/encoders/riscv
Mar 23 03:37:52 Finished compiler/encoders/riscv                                  0s  93MB
Mar 23 03:37:53 Starting compiler/encoders/ag32
Mar 23 03:37:54 Finished compiler/encoders/ag32                                   0s  93MB
Mar 23 03:37:55 Starting compiler/backend/x64
Mar 23 03:37:57 Finished compiler/backend/x64                                     0s 135MB
Mar 23 03:37:58 Starting compiler/backend/arm7
Mar 23 03:38:00 Finished compiler/backend/arm7                                    0s 134MB
Mar 23 03:38:01 Starting compiler/backend/arm8
Mar 23 03:38:02 Finished compiler/backend/arm8                                    0s 134MB
Mar 23 03:38:03 Starting compiler/backend/mips
Mar 23 03:38:05 Finished compiler/backend/mips                                    0s 134MB
Mar 23 03:38:06 Starting compiler/backend/riscv
Mar 23 03:38:08 Finished compiler/backend/riscv                                   0s 134MB
Mar 23 03:38:09 Starting compiler/backend/ag32
Mar 23 03:39:26 Finished compiler/backend/ag32                                 1m16s   2GB
Mar 23 03:39:27 Starting compiler/parsing/proofs
Mar 23 03:39:28 Finished compiler/parsing/proofs                                  0s  76MB
Mar 23 03:39:29 Starting compiler/inference/proofs
Mar 23 03:39:31 Finished compiler/inference/proofs                                0s  89MB
Mar 23 03:39:32 Starting compiler/backend/semantics
Mar 23 03:43:11 Finished compiler/backend/semantics                            3m38s   4GB
Mar 23 03:43:12 Starting compiler/backend/reg_alloc/proofs
Mar 23 03:43:14 Finished compiler/backend/reg_alloc/proofs                        0s  95MB
Mar 23 03:43:15 Starting compiler/backend/proofs
Mar 23 03:44:21 Finished compiler/backend/proofs                               1m05s   5GB
Mar 23 03:44:22 Starting compiler/backend/serialiser
Mar 23 03:44:24 Finished compiler/backend/serialiser                              1s 195MB
Mar 23 03:44:25 Starting compiler/encoders/x64/proofs
Mar 23 03:53:49 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Mar 23 03:53:50 Starting compiler/encoders/arm7/proofs
Mar 23 04:06:34 Finished compiler/encoders/arm7/proofs                        12m43s   8GB
Mar 23 04:06:35 Starting compiler/encoders/arm8/proofs
Mar 23 04:12:56 Finished compiler/encoders/arm8/proofs                         6m20s   6GB
Mar 23 04:12:57 Starting compiler/encoders/arm8_asl/proofs
Mar 23 05:00:24 Finished compiler/encoders/arm8_asl/proofs                    47m26s  11GB
Mar 23 05:00:25 Starting compiler/encoders/mips/proofs
Mar 23 05:10:35 Finished compiler/encoders/mips/proofs                        10m08s   7GB
Mar 23 05:10:36 Starting compiler/encoders/riscv/proofs
Mar 23 05:18:51 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Mar 23 05:18:52 Starting compiler/encoders/ag32/proofs
Mar 23 05:21:14 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 23 05:21:15 Starting compiler/backend/x64/proofs
Mar 23 05:21:55 Finished compiler/backend/x64/proofs                             39s   3GB
Mar 23 05:21:56 Starting compiler/backend/arm7/proofs
Mar 23 05:22:39 Finished compiler/backend/arm7/proofs                            41s   2GB
Mar 23 05:22:40 Starting compiler/backend/arm8/proofs
Mar 23 05:23:19 Finished compiler/backend/arm8/proofs                            38s   3GB
Mar 23 05:23:20 Starting compiler/backend/arm8_asl
Mar 23 05:23:48 Finished compiler/backend/arm8_asl                               27s   2GB
Mar 23 05:23:49 Starting compiler/backend/mips/proofs
Mar 23 05:24:33 Finished compiler/backend/mips/proofs                            43s   3GB
Mar 23 05:24:34 Starting compiler/backend/riscv/proofs
Mar 23 05:25:25 Finished compiler/backend/riscv/proofs                           49s   3GB
Mar 23 05:25:26 Starting compiler/backend/ag32/proofs
Mar 23 05:39:18 Finished compiler/backend/ag32/proofs                         13m51s   6GB
Mar 23 05:39:19 Starting candle/set-theory
Mar 23 05:40:01 Finished candle/set-theory                                       41s   1GB
Mar 23 05:40:02 Starting candle/syntax-lib
Mar 23 05:40:04 Finished candle/syntax-lib                                        0s  69MB
Mar 23 05:40:05 Starting candle/standard/syntax
Mar 23 05:40:20 Finished candle/standard/syntax                                  14s   1GB
Mar 23 05:40:21 Starting candle/standard/semantics
Mar 23 05:42:44 Finished candle/standard/semantics                             2m22s   3GB
Mar 23 05:42:45 Starting candle/standard/monadic
Mar 23 05:42:47 Finished candle/standard/monadic                                  0s 102MB
Mar 23 05:42:47 Starting candle/standard/ml_kernel
Mar 23 05:44:42 Finished candle/standard/ml_kernel                             1m53s   6GB
Mar 23 05:44:43 Starting candle/overloading/syntax
Mar 23 05:48:08 Finished candle/overloading/syntax                             3m24s   2GB
Mar 23 05:48:09 Starting candle/overloading/semantics
Mar 23 05:59:27 Finished candle/overloading/semantics                         11m17s   6GB
Mar 23 05:59:28 Starting candle/overloading/monadic
Mar 23 06:02:01 Finished candle/overloading/monadic                            2m32s   3GB
Mar 23 06:02:02 Starting candle/overloading/ml_kernel
Mar 23 06:09:37 Finished candle/overloading/ml_kernel                          7m34s   7GB
Mar 23 06:09:38 Starting candle/overloading/ml_checker
Mar 23 06:12:08 Finished candle/overloading/ml_checker                         2m28s   6GB
Mar 23 06:12:09 Starting candle/prover
Mar 23 06:21:57 Finished candle/prover                                         9m47s   5GB
Mar 23 06:21:58 Starting pancake
Mar 23 06:22:58 Finished pancake                                                 59s   1GB
Mar 23 06:22:59 Starting pancake/ffi
Mar 23 06:23:00 Finished pancake/ffi                                              0s  20MB
Mar 23 06:23:01 Starting pancake/semantics
Mar 23 06:25:36 Finished pancake/semantics                                     2m33s   2GB
Mar 23 06:25:37 Starting pancake/parser
Mar 23 06:26:03 Finished pancake/parser                                          25s   2GB
Mar 23 06:26:04 Starting pancake/proofs
Mar 23 06:56:42 Finished pancake/proofs                                       30m36s   9GB
Mar 23 06:56:43 Starting characteristic/examples
Mar 23 06:58:20 Finished characteristic/examples                               1m36s   6GB
Mar 23 06:58:21 Starting tutorial/solutions
Mar 23 07:13:50 Finished tutorial/solutions                                   15m27s  11GB
Mar 23 07:13:51 Starting translator/monadic/examples
Mar 23 07:17:37 Finished translator/monadic/examples                           3m45s   5GB
Mar 23 07:17:38 Starting examples
Mar 23 07:32:07 Finished examples                                             14m28s   7GB
Mar 23 07:32:08 Starting examples/compilation/x64
Mar 23 09:29:31 Finished examples/compilation/x64                           1h57m22s  19GB
Mar 23 09:29:32 Starting examples/compilation/x64/proofs
Mar 23 09:33:19 Finished examples/compilation/x64/proofs                       3m46s   6GB
Mar 23 09:33:20 Starting examples/compilation/ag32
Mar 23 10:03:18 Finished examples/compilation/ag32                            29m57s  11GB
Mar 23 10:03:19 Starting examples/compilation/ag32/proofs
Mar 23 10:04:49 Finished examples/compilation/ag32/proofs                      1m28s   7GB
Mar 23 10:04:50 Starting examples/compilation/to_word
Mar 23 10:08:41 Finished examples/compilation/to_word                          3m50s  10GB
Mar 23 10:08:42 Starting examples/lpr_checker
Mar 23 10:09:56 Finished examples/lpr_checker                                  1m12s   2GB
Mar 23 10:09:57 Starting examples/lpr_checker/array
Mar 23 10:40:18 Finished examples/lpr_checker/array                           30m20s  11GB
Mar 23 10:40:19 Starting examples/lpr_checker/array/compilation
Mar 23 11:17:33 Finished examples/lpr_checker/array/compilation               37m12s  62GB
Mar 23 11:17:33 Starting examples/lpr_checker/array/compilation/proofs
Mar 23 11:19:12 Finished examples/lpr_checker/array/compilation/proofs         1m37s   8GB
Mar 23 11:19:13 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 23 11:34:50 Finished examples/lpr_checker/array/compilation/proofsARM8    15m35s  36GB
Mar 23 11:34:51 Starting examples/xlrup_checker
Mar 23 11:36:00 Finished examples/xlrup_checker                                1m07s   1GB
Mar 23 11:36:00 Starting examples/xlrup_checker/array
Mar 23 11:52:20 Finished examples/xlrup_checker/array                         16m18s   8GB
Mar 23 11:52:21 Starting examples/xlrup_checker/array/compilation
Mar 23 12:13:25 Finished examples/xlrup_checker/array/compilation             21m03s  31GB
Mar 23 12:13:26 Starting examples/xlrup_checker/array/compilation/proofs
Mar 23 12:14:54 Finished examples/xlrup_checker/array/compilation/proofs       1m26s   7GB
Mar 23 12:14:55 Starting examples/pseudo_bool
Mar 23 12:16:59 Finished examples/pseudo_bool                                  2m03s   2GB
Mar 23 12:17:00 Starting examples/pseudo_bool/cnf_encoding
Mar 23 12:17:36 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Mar 23 12:17:37 Starting examples/pseudo_bool/graph_encoding
Mar 23 12:18:28 Finished examples/pseudo_bool/graph_encoding                     50s   2GB
Mar 23 12:18:28 Starting examples/pseudo_bool/array
Mar 23 13:30:19 Finished examples/pseudo_bool/array                         1h11m50s  35GB
Mar 23 13:30:20 Starting examples/pseudo_bool/array/compilation
Mar 23 21:27:48 Finished examples/pseudo_bool/array/compilation             7h57m26s 145GB
Mar 23 21:27:49 Starting examples/pseudo_bool/array/compilation/proofs
Mar 23 21:31:10 Finished examples/pseudo_bool/array/compilation/proofs         3m20s   7GB
Mar 23 21:31:11 Starting examples/opentheory
Mar 23 21:41:54 Finished examples/opentheory                                  10m42s   7GB
Mar 23 21:41:55 Starting examples/opentheory
Mar 23 21:41:57 Finished examples/opentheory                                      0s 122MB
Mar 23 21:41:58 Starting examples/opentheory/compilation
Mar 23 22:18:37 Finished examples/opentheory/compilation                      36m37s  49GB
Mar 23 22:18:38 Starting examples/opentheory/compilation/proofs
Mar 23 22:20:04 Finished examples/opentheory/compilation/proofs                1m25s   7GB
Mar 23 22:20:05 Starting examples/opentheory/compilation/ag32
Mar 23 22:54:16 Finished examples/opentheory/compilation/ag32                 34m09s  69GB
Mar 23 22:54:16 Starting examples/opentheory/compilation/ag32/proofs
Mar 23 22:56:34 Finished examples/opentheory/compilation/ag32/proofs           2m16s  11GB
Mar 23 22:56:35 Starting examples/sat_encodings
Mar 23 22:59:12 Finished examples/sat_encodings                                2m36s   1GB
Mar 23 22:59:13 Starting examples/sat_encodings/case_studies
Mar 23 23:01:10 Finished examples/sat_encodings/case_studies                   1m56s   1GB
Mar 23 23:01:11 Starting examples/sat_encodings/translation
Mar 23 23:07:26 Finished examples/sat_encodings/translation                    6m13s   7GB
Mar 23 23:07:27 Starting examples/sat_encodings/translation/compilation
Mar 23 23:43:58 Finished examples/sat_encodings/translation/compilation       36m30s  45GB
Mar 23 23:43:59 Starting examples/deflate
Mar 23 23:45:17 Finished examples/deflate                                      1m16s   1GB
Mar 23 23:45:18 Starting examples/deflate/translation
Mar 23 23:46:59 Finished examples/deflate/translation                          1m40s   7GB
Mar 23 23:47:00 Starting examples/deflate/translation/compilation
Mar 24 00:03:48 Finished examples/deflate/translation/compilation             16m46s  19GB
Mar 24 00:03:49 Starting examples/vipr
Mar 24 00:07:51 Finished examples/vipr                                         4m00s   5GB
Mar 24 00:07:52 Starting examples/vipr/compilation
Mar 24 00:28:04 Finished examples/vipr/compilation                            20m11s  33GB
Mar 24 00:28:05 Starting translator/okasaki-examples
Mar 24 00:33:06 Finished translator/okasaki-examples                           4m59s   3GB
Mar 24 00:33:06 Starting translator/other-examples
Mar 24 00:37:46 Finished translator/other-examples                             4m39s   3GB
Mar 24 00:37:47 Starting compiler/parsing/tests
Mar 24 00:38:21 Finished compiler/parsing/tests                                  33s   2GB
Mar 24 00:38:22 Starting compiler/inference/tests
Mar 24 00:45:53 Finished compiler/inference/tests                              7m29s   8GB
Mar 24 00:45:54 Starting compiler/printing/test
Mar 24 00:49:23 Finished compiler/printing/test                                3m27s   6GB
Mar 24 00:49:23 Starting icing/flover
Mar 24 01:24:28 Finished icing/flover                                         35m03s   5GB
Mar 24 01:24:29 Starting icing/
Mar 24 02:19:08 Finished icing/                                               54m37s  29GB
Mar 24 02:19:08 Starting icing/examples
Mar 24 02:20:53 Finished icing/examples                                        1m43s   9GB
Mar 24 02:20:53 Starting compiler/repl
Mar 24 02:29:53 Finished compiler/repl                                         8m58s   8GB
Mar 24 02:29:54 Starting unverified/sexpr-bootstrap/x64/64
Mar 24 02:41:17 Finished unverified/sexpr-bootstrap/x64/64                    10m59s  16GB
Mar 24 02:41:18 Starting unverified/sexpr-bootstrap/x64/32
Mar 24 02:50:47 Finished unverified/sexpr-bootstrap/x64/32                     9m10s  15GB
Mar 24 02:50:48 Starting compiler/benchmarks
Mar 24 02:51:33 Finished compiler/benchmarks                                     43s 713MB
Mar 24 02:51:34 Starting compiler/bootstrap/compilation/x64/64
Mar 24 18:19:23 Finished compiler/bootstrap/compilation/x64/64             15h27m36s 207GB
Mar 24 18:19:24 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 24 18:40:34 Finished compiler/bootstrap/compilation/x64/64/proofs         21m08s  49GB
Mar 24 18:40:35 Starting compiler/bootstrap/compilation/x64/32
Mar 25 02:16:28 Finished compiler/bootstrap/compilation/x64/32              7h35m45s 188GB
Mar 25 02:16:28 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 25 02:20:07 Finished compiler/bootstrap/compilation/x64/32/proofs          3m37s  18GB
Mar 25 02:20:08 Starting compiler/bootstrap/compilation/ag32/32
Mar 25 10:01:02 Finished compiler/bootstrap/compilation/ag32/32             7h40m53s 189GB
Mar 25 10:01:03 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 25 10:08:50 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m46s  51GB
Mar 25 10:08:51 SUCCESS