Job 2353

CakeML:b377df8d9ae3aa2f6ef354f96f868787e781851e
  Merge pull request #988 from CakeML/pancake_shmem_syntax [Mar 23 22:12:00]
HOL:671b4b712f9e860a558393b4b0c6a15e3a52a754
  Updated HOL Description with higher mathematics contents promoted to  [Mar 18 23:15:32]
Machine:pavlova
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Mar 23 22:27:34 Claimed job
Mar 23 22:27:40 Reusing HOL
Mar 23 22:27:50 Starting developers
Mar 23 22:27:53 Finished developers                                               2s 201MB
Mar 23 22:27:54 Starting developers/bin
Mar 23 22:28:05 Finished developers/bin                                           9s   1GB
Mar 23 22:28:06 Starting compiler/proofs
Mar 24 00:18:08 Finished compiler/proofs                                    1h50m00s  27GB
Mar 24 00:18:09 Starting compiler/bootstrap/translation
Mar 24 08:18:43 Finished compiler/bootstrap/translation                     8h00m32s  77GB
Mar 24 08:18:43 Starting semantics/ffi
Mar 24 08:18:52 Finished semantics/ffi                                            7s 637MB
Mar 24 08:18:53 Starting semantics
Mar 24 08:18:54 Finished semantics                                                0s  66MB
Mar 24 08:18:55 Starting semantics/proofs
Mar 24 08:19:30 Finished semantics/proofs                                        34s   1GB
Mar 24 08:19:31 Starting semantics/alt_semantics
Mar 24 08:20:10 Finished semantics/alt_semantics                                 37s   1GB
Mar 24 08:20:11 Starting semantics/alt_semantics/proofs
Mar 24 08:31:05 Finished semantics/alt_semantics/proofs                       10m52s   3GB
Mar 24 08:31:06 Starting basis/pure
Mar 24 08:31:07 Finished basis/pure                                               0s  69MB
Mar 24 08:31:08 Starting translator
Mar 24 08:32:51 Finished translator                                            1m41s   4GB
Mar 24 08:32:52 Starting compiler/parsing
Mar 24 08:32:53 Finished compiler/parsing                                         0s  67MB
Mar 24 08:32:54 Starting characteristic
Mar 24 08:32:55 Finished characteristic                                           0s  88MB
Mar 24 08:32:56 Starting translator/monadic
Mar 24 08:32:58 Finished translator/monadic                                       0s  91MB
Mar 24 08:32:59 Starting basis
Mar 24 08:36:37 Finished basis                                                 3m36s   4GB
Mar 24 08:36:38 Starting compiler/inference
Mar 24 08:36:39 Finished compiler/inference                                       0s  79MB
Mar 24 08:36:40 Starting compiler/backend/reg_alloc
Mar 24 08:36:41 Finished compiler/backend/reg_alloc                               0s  67MB
Mar 24 08:36:42 Starting compiler/backend/gc
Mar 24 08:36:44 Finished compiler/backend/gc                                      0s 137MB
Mar 24 08:36:45 Starting compiler/backend
Mar 24 08:37:02 Finished compiler/backend                                        16s   1GB
Mar 24 08:37:03 Starting compiler/encoders/asm
Mar 24 08:37:05 Finished compiler/encoders/asm                                    0s  93MB
Mar 24 08:37:06 Starting compiler/encoders/x64
Mar 24 08:37:07 Finished compiler/encoders/x64                                    0s  94MB
Mar 24 08:37:08 Starting compiler/encoders/arm7
Mar 24 08:37:10 Finished compiler/encoders/arm7                                   0s  93MB
Mar 24 08:37:11 Starting compiler/encoders/arm8
Mar 24 08:37:12 Finished compiler/encoders/arm8                                   0s  93MB
Mar 24 08:37:13 Starting compiler/encoders/arm8_asl
Mar 24 08:39:32 Finished compiler/encoders/arm8_asl                            2m17s   1GB
Mar 24 08:39:33 Starting compiler/encoders/mips
Mar 24 08:39:34 Finished compiler/encoders/mips                                   0s  93MB
Mar 24 08:39:35 Starting compiler/encoders/riscv
Mar 24 08:39:36 Finished compiler/encoders/riscv                                  0s  94MB
Mar 24 08:39:37 Starting compiler/encoders/ag32
Mar 24 08:39:39 Finished compiler/encoders/ag32                                   0s  92MB
Mar 24 08:39:40 Starting compiler/backend/x64
Mar 24 08:39:41 Finished compiler/backend/x64                                     0s 130MB
Mar 24 08:39:42 Starting compiler/backend/arm7
Mar 24 08:39:44 Finished compiler/backend/arm7                                    0s 126MB
Mar 24 08:39:45 Starting compiler/backend/arm8
Mar 24 08:39:47 Finished compiler/backend/arm8                                    0s 126MB
Mar 24 08:39:48 Starting compiler/backend/mips
Mar 24 08:39:50 Finished compiler/backend/mips                                    0s 125MB
Mar 24 08:39:51 Starting compiler/backend/riscv
Mar 24 08:39:52 Finished compiler/backend/riscv                                   0s 126MB
Mar 24 08:39:53 Starting compiler/backend/ag32
Mar 24 08:41:14 Finished compiler/backend/ag32                                 1m19s   3GB
Mar 24 08:41:15 Starting compiler/parsing/proofs
Mar 24 08:41:16 Finished compiler/parsing/proofs                                  0s  78MB
Mar 24 08:41:17 Starting compiler/inference/proofs
Mar 24 08:41:19 Finished compiler/inference/proofs                                0s  89MB
Mar 24 08:41:20 Starting compiler/backend/semantics
Mar 24 08:44:59 Finished compiler/backend/semantics                            3m38s   2GB
Mar 24 08:44:59 Starting compiler/backend/reg_alloc/proofs
Mar 24 08:45:01 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Mar 24 08:45:02 Starting compiler/backend/proofs
Mar 24 08:46:05 Finished compiler/backend/proofs                               1m01s   3GB
Mar 24 08:46:06 Starting compiler/backend/serialiser
Mar 24 08:46:08 Finished compiler/backend/serialiser                              1s 193MB
Mar 24 08:46:09 Starting compiler/encoders/x64/proofs
Mar 24 08:55:34 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Mar 24 08:55:35 Starting compiler/encoders/arm7/proofs
Mar 24 09:08:18 Finished compiler/encoders/arm7/proofs                        12m42s   7GB
Mar 24 09:08:19 Starting compiler/encoders/arm8/proofs
Mar 24 09:15:03 Finished compiler/encoders/arm8/proofs                         6m42s   5GB
Mar 24 09:15:04 Starting compiler/encoders/arm8_asl/proofs
Mar 24 09:28:54 Finished compiler/encoders/arm8_asl/proofs                    13m49s   4GB
Mar 24 09:28:55 Starting compiler/encoders/mips/proofs
Mar 24 09:39:08 Finished compiler/encoders/mips/proofs                        10m11s   6GB
Mar 24 09:39:09 Starting compiler/encoders/riscv/proofs
Mar 24 09:47:33 Finished compiler/encoders/riscv/proofs                        8m23s   3GB
Mar 24 09:47:34 Starting compiler/encoders/ag32/proofs
Mar 24 09:49:55 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 24 09:49:56 Starting compiler/backend/x64/proofs
Mar 24 09:50:37 Finished compiler/backend/x64/proofs                             40s   3GB
Mar 24 09:50:38 Starting compiler/backend/arm7/proofs
Mar 24 09:51:20 Finished compiler/backend/arm7/proofs                            41s   2GB
Mar 24 09:51:21 Starting compiler/backend/arm8/proofs
Mar 24 09:52:03 Finished compiler/backend/arm8/proofs                            40s   3GB
Mar 24 09:52:04 Starting compiler/backend/arm8_asl
Mar 24 09:52:31 Finished compiler/backend/arm8_asl                               25s   1GB
Mar 24 09:52:32 Starting compiler/backend/mips/proofs
Mar 24 09:53:15 Finished compiler/backend/mips/proofs                            42s   3GB
Mar 24 09:53:16 Starting compiler/backend/riscv/proofs
Mar 24 09:54:06 Finished compiler/backend/riscv/proofs                           48s   4GB
Mar 24 09:54:06 Starting compiler/backend/ag32/proofs
Mar 24 10:08:01 Finished compiler/backend/ag32/proofs                         13m53s   6GB
Mar 24 10:08:02 Starting candle/set-theory
Mar 24 10:08:46 Finished candle/set-theory                                       43s   1GB
Mar 24 10:08:47 Starting candle/syntax-lib
Mar 24 10:08:48 Finished candle/syntax-lib                                        0s  74MB
Mar 24 10:08:49 Starting candle/standard/syntax
Mar 24 10:09:06 Finished candle/standard/syntax                                  16s   1GB
Mar 24 10:09:07 Starting candle/standard/semantics
Mar 24 10:11:32 Finished candle/standard/semantics                             2m24s   3GB
Mar 24 10:11:33 Starting candle/standard/monadic
Mar 24 10:11:35 Finished candle/standard/monadic                                  0s  96MB
Mar 24 10:11:36 Starting candle/standard/ml_kernel
Mar 24 10:13:27 Finished candle/standard/ml_kernel                             1m50s   5GB
Mar 24 10:13:28 Starting candle/overloading/syntax
Mar 24 10:16:48 Finished candle/overloading/syntax                             3m19s   2GB
Mar 24 10:16:49 Starting candle/overloading/semantics
Mar 24 10:28:11 Finished candle/overloading/semantics                         11m21s   6GB
Mar 24 10:28:12 Starting candle/overloading/monadic
Mar 24 10:30:49 Finished candle/overloading/monadic                            2m35s   3GB
Mar 24 10:30:50 Starting candle/overloading/ml_kernel
Mar 24 10:38:18 Finished candle/overloading/ml_kernel                          7m27s   6GB
Mar 24 10:38:19 Starting candle/overloading/ml_checker
Mar 24 10:40:51 Finished candle/overloading/ml_checker                         2m30s   7GB
Mar 24 10:40:52 Starting candle/prover
Mar 24 10:50:40 Finished candle/prover                                         9m46s   5GB
Mar 24 10:50:41 Starting pancake
Mar 24 10:51:42 Finished pancake                                               1m00s   1GB
Mar 24 10:51:43 Starting pancake/ffi
Mar 24 10:51:44 Finished pancake/ffi                                              0s  19MB
Mar 24 10:51:45 Starting pancake/semantics
Mar 24 10:54:20 Finished pancake/semantics                                     2m34s   2GB
Mar 24 10:54:21 Starting pancake/parser
Mar 24 10:54:49 Finished pancake/parser                                          26s   2GB
Mar 24 10:54:49 Starting pancake/proofs
Mar 24 11:26:03 Finished pancake/proofs                                       31m12s   9GB
Mar 24 11:26:04 Starting characteristic/examples
Mar 24 11:27:43 Finished characteristic/examples                               1m38s   5GB
Mar 24 11:27:44 Starting tutorial/solutions
Mar 24 11:44:04 Finished tutorial/solutions                                   16m18s  11GB
Mar 24 11:44:05 Starting translator/monadic/examples
Mar 24 11:47:57 Finished translator/monadic/examples                           3m51s   5GB
Mar 24 11:47:58 Starting examples
Mar 24 12:02:12 Finished examples                                             14m13s   7GB
Mar 24 12:02:13 Starting examples/compilation/x64
Mar 24 14:00:53 Finished examples/compilation/x64                           1h58m39s  20GB
Mar 24 14:00:54 Starting examples/compilation/x64/proofs
Mar 24 14:04:44 Finished examples/compilation/x64/proofs                       3m49s   5GB
Mar 24 14:04:45 Starting examples/compilation/ag32
Mar 24 14:35:02 Finished examples/compilation/ag32                            30m15s  15GB
Mar 24 14:35:03 Starting examples/compilation/ag32/proofs
Mar 24 14:36:33 Finished examples/compilation/ag32/proofs                      1m29s   6GB
Mar 24 14:36:34 Starting examples/compilation/to_word
Mar 24 14:40:30 Finished examples/compilation/to_word                          3m55s  13GB
Mar 24 14:40:31 Starting examples/lpr_checker
Mar 24 14:41:47 Finished examples/lpr_checker                                  1m14s   2GB
Mar 24 14:41:48 Starting examples/lpr_checker/array
Mar 24 15:12:05 Finished examples/lpr_checker/array                           30m16s   9GB
Mar 24 15:12:06 Starting examples/lpr_checker/array/compilation
Mar 24 15:49:27 Finished examples/lpr_checker/array/compilation               37m20s  64GB
Mar 24 15:49:28 Starting examples/lpr_checker/array/compilation/proofs
Mar 24 15:51:09 Finished examples/lpr_checker/array/compilation/proofs         1m39s   8GB
Mar 24 15:51:10 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 24 16:02:23 Finished examples/lpr_checker/array/compilation/proofsARM8    11m12s  36GB
Mar 24 16:02:25 Starting examples/xlrup_checker
Mar 24 16:03:35 Finished examples/xlrup_checker                                1m09s   1GB
Mar 24 16:03:36 Starting examples/xlrup_checker/array
Mar 24 16:19:47 Finished examples/xlrup_checker/array                         16m10s   8GB
Mar 24 16:19:48 Starting examples/xlrup_checker/array/compilation
Mar 24 16:40:49 Finished examples/xlrup_checker/array/compilation             20m59s  21GB
Mar 24 16:40:50 Starting examples/xlrup_checker/array/compilation/proofs
Mar 24 16:42:20 Finished examples/xlrup_checker/array/compilation/proofs       1m29s   6GB
Mar 24 16:42:22 Starting examples/pseudo_bool
Mar 24 16:44:26 Finished examples/pseudo_bool                                  2m02s   2GB
Mar 24 16:44:27 Starting examples/pseudo_bool/cnf_encoding
Mar 24 16:45:02 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Mar 24 16:45:03 Starting examples/pseudo_bool/graph_encoding
Mar 24 16:45:52 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Mar 24 16:45:53 Starting examples/pseudo_bool/array
Mar 24 17:57:20 Finished examples/pseudo_bool/array                         1h11m26s  38GB
Mar 24 17:57:21 Starting examples/pseudo_bool/array/compilation
Mar 25 01:43:53 Finished examples/pseudo_bool/array/compilation             7h46m30s 144GB
Mar 25 01:43:54 Starting examples/pseudo_bool/array/compilation/proofs
Mar 25 01:47:16 Finished examples/pseudo_bool/array/compilation/proofs         3m20s   8GB
Mar 25 01:47:17 Starting examples/opentheory
Mar 25 01:57:52 Finished examples/opentheory                                  10m34s   7GB
Mar 25 01:57:53 Starting examples/opentheory
Mar 25 01:57:55 Finished examples/opentheory                                      0s 123MB
Mar 25 01:57:56 Starting examples/opentheory/compilation
Mar 25 02:33:58 Finished examples/opentheory/compilation                      36m01s  49GB
Mar 25 02:33:59 Starting examples/opentheory/compilation/proofs
Mar 25 02:35:30 Finished examples/opentheory/compilation/proofs                1m29s   6GB
Mar 25 02:35:31 Starting examples/opentheory/compilation/ag32
Mar 25 03:07:50 Finished examples/opentheory/compilation/ag32                 32m18s  51GB
Mar 25 03:07:51 Starting examples/opentheory/compilation/ag32/proofs
Mar 25 03:10:15 Finished examples/opentheory/compilation/ag32/proofs           2m22s  10GB
Mar 25 03:10:16 Starting examples/sat_encodings
Mar 25 03:12:56 Finished examples/sat_encodings                                2m39s   1GB
Mar 25 03:12:57 Starting examples/sat_encodings/case_studies
Mar 25 03:14:56 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Mar 25 03:14:57 Starting examples/sat_encodings/translation
Mar 25 03:21:12 Finished examples/sat_encodings/translation                    6m13s   7GB
Mar 25 03:21:13 Starting examples/sat_encodings/translation/compilation
Mar 25 03:58:47 Finished examples/sat_encodings/translation/compilation       37m32s  43GB
Mar 25 03:58:48 Starting examples/deflate
Mar 25 04:00:04 Finished examples/deflate                                      1m15s   1GB
Mar 25 04:00:05 Starting examples/deflate/translation
Mar 25 04:01:45 Finished examples/deflate/translation                          1m38s   7GB
Mar 25 04:01:46 Starting examples/deflate/translation/compilation
Mar 25 04:19:40 Finished examples/deflate/translation/compilation             17m53s  25GB
Mar 25 04:19:41 Starting examples/vipr
Mar 25 04:23:57 Finished examples/vipr                                         4m14s   7GB
Mar 25 04:23:58 Starting examples/vipr/compilation
Mar 25 04:44:29 Finished examples/vipr/compilation                            20m30s  33GB
Mar 25 04:44:30 Starting translator/okasaki-examples
Mar 25 04:49:38 Finished translator/okasaki-examples                           5m06s   4GB
Mar 25 04:49:39 Starting translator/other-examples
Mar 25 04:50:49 Finished translator/other-examples                             1m09s   3GB
Mar 25 04:50:50 Starting compiler/parsing/tests
Mar 25 04:51:24 Finished compiler/parsing/tests                                  33s   1GB
Mar 25 04:51:25 Starting compiler/inference/tests
Mar 25 04:58:50 Finished compiler/inference/tests                              7m23s   5GB
Mar 25 04:58:51 Starting compiler/printing/test
Mar 25 05:02:18 Finished compiler/printing/test                                3m26s   6GB
Mar 25 05:02:19 Starting icing/flover
Mar 25 05:37:43 Finished icing/flover                                         35m22s   4GB
Mar 25 05:37:44 Starting icing/
Mar 25 06:32:35 Finished icing/                                               54m49s  22GB
Mar 25 06:32:36 Starting icing/examples
Mar 25 06:34:14 Finished icing/examples                                        1m36s   8GB
Mar 25 06:34:14 Starting compiler/repl
Mar 25 06:42:58 Finished compiler/repl                                         8m42s  10GB
Mar 25 06:42:59 Starting unverified/sexpr-bootstrap/x64/64
Mar 25 06:54:24 Finished unverified/sexpr-bootstrap/x64/64                    11m00s  15GB
Mar 25 06:54:25 Starting unverified/sexpr-bootstrap/x64/32
Mar 25 07:03:55 Finished unverified/sexpr-bootstrap/x64/32                     9m12s  13GB
Mar 25 07:03:56 Starting compiler/benchmarks
Mar 25 07:04:42 Finished compiler/benchmarks                                     44s 713MB
Mar 25 07:04:43 Starting compiler/bootstrap/compilation/x64/64
Mar 25 22:18:37 Finished compiler/bootstrap/compilation/x64/64             15h13m42s 188GB
Mar 25 22:18:38 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 25 22:40:25 Finished compiler/bootstrap/compilation/x64/64/proofs         21m46s  52GB
Mar 25 22:40:26 Starting compiler/bootstrap/compilation/x64/32
Mar 26 06:06:38 Finished compiler/bootstrap/compilation/x64/32              7h26m04s 133GB
Mar 26 06:06:39 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 26 06:10:18 Finished compiler/bootstrap/compilation/x64/32/proofs          3m38s  20GB
Mar 26 06:10:19 Starting compiler/bootstrap/compilation/ag32/32
Mar 26 13:58:00 Finished compiler/bootstrap/compilation/ag32/32             7h47m39s 148GB
Mar 26 13:58:01 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 26 14:06:00 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m58s  42GB
Mar 26 14:06:01 SUCCESS