Job 2760

CakeML:b0d62f81210d9be53e885b7e319b52fca75de313
  Merge pull request #1118 from CakeML/1117-remove-option_map-defined-i [Dec 22 07:28:01]
HOL:1feeec007109c470c888c0f26819f864fdc38e28
  Merge pull request #1368 from HOL-Theorem-Prover/keccak [Dec 19 08:31:44]
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

Dec 22 07:36:49 Claimed job
Dec 22 07:36:53 Reusing HOL
Dec 22 07:37:03 Starting developers
Dec 22 07:37:07 Finished developers                                               3s 215MB
Dec 22 07:37:08 Starting developers/bin
Dec 22 07:37:15 Finished developers/bin                                           5s 746MB
Dec 22 07:37:16 Starting misc
Dec 22 07:38:00 Finished misc                                                    43s   2GB
Dec 22 07:38:01 Starting compiler/proofs
Dec 22 09:16:34 Finished compiler/proofs                                    1h38m31s  36GB
Dec 22 09:16:35 Starting compiler/bootstrap/translation
Dec 22 15:07:38 Finished compiler/bootstrap/translation                     5h51m02s 105GB
Dec 22 15:07:39 Starting semantics/ffi
Dec 22 15:07:49 Finished semantics/ffi                                            9s 606MB
Dec 22 15:07:50 Starting semantics
Dec 22 15:07:52 Finished semantics                                                0s  54MB
Dec 22 15:07:53 Starting semantics/proofs
Dec 22 15:08:16 Finished semantics/proofs                                        22s   1GB
Dec 22 15:08:17 Starting semantics/alt_semantics
Dec 22 15:08:38 Finished semantics/alt_semantics                                 19s 902MB
Dec 22 15:08:39 Starting semantics/alt_semantics/proofs
Dec 22 15:18:59 Finished semantics/alt_semantics/proofs                       10m19s   2GB
Dec 22 15:19:00 Starting basis/pure
Dec 22 15:19:02 Finished basis/pure                                               0s  64MB
Dec 22 15:19:02 Starting translator
Dec 22 15:20:36 Finished translator                                            1m32s   3GB
Dec 22 15:20:36 Starting compiler/parsing
Dec 22 15:20:38 Finished compiler/parsing                                         0s  56MB
Dec 22 15:20:39 Starting characteristic
Dec 22 15:20:40 Finished characteristic                                           0s  84MB
Dec 22 15:20:41 Starting translator/monadic
Dec 22 15:20:43 Finished translator/monadic                                       0s  90MB
Dec 22 15:20:44 Starting translator/monadic/monad_base
Dec 22 15:20:45 Finished translator/monadic/monad_base                            0s  52MB
Dec 22 15:20:46 Starting basis
Dec 22 15:23:11 Finished basis                                                 2m23s   4GB
Dec 22 15:23:11 Starting compiler
Dec 22 15:23:14 Finished compiler                                                 1s 197MB
Dec 22 15:23:15 Starting compiler/inference
Dec 22 15:23:17 Finished compiler/inference                                       0s  85MB
Dec 22 15:23:18 Starting compiler/backend/reg_alloc
Dec 22 15:23:19 Finished compiler/backend/reg_alloc                               0s  57MB
Dec 22 15:23:20 Starting compiler/backend/gc
Dec 22 15:23:22 Finished compiler/backend/gc                                      1s 135MB
Dec 22 15:23:23 Starting compiler/backend
Dec 22 15:23:28 Finished compiler/backend                                         3s 259MB
Dec 22 15:23:29 Starting compiler/encoders/asm
Dec 22 15:23:30 Finished compiler/encoders/asm                                    0s  82MB
Dec 22 15:23:31 Starting compiler/encoders/x64
Dec 22 15:23:33 Finished compiler/encoders/x64                                    0s  86MB
Dec 22 15:23:34 Starting compiler/encoders/arm7
Dec 22 15:23:36 Finished compiler/encoders/arm7                                   0s  90MB
Dec 22 15:23:37 Starting compiler/encoders/arm8
Dec 22 15:23:38 Finished compiler/encoders/arm8                                   0s  90MB
Dec 22 15:23:39 Starting compiler/encoders/arm8_asl
Dec 22 15:24:36 Finished compiler/encoders/arm8_asl                              56s  20GB
Dec 22 15:24:37 Starting compiler/encoders/mips
Dec 22 15:24:39 Finished compiler/encoders/mips                                   0s  90MB
Dec 22 15:24:40 Starting compiler/encoders/riscv
Dec 22 15:24:41 Finished compiler/encoders/riscv                                  0s  90MB
Dec 22 15:24:42 Starting compiler/encoders/ag32
Dec 22 15:24:44 Finished compiler/encoders/ag32                                   0s  80MB
Dec 22 15:24:45 Starting compiler/encoders/tests
Dec 22 15:24:47 Finished compiler/encoders/tests                                  0s 102MB
Dec 22 15:24:47 Starting compiler/encoders/monadic_enc
Dec 22 15:24:49 Finished compiler/encoders/monadic_enc                            1s 123MB
Dec 22 15:24:50 Starting compiler/backend/x64
Dec 22 15:24:52 Finished compiler/backend/x64                                     1s 126MB
Dec 22 15:24:53 Starting compiler/backend/arm7
Dec 22 15:24:55 Finished compiler/backend/arm7                                    1s 132MB
Dec 22 15:24:56 Starting compiler/backend/arm8
Dec 22 15:24:58 Finished compiler/backend/arm8                                    1s 132MB
Dec 22 15:24:59 Starting compiler/backend/mips
Dec 22 15:25:01 Finished compiler/backend/mips                                    1s 127MB
Dec 22 15:25:02 Starting compiler/backend/riscv
Dec 22 15:25:04 Finished compiler/backend/riscv                                   1s 127MB
Dec 22 15:25:05 Starting compiler/backend/ag32
Dec 22 15:26:12 Finished compiler/backend/ag32                                 1m05s   2GB
Dec 22 15:26:12 Starting compiler/backend/pattern_matching
Dec 22 15:26:14 Finished compiler/backend/pattern_matching                        0s  52MB
Dec 22 15:26:15 Starting compiler/parsing/ocaml
Dec 22 15:27:57 Finished compiler/parsing/ocaml                                1m41s   1GB
Dec 22 15:27:58 Starting compiler/printing
Dec 22 15:28:00 Finished compiler/printing                                        0s  83MB
Dec 22 15:28:01 Starting compiler/parsing/proofs
Dec 22 15:28:02 Finished compiler/parsing/proofs                                  0s  59MB
Dec 22 15:28:03 Starting compiler/inference/proofs
Dec 22 15:28:05 Finished compiler/inference/proofs                                0s  85MB
Dec 22 15:28:06 Starting compiler/backend/semantics
Dec 22 15:31:11 Finished compiler/backend/semantics                            3m04s   2GB
Dec 22 15:31:12 Starting compiler/backend/reg_alloc/proofs
Dec 22 15:31:13 Finished compiler/backend/reg_alloc/proofs                        0s  84MB
Dec 22 15:31:14 Starting compiler/backend/proofs
Dec 22 15:32:05 Finished compiler/backend/proofs                                 49s   4GB
Dec 22 15:32:06 Starting compiler/backend/serialiser
Dec 22 15:32:08 Finished compiler/backend/serialiser                              1s 135MB
Dec 22 15:32:09 Starting compiler/encoders/x64/proofs
Dec 22 15:42:21 Finished compiler/encoders/x64/proofs                         10m10s   4GB
Dec 22 15:42:21 Starting compiler/encoders/arm7/proofs
Dec 22 15:55:27 Finished compiler/encoders/arm7/proofs                        13m04s   7GB
Dec 22 15:55:28 Starting compiler/encoders/arm8/proofs
Dec 22 16:02:38 Finished compiler/encoders/arm8/proofs                         7m09s   4GB
Dec 22 16:02:39 Starting compiler/encoders/arm8_asl/proofs
Dec 22 16:17:45 Finished compiler/encoders/arm8_asl/proofs                    15m05s   3GB
Dec 22 16:17:46 Starting compiler/encoders/mips/proofs
Dec 22 16:27:54 Finished compiler/encoders/mips/proofs                        10m07s   9GB
Dec 22 16:27:55 Starting compiler/encoders/riscv/proofs
Dec 22 16:36:07 Finished compiler/encoders/riscv/proofs                        8m10s   3GB
Dec 22 16:36:08 Starting compiler/encoders/ag32/proofs
Dec 22 16:38:59 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Dec 22 16:39:00 Starting compiler/backend/x64/proofs
Dec 22 16:39:32 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 22 16:39:33 Starting compiler/backend/arm7/proofs
Dec 22 16:40:05 Finished compiler/backend/arm7/proofs                            30s   2GB
Dec 22 16:40:06 Starting compiler/backend/arm8/proofs
Dec 22 16:40:38 Finished compiler/backend/arm8/proofs                            31s   2GB
Dec 22 16:40:39 Starting compiler/backend/arm8_asl
Dec 22 16:40:59 Finished compiler/backend/arm8_asl                               18s   1GB
Dec 22 16:40:59 Starting compiler/backend/mips/proofs
Dec 22 16:41:30 Finished compiler/backend/mips/proofs                            29s   2GB
Dec 22 16:41:31 Starting compiler/backend/riscv/proofs
Dec 22 16:42:05 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 22 16:42:06 Starting compiler/backend/ag32/proofs
Dec 22 16:55:51 Finished compiler/backend/ag32/proofs                         13m43s   5GB
Dec 22 16:55:52 Starting compiler/backend/cv_compute
Dec 22 16:57:03 Finished compiler/backend/cv_compute                           1m10s   2GB
Dec 22 16:57:04 Starting cv_translator
Dec 22 17:17:49 Finished cv_translator                                        20m44s  11GB
Dec 22 17:17:50 Starting candle
Dec 22 17:17:51 Finished candle                                                   0s  12MB
Dec 22 17:17:52 Starting candle/set-theory
Dec 22 17:18:26 Finished candle/set-theory                                       33s   1GB
Dec 22 17:18:27 Starting candle/syntax-lib
Dec 22 17:18:28 Finished candle/syntax-lib                                        0s  59MB
Dec 22 17:18:29 Starting candle/standard
Dec 22 17:18:30 Finished candle/standard                                          0s  12MB
Dec 22 17:18:31 Starting candle/standard/syntax
Dec 22 17:18:43 Finished candle/standard/syntax                                  11s 796MB
Dec 22 17:18:44 Starting candle/standard/semantics
Dec 22 17:20:45 Finished candle/standard/semantics                             1m59s   1GB
Dec 22 17:20:46 Starting candle/standard/monadic
Dec 22 17:20:47 Finished candle/standard/monadic                                  0s  88MB
Dec 22 17:20:48 Starting candle/standard/ml_kernel
Dec 22 17:22:33 Finished candle/standard/ml_kernel                             1m43s   4GB
Dec 22 17:22:34 Starting candle/standard/ml_kernel/lisp
Dec 22 17:22:35 Finished candle/standard/ml_kernel/lisp                           0s  48MB
Dec 22 17:22:36 Starting candle/overloading
Dec 22 17:22:37 Finished candle/overloading                                       0s  12MB
Dec 22 17:22:38 Starting candle/overloading/syntax
Dec 22 17:25:45 Finished candle/overloading/syntax                             3m06s   2GB
Dec 22 17:25:46 Starting candle/overloading/semantics
Dec 22 17:36:47 Finished candle/overloading/semantics                         11m00s   8GB
Dec 22 17:36:48 Starting candle/overloading/monadic
Dec 22 17:39:07 Finished candle/overloading/monadic                            2m18s   2GB
Dec 22 17:39:08 Starting candle/overloading/ml_kernel
Dec 22 17:46:19 Finished candle/overloading/ml_kernel                          7m09s   5GB
Dec 22 17:46:20 Starting candle/overloading/ml_checker
Dec 22 17:48:31 Finished candle/overloading/ml_checker                         2m10s   6GB
Dec 22 17:48:32 Starting candle/prover
Dec 22 17:58:11 Finished candle/prover                                         9m37s   5GB
Dec 22 17:58:12 Starting candle/prover/compute
Dec 22 17:58:14 Finished candle/prover/compute                                    1s 116MB
Dec 22 17:58:15 Starting pancake
Dec 22 17:58:36 Finished pancake                                                 20s 842MB
Dec 22 17:58:37 Starting pancake/semantics
Dec 22 18:00:47 Finished pancake/semantics                                     2m08s   2GB
Dec 22 18:00:48 Starting pancake/parser
Dec 22 18:01:11 Finished pancake/parser                                          22s 442MB
Dec 22 18:01:12 Starting pancake/proofs
Dec 22 18:17:13 Finished pancake/proofs                                       15m59s   7GB
Dec 22 18:17:14 Starting pancake/ta_progs
Dec 22 18:17:14 Finished pancake/ta_progs                                         0s  10MB
Dec 22 18:17:15 Starting compiler/dafny
Dec 22 18:19:50 Finished compiler/dafny                                        2m33s   8GB
Dec 22 18:19:51 Starting compiler/dafny/translation
Dec 22 18:38:09 Finished compiler/dafny/translation                           18m17s  22GB
Dec 22 18:38:10 Starting compiler/dafny/compilation
Dec 22 18:40:51 Finished compiler/dafny/compilation                            2m39s   9GB
Dec 22 18:40:52 Starting compiler/dafny/semantics
Dec 22 18:41:29 Finished compiler/dafny/semantics                                35s   1GB
Dec 22 18:41:29 Starting characteristic/examples
Dec 22 18:42:55 Finished characteristic/examples                               1m24s   5GB
Dec 22 18:42:56 Starting tutorial/solutions
Dec 22 18:45:17 Finished tutorial/solutions                                    2m19s   3GB
Dec 22 18:45:18 Starting translator/monadic/examples
Dec 22 18:48:15 Finished translator/monadic/examples                           2m56s   3GB
Dec 22 18:48:16 Starting examples
Dec 22 18:54:11 Finished examples                                              5m53s   5GB
Dec 22 18:54:12 Starting examples/compilation
Dec 22 18:54:13 Finished examples/compilation                                     0s  11MB
Dec 22 18:54:13 Starting examples/compilation/x64
Dec 22 19:00:46 Finished examples/compilation/x64                              6m31s   4GB
Dec 22 19:00:47 Starting examples/compilation/x64/proofs
Dec 22 19:03:12 Finished examples/compilation/x64/proofs                       2m23s   4GB
Dec 22 19:03:12 Starting examples/compilation/ag32
Dec 22 19:04:59 Finished examples/compilation/ag32                             1m45s   3GB
Dec 22 19:05:00 Starting examples/compilation/ag32/proofs
Dec 22 19:06:01 Finished examples/compilation/ag32/proofs                        59s   5GB
Dec 22 19:06:02 Starting examples/lpr_checker
Dec 22 19:06:32 Finished examples/lpr_checker                                    28s   1GB
Dec 22 19:06:33 Starting examples/lpr_checker/array
Dec 22 19:32:33 Finished examples/lpr_checker/array                           25m59s  23GB
Dec 22 19:32:34 Starting examples/lpr_checker/array/compilation
Dec 22 19:40:38 Finished examples/lpr_checker/array/compilation                8m03s  36GB
Dec 22 19:40:39 Starting examples/lpr_checker/array/compilation/proofs
Dec 22 19:41:51 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Dec 22 19:41:52 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 22 19:43:03 Finished examples/lpr_checker/array/compilation/proofsARM8     1m10s   6GB
Dec 22 19:43:04 Starting .
Dec 22 19:43:07 Finished .                                                        2s 288MB
Dec 22 19:43:08 Starting examples/xlrup_checker
Dec 22 19:43:42 Finished examples/xlrup_checker                                  32s   1GB
Dec 22 19:43:43 Starting examples/xlrup_checker/array
Dec 22 19:56:28 Finished examples/xlrup_checker/array                         12m44s   9GB
Dec 22 19:56:29 Starting examples/xlrup_checker/array/compilation
Dec 22 19:57:28 Finished examples/xlrup_checker/array/compilation                58s   4GB
Dec 22 19:57:29 Starting examples/xlrup_checker/array/compilation/proofs
Dec 22 19:58:29 Finished examples/xlrup_checker/array/compilation/proofs         59s   4GB
Dec 22 19:58:30 Starting examples/pseudo_bool
Dec 22 20:00:02 Finished examples/pseudo_bool                                  1m30s   2GB
Dec 22 20:00:03 Starting examples/pseudo_bool/cnf_encoding
Dec 22 20:00:32 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Dec 22 20:00:33 Starting examples/pseudo_bool/graph_encoding
Dec 22 20:01:15 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Dec 22 20:01:16 Starting examples/pseudo_bool/array
Dec 22 21:08:26 Finished examples/pseudo_bool/array                         1h07m08s  32GB
Dec 22 21:08:27 Starting examples/pseudo_bool/array/compilation
Dec 22 21:17:12 Finished examples/pseudo_bool/array/compilation                8m43s  15GB
Dec 22 21:17:13 Starting examples/pseudo_bool/array/compilation/proofs
Dec 22 21:19:48 Finished examples/pseudo_bool/array/compilation/proofs         2m34s   6GB
Dec 22 21:19:49 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 22 21:21:03 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m12s   6GB
Dec 22 21:21:03 Starting examples/opentheory
Dec 22 21:29:36 Finished examples/opentheory                                   8m31s   5GB
Dec 22 21:29:37 Starting examples/opentheory/compilation
Dec 22 21:31:01 Finished examples/opentheory/compilation                       1m22s   5GB
Dec 22 21:31:02 Starting examples/opentheory/compilation/proofs
Dec 22 21:32:04 Finished examples/opentheory/compilation/proofs                1m01s   4GB
Dec 22 21:32:05 Starting examples/opentheory/compilation/ag32
Dec 22 21:33:32 Finished examples/opentheory/compilation/ag32                  1m26s   6GB
Dec 22 21:33:33 Starting examples/opentheory/compilation/ag32/proofs
Dec 22 21:35:11 Finished examples/opentheory/compilation/ag32/proofs           1m37s   8GB
Dec 22 21:35:12 Starting examples/sat_encodings
Dec 22 21:36:12 Finished examples/sat_encodings                                  59s 894MB
Dec 22 21:36:13 Starting examples/sat_encodings/demo
Dec 22 21:36:14 Finished examples/sat_encodings/demo                              0s  11MB
Dec 22 21:36:15 Starting examples/sat_encodings/case_studies
Dec 22 21:38:01 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Dec 22 21:38:02 Starting examples/sat_encodings/translation
Dec 22 21:41:39 Finished examples/sat_encodings/translation                    3m36s   3GB
Dec 22 21:41:40 Starting examples/sat_encodings/translation/compilation
Dec 22 21:43:26 Finished examples/sat_encodings/translation/compilation        1m45s   4GB
Dec 22 21:43:27 Starting examples/deflate
Dec 22 21:43:55 Finished examples/deflate                                        27s 711MB
Dec 22 21:43:56 Starting examples/deflate/translation
Dec 22 21:45:00 Finished examples/deflate/translation                          1m03s   4GB
Dec 22 21:45:01 Starting examples/deflate/translation/compilation
Dec 22 21:45:48 Finished examples/deflate/translation/compilation                45s   3GB
Dec 22 21:45:49 Starting examples/vipr
Dec 22 21:49:13 Finished examples/vipr                                         3m23s   3GB
Dec 22 21:49:14 Starting examples/vipr/compilation
Dec 22 21:50:08 Finished examples/vipr/compilation                               52s   3GB
Dec 22 21:50:09 Starting translator/okasaki-examples
Dec 22 21:54:11 Finished translator/okasaki-examples                           4m01s   3GB
Dec 22 21:54:12 Starting translator/other-examples
Dec 22 21:55:01 Finished translator/other-examples                               48s   3GB
Dec 22 21:55:02 Starting translator/other-examples/auxiliary
Dec 22 21:55:03 Finished translator/other-examples/auxiliary                      0s  11MB
Dec 22 21:55:04 Starting compiler/parsing/tests
Dec 22 21:55:39 Finished compiler/parsing/tests                                  34s   1GB
Dec 22 21:55:40 Starting compiler/inference/tests
Dec 22 21:56:17 Finished compiler/inference/tests                                35s   2GB
Dec 22 21:56:18 Starting compiler/printing/test
Dec 22 21:57:29 Finished compiler/printing/test                                1m10s   5GB
Dec 22 21:57:30 Starting icing/flover
Dec 22 22:31:47 Finished icing/flover                                         34m15s   2GB
Dec 22 22:31:48 Starting icing/flover/Infra
Dec 22 22:31:48 Finished icing/flover/Infra                                       0s  11MB
Dec 22 22:31:49 Starting icing/flover/semantics
Dec 22 22:31:50 Finished icing/flover/semantics                                   0s  12MB
Dec 22 22:31:51 Starting icing/
Dec 22 22:58:56 Finished icing/                                               27m04s   7GB
Dec 22 22:58:57 Starting icing/examples
Dec 22 23:00:31 Finished icing/examples                                        1m33s   8GB
Dec 22 23:00:32 Starting compiler/repl
Dec 22 23:08:19 Finished compiler/repl                                         7m45s   6GB
Dec 22 23:08:20 Starting unverified/sexpr-bootstrap/x64/64
Dec 22 23:12:23 Finished unverified/sexpr-bootstrap/x64/64                     3m49s  17GB
Dec 22 23:12:24 Starting unverified/sexpr-bootstrap/x64/32
Dec 22 23:15:55 Finished unverified/sexpr-bootstrap/x64/32                     3m20s  15GB
Dec 22 23:15:56 Starting compiler/benchmarks
Dec 22 23:16:41 Finished compiler/benchmarks                                     44s 711MB
Dec 22 23:16:42 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Dec 22 23:16:45 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 256MB
Dec 22 23:16:46 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Dec 22 23:16:50 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 258MB
Dec 22 23:16:50 Starting compiler/bootstrap/compilation/x64/64
Dec 22 23:41:04 Finished compiler/bootstrap/compilation/x64/64                24m01s  82GB
Dec 22 23:41:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 23 00:04:19 Finished compiler/bootstrap/compilation/x64/64/proofs         23m13s  49GB
Dec 23 00:04:19 Starting compiler/bootstrap/compilation/x64/32
Dec 23 00:29:08 Finished compiler/bootstrap/compilation/x64/32                24m41s  65GB
Dec 23 00:29:09 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 23 00:33:12 Finished compiler/bootstrap/compilation/x64/32/proofs          4m02s  23GB
Dec 23 00:33:13 Starting compiler/bootstrap/compilation/arm8/64
Dec 23 01:07:28 Finished compiler/bootstrap/compilation/arm8/64               34m07s  60GB
Dec 23 01:07:29 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 23 01:12:42 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m11s  29GB
Dec 23 01:12:42 Starting compiler/bootstrap/compilation/ag32/32
Dec 23 01:38:27 Finished compiler/bootstrap/compilation/ag32/32               25m43s  68GB
Dec 23 01:38:28 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 23 01:43:09 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m40s  31GB
Dec 23 01:43:10 SUCCESS