Job 2650

CakeML:b9843ac59b40ad1a8adc0dfdfcd5e0656f44ab6e
  Merge pull request #1064 from CakeML/remove-define [Oct 10 11:32:18]
HOL:4d1b16443810923d9832780d757d1b868bc9eef4
  cv translator: allow known fun types in ctors [Oct 09 12:54:25]
Machine:pavlova
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-arm8-64.tar.gz
cake-x64-32.tar.gz

Oct 11 17:24:02 Claimed job
Oct 11 17:24:05 Reusing HOL
Oct 11 17:24:17 Starting developers
Oct 11 17:24:21 Finished developers                                               3s 130MB
Oct 11 17:24:22 Starting developers/bin
Oct 11 17:24:45 Finished developers/bin                                          22s   1GB
Oct 11 17:24:46 Starting compiler/proofs
Oct 11 19:07:53 Finished compiler/proofs                                    1h43m05s  35GB
Oct 11 19:07:54 Starting compiler/bootstrap/translation
Oct 12 04:16:49 Finished compiler/bootstrap/translation                     9h08m54s  57GB
Oct 12 04:16:50 Starting semantics/ffi
Oct 12 04:17:00 Finished semantics/ffi                                            8s 730MB
Oct 12 04:17:01 Starting semantics
Oct 12 04:17:02 Finished semantics                                                0s  70MB
Oct 12 04:17:03 Starting semantics/proofs
Oct 12 04:17:28 Finished semantics/proofs                                        23s 797MB
Oct 12 04:17:29 Starting semantics/alt_semantics
Oct 12 04:17:52 Finished semantics/alt_semantics                                 22s 673MB
Oct 12 04:17:53 Starting semantics/alt_semantics/proofs
Oct 12 04:28:10 Finished semantics/alt_semantics/proofs                       10m15s   4GB
Oct 12 04:28:11 Starting basis/pure
Oct 12 04:28:12 Finished basis/pure                                               0s  71MB
Oct 12 04:28:13 Starting translator
Oct 12 04:29:50 Finished translator                                            1m35s   4GB
Oct 12 04:29:51 Starting compiler/parsing
Oct 12 04:29:52 Finished compiler/parsing                                         0s  72MB
Oct 12 04:29:53 Starting characteristic
Oct 12 04:29:55 Finished characteristic                                           0s  95MB
Oct 12 04:29:56 Starting translator/monadic
Oct 12 04:29:58 Finished translator/monadic                                       0s  99MB
Oct 12 04:29:58 Starting basis
Oct 12 04:32:34 Finished basis                                                 2m34s   9GB
Oct 12 04:32:35 Starting compiler/inference
Oct 12 04:32:36 Finished compiler/inference                                       0s  94MB
Oct 12 04:32:37 Starting compiler/backend/reg_alloc
Oct 12 04:32:39 Finished compiler/backend/reg_alloc                               0s  64MB
Oct 12 04:32:40 Starting compiler/backend/gc
Oct 12 04:32:42 Finished compiler/backend/gc                                      1s 143MB
Oct 12 04:32:43 Starting compiler/backend
Oct 12 04:32:48 Finished compiler/backend                                         4s 381MB
Oct 12 04:32:49 Starting compiler/encoders/asm
Oct 12 04:32:51 Finished compiler/encoders/asm                                    0s  90MB
Oct 12 04:32:52 Starting compiler/encoders/x64
Oct 12 04:32:53 Finished compiler/encoders/x64                                    0s  94MB
Oct 12 04:32:54 Starting compiler/encoders/arm7
Oct 12 04:32:56 Finished compiler/encoders/arm7                                   0s  99MB
Oct 12 04:32:57 Starting compiler/encoders/arm8
Oct 12 04:32:58 Finished compiler/encoders/arm8                                   0s  99MB
Oct 12 04:32:59 Starting compiler/encoders/arm8_asl
Oct 12 06:49:59 Finished compiler/encoders/arm8_asl                         2h16m58s  39GB
Oct 12 06:50:00 Starting compiler/encoders/mips
Oct 12 06:50:02 Finished compiler/encoders/mips                                   0s  92MB
Oct 12 06:50:03 Starting compiler/encoders/riscv
Oct 12 06:50:04 Finished compiler/encoders/riscv                                  0s  99MB
Oct 12 06:50:05 Starting compiler/encoders/ag32
Oct 12 06:50:07 Finished compiler/encoders/ag32                                   0s  89MB
Oct 12 06:50:08 Starting compiler/backend/x64
Oct 12 06:50:10 Finished compiler/backend/x64                                     1s 137MB
Oct 12 06:50:11 Starting compiler/backend/arm7
Oct 12 06:50:13 Finished compiler/backend/arm7                                    1s 139MB
Oct 12 06:50:14 Starting compiler/backend/arm8
Oct 12 06:50:16 Finished compiler/backend/arm8                                    1s 139MB
Oct 12 06:50:17 Starting compiler/backend/mips
Oct 12 06:50:19 Finished compiler/backend/mips                                    1s 139MB
Oct 12 06:50:20 Starting compiler/backend/riscv
Oct 12 06:50:22 Finished compiler/backend/riscv                                   1s 139MB
Oct 12 06:50:23 Starting compiler/backend/ag32
Oct 12 06:51:33 Finished compiler/backend/ag32                                 1m09s   2GB
Oct 12 06:51:34 Starting compiler/parsing/proofs
Oct 12 06:51:36 Finished compiler/parsing/proofs                                  0s  74MB
Oct 12 06:51:37 Starting compiler/inference/proofs
Oct 12 06:51:38 Finished compiler/inference/proofs                                0s  99MB
Oct 12 06:51:39 Starting compiler/backend/semantics
Oct 12 06:54:55 Finished compiler/backend/semantics                            3m14s   4GB
Oct 12 06:54:56 Starting compiler/backend/reg_alloc/proofs
Oct 12 06:54:57 Finished compiler/backend/reg_alloc/proofs                        0s 101MB
Oct 12 06:54:58 Starting compiler/backend/proofs
Oct 12 06:55:53 Finished compiler/backend/proofs                                 53s   2GB
Oct 12 06:55:54 Starting compiler/backend/serialiser
Oct 12 06:55:56 Finished compiler/backend/serialiser                              1s 152MB
Oct 12 06:55:57 Starting compiler/encoders/x64/proofs
Oct 12 07:06:15 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Oct 12 07:06:16 Starting compiler/encoders/arm7/proofs
Oct 12 07:19:32 Finished compiler/encoders/arm7/proofs                        13m14s  11GB
Oct 12 07:19:33 Starting compiler/encoders/arm8/proofs
Oct 12 07:27:00 Finished compiler/encoders/arm8/proofs                         7m25s   6GB
Oct 12 07:27:01 Starting compiler/encoders/arm8_asl/proofs
Oct 12 08:17:49 Finished compiler/encoders/arm8_asl/proofs                    50m47s  11GB
Oct 12 08:17:50 Starting compiler/encoders/mips/proofs
Oct 12 08:28:12 Finished compiler/encoders/mips/proofs                        10m21s   9GB
Oct 12 08:28:13 Starting compiler/encoders/riscv/proofs
Oct 12 08:36:30 Finished compiler/encoders/riscv/proofs                        8m15s   3GB
Oct 12 08:36:31 Starting compiler/encoders/ag32/proofs
Oct 12 08:39:27 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Oct 12 08:39:28 Starting compiler/backend/x64/proofs
Oct 12 08:40:16 Finished compiler/backend/x64/proofs                             46s   3GB
Oct 12 08:40:16 Starting compiler/backend/arm7/proofs
Oct 12 08:41:05 Finished compiler/backend/arm7/proofs                            47s   2GB
Oct 12 08:41:06 Starting compiler/backend/arm8/proofs
Oct 12 08:41:50 Finished compiler/backend/arm8/proofs                            43s   3GB
Oct 12 08:41:51 Starting compiler/backend/arm8_asl
Oct 12 08:42:22 Finished compiler/backend/arm8_asl                               30s   2GB
Oct 12 08:42:23 Starting compiler/backend/mips/proofs
Oct 12 08:43:14 Finished compiler/backend/mips/proofs                            50s   3GB
Oct 12 08:43:15 Starting compiler/backend/riscv/proofs
Oct 12 08:44:12 Finished compiler/backend/riscv/proofs                           55s   3GB
Oct 12 08:44:13 Starting compiler/backend/ag32/proofs
Oct 12 08:58:39 Finished compiler/backend/ag32/proofs                         14m25s   6GB
Oct 12 08:58:40 Starting compiler/backend/cv_compute
Oct 12 09:00:35 Finished compiler/backend/cv_compute                           1m53s   3GB
Oct 12 09:00:35 Starting cv_translator
Oct 12 09:20:32 Finished cv_translator                                        19m55s  13GB
Oct 12 09:20:33 Starting candle/set-theory
Oct 12 09:21:20 Finished candle/set-theory                                       46s   1GB
Oct 12 09:21:21 Starting candle/syntax-lib
Oct 12 09:21:22 Finished candle/syntax-lib                                        0s  69MB
Oct 12 09:21:23 Starting candle/standard/syntax
Oct 12 09:21:44 Finished candle/standard/syntax                                  19s   1GB
Oct 12 09:21:45 Starting candle/standard/semantics
Oct 12 09:24:37 Finished candle/standard/semantics                             2m51s   3GB
Oct 12 09:24:38 Starting candle/standard/monadic
Oct 12 09:24:39 Finished candle/standard/monadic                                  0s 106MB
Oct 12 09:24:40 Starting candle/standard/ml_kernel
Oct 12 09:26:53 Finished candle/standard/ml_kernel                             2m11s   7GB
Oct 12 09:26:53 Starting candle/overloading/syntax
Oct 12 09:30:36 Finished candle/overloading/syntax                             3m41s   2GB
Oct 12 09:30:37 Starting candle/overloading/semantics
Oct 12 09:42:21 Finished candle/overloading/semantics                         11m42s   5GB
Oct 12 09:42:22 Starting candle/overloading/monadic
Oct 12 09:44:50 Finished candle/overloading/monadic                            2m27s   2GB
Oct 12 09:44:51 Starting candle/overloading/ml_kernel
Oct 12 09:52:53 Finished candle/overloading/ml_kernel                          8m01s   7GB
Oct 12 09:52:54 Starting candle/overloading/ml_checker
Oct 12 09:55:37 Finished candle/overloading/ml_checker                         2m42s   7GB
Oct 12 09:55:38 Starting candle/prover
Oct 12 10:06:20 Finished candle/prover                                        10m40s   5GB
Oct 12 10:06:21 Starting pancake
Oct 12 10:06:48 Finished pancake                                                 26s 994MB
Oct 12 10:06:49 Starting pancake/ffi
Oct 12 10:06:50 Finished pancake/ffi                                              0s  22MB
Oct 12 10:06:51 Starting pancake/semantics
Oct 12 10:09:05 Finished pancake/semantics                                     2m13s   2GB
Oct 12 10:09:06 Starting pancake/parser
Oct 12 10:09:30 Finished pancake/parser                                          22s 819MB
Oct 12 10:09:31 Starting pancake/proofs
Oct 12 10:25:38 Finished pancake/proofs                                       16m05s   9GB
Oct 12 10:25:39 Starting compiler/dafny
Oct 12 10:28:10 Finished compiler/dafny                                        2m30s   8GB
Oct 12 10:28:11 Starting compiler/dafny/translation
Oct 12 10:57:06 Finished compiler/dafny/translation                           28m53s  14GB
Oct 12 10:57:07 Starting compiler/dafny/compilation
Oct 12 11:00:38 Finished compiler/dafny/compilation                            3m30s  14GB
Oct 12 11:00:39 Starting compiler/dafny/semantics
Oct 12 11:01:17 Finished compiler/dafny/semantics                                37s   1GB
Oct 12 11:01:18 Starting characteristic/examples
Oct 12 11:02:51 Finished characteristic/examples                               1m32s   4GB
Oct 12 11:02:52 Starting tutorial/solutions
Oct 12 11:05:39 Finished tutorial/solutions                                    2m46s   5GB
Oct 12 11:05:40 Starting translator/monadic/examples
Oct 12 11:08:52 Finished translator/monadic/examples                           3m10s   3GB
Oct 12 11:08:53 Starting examples
Oct 12 11:21:09 Finished examples                                             12m14s   5GB
Oct 12 11:21:09 Starting examples/compilation/x64
Oct 12 11:31:18 Finished examples/compilation/x64                             10m06s   7GB
Oct 12 11:31:19 Starting examples/compilation/x64/proofs
Oct 12 11:36:14 Finished examples/compilation/x64/proofs                       4m54s   7GB
Oct 12 11:36:15 Starting examples/compilation/ag32
Oct 12 11:39:03 Finished examples/compilation/ag32                             2m47s   5GB
Oct 12 11:39:04 Starting examples/compilation/ag32/proofs
Oct 12 11:40:54 Finished examples/compilation/ag32/proofs                      1m49s  10GB
Oct 12 11:40:55 Starting examples/compilation/to_word
Oct 12 11:45:09 Finished examples/compilation/to_word                          4m13s  14GB
Oct 12 11:45:10 Starting examples/lpr_checker
Oct 12 11:45:42 Finished examples/lpr_checker                                    30s   1GB
Oct 12 11:45:43 Starting examples/lpr_checker/array
Oct 12 12:12:41 Finished examples/lpr_checker/array                           26m56s  32GB
Oct 12 12:12:42 Starting examples/lpr_checker/array/compilation
Oct 12 12:15:36 Finished examples/lpr_checker/array/compilation                2m53s  11GB
Oct 12 12:15:37 Starting examples/lpr_checker/array/compilation/proofs
Oct 12 12:17:42 Finished examples/lpr_checker/array/compilation/proofs         2m03s   9GB
Oct 12 12:17:43 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 12 12:19:38 Finished examples/lpr_checker/array/compilation/proofsARM8     1m54s  10GB
Oct 12 12:19:39 Starting examples/xlrup_checker
Oct 12 12:20:15 Finished examples/xlrup_checker                                  34s   1GB
Oct 12 12:20:15 Starting examples/xlrup_checker/array
Oct 12 12:33:38 Finished examples/xlrup_checker/array                         13m21s  10GB
Oct 12 12:33:39 Starting examples/xlrup_checker/array/compilation
Oct 12 12:35:07 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Oct 12 12:35:08 Starting examples/xlrup_checker/array/compilation/proofs
Oct 12 12:37:05 Finished examples/xlrup_checker/array/compilation/proofs       1m56s   8GB
Oct 12 12:37:06 Starting examples/pseudo_bool
Oct 12 12:38:33 Finished examples/pseudo_bool                                  1m25s   1GB
Oct 12 12:38:34 Starting examples/pseudo_bool/cnf_encoding
Oct 12 12:39:16 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Oct 12 12:39:17 Starting examples/pseudo_bool/graph_encoding
Oct 12 12:40:13 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 12 12:40:13 Starting examples/pseudo_bool/array
Oct 12 13:43:33 Finished examples/pseudo_bool/array                         1h03m18s  33GB
Oct 12 13:43:34 Starting examples/pseudo_bool/array/compilation
Oct 12 13:57:18 Finished examples/pseudo_bool/array/compilation               13m43s  29GB
Oct 12 13:57:19 Starting examples/pseudo_bool/array/compilation/proofs
Oct 12 14:01:32 Finished examples/pseudo_bool/array/compilation/proofs         4m12s   9GB
Oct 12 14:01:33 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 12 14:03:27 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m53s   8GB
Oct 12 14:03:28 Starting examples/opentheory
Oct 12 14:12:08 Finished examples/opentheory                                   8m38s   5GB
Oct 12 14:12:09 Starting examples/opentheory
Oct 12 14:12:11 Finished examples/opentheory                                      1s 126MB
Oct 12 14:12:12 Starting examples/opentheory/compilation
Oct 12 14:14:21 Finished examples/opentheory/compilation                       2m07s   9GB
Oct 12 14:14:22 Starting examples/opentheory/compilation/proofs
Oct 12 14:16:17 Finished examples/opentheory/compilation/proofs                1m54s   7GB
Oct 12 14:16:18 Starting examples/opentheory/compilation/ag32
Oct 12 14:18:30 Finished examples/opentheory/compilation/ag32                  2m11s   9GB
Oct 12 14:18:31 Starting examples/opentheory/compilation/ag32/proofs
Oct 12 14:21:03 Finished examples/opentheory/compilation/ag32/proofs           2m31s  13GB
Oct 12 14:21:04 Starting examples/sat_encodings
Oct 12 14:22:07 Finished examples/sat_encodings                                1m02s 932MB
Oct 12 14:22:08 Starting examples/sat_encodings/case_studies
Oct 12 14:24:22 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 12 14:24:23 Starting examples/sat_encodings/translation
Oct 12 14:28:06 Finished examples/sat_encodings/translation                    3m42s   3GB
Oct 12 14:28:07 Starting examples/sat_encodings/translation/compilation
Oct 12 14:30:38 Finished examples/sat_encodings/translation/compilation        2m30s   7GB
Oct 12 14:30:39 Starting examples/deflate
Oct 12 14:31:08 Finished examples/deflate                                        27s 759MB
Oct 12 14:31:09 Starting examples/deflate/translation
Oct 12 14:32:10 Finished examples/deflate/translation                          1m00s   2GB
Oct 12 14:32:11 Starting examples/deflate/translation/compilation
Oct 12 14:33:20 Finished examples/deflate/translation/compilation              1m07s   5GB
Oct 12 14:33:21 Starting examples/vipr
Oct 12 14:37:10 Finished examples/vipr                                         3m48s   8GB
Oct 12 14:37:11 Starting examples/vipr/compilation
Oct 12 14:38:32 Finished examples/vipr/compilation                             1m20s   6GB
Oct 12 14:38:33 Starting translator/okasaki-examples
Oct 12 14:42:48 Finished translator/okasaki-examples                           4m13s   4GB
Oct 12 14:42:49 Starting translator/other-examples
Oct 12 14:47:50 Finished translator/other-examples                             5m00s   3GB
Oct 12 14:47:51 Starting compiler/parsing/tests
Oct 12 14:48:30 Finished compiler/parsing/tests                                  38s   2GB
Oct 12 14:48:31 Starting compiler/inference/tests
Oct 12 14:49:17 Finished compiler/inference/tests                                45s   3GB
Oct 12 14:49:17 Starting compiler/printing/test
Oct 12 14:50:56 Finished compiler/printing/test                                1m37s   7GB
Oct 12 14:50:57 Starting icing/flover
Oct 12 15:27:41 Finished icing/flover                                         36m43s   4GB
Oct 12 15:27:42 Starting icing/
Oct 12 15:55:33 Finished icing/                                               27m50s   9GB
Oct 12 15:55:34 Starting icing/examples
Oct 12 15:57:29 Finished icing/examples                                        1m53s   9GB
Oct 12 15:57:30 Starting compiler/repl
Oct 12 16:06:52 Finished compiler/repl                                         9m20s  12GB
Oct 12 16:06:52 Starting unverified/sexpr-bootstrap/x64/64
Oct 12 16:20:56 Finished unverified/sexpr-bootstrap/x64/64                    13m36s  17GB
Oct 12 16:20:57 Starting unverified/sexpr-bootstrap/x64/32
Oct 12 16:32:32 Finished unverified/sexpr-bootstrap/x64/32                    11m14s  15GB
Oct 12 16:32:33 Starting compiler/benchmarks
Oct 12 16:33:18 Finished compiler/benchmarks                                     44s 712MB
Oct 12 16:33:19 Starting compiler/bootstrap/compilation/x64/64
Oct 12 17:19:45 Finished compiler/bootstrap/compilation/x64/64                46m12s 129GB
Oct 12 17:19:46 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 12 17:44:41 Finished compiler/bootstrap/compilation/x64/64/proofs         24m53s  48GB
Oct 12 17:44:42 Starting compiler/bootstrap/compilation/x64/32
Oct 12 18:27:10 Finished compiler/bootstrap/compilation/x64/32                42m20s 110GB
Oct 12 18:27:11 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 12 18:32:35 Finished compiler/bootstrap/compilation/x64/32/proofs          5m22s  25GB
Oct 12 18:32:36 Starting compiler/bootstrap/compilation/arm8/64
Oct 12 19:33:19 Finished compiler/bootstrap/compilation/arm8/64             1h00m34s 128GB
Oct 12 19:33:20 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 12 19:39:44 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m22s  32GB
Oct 12 19:39:44 Starting compiler/bootstrap/compilation/ag32/32
Oct 12 20:22:48 Finished compiler/bootstrap/compilation/ag32/32               43m02s 109GB
Oct 12 20:22:49 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 12 20:28:48 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m58s  31GB
Oct 12 20:28:49 SUCCESS