Job 2759

CakeML:f86557b251a98fdb9e2359cf56828e04df6ca34d
  Merge pull request #1038 from CakeML/ssa_fix [Dec 21 01:43:26]
HOL:1feeec007109c470c888c0f26819f864fdc38e28
  Merge pull request #1368 from HOL-Theorem-Prover/keccak [Dec 19 08:31:44]
Machine:lammmington
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 21 17:02:38 Claimed job
Dec 21 17:02:43 Building HOL
Dec 21 17:13:45 Starting developers
Dec 21 17:13:49 Finished developers                                               3s 208MB
Dec 21 17:13:50 Starting developers/bin
Dec 21 17:13:56 Finished developers/bin                                           4s 746MB
Dec 21 17:13:57 Starting misc
Dec 21 17:14:58 Finished misc                                                  1m00s   2GB
Dec 21 17:14:59 Starting compiler/proofs
Dec 21 18:56:18 Finished compiler/proofs                                    1h41m17s  46GB
Dec 21 18:56:18 Starting compiler/bootstrap/translation
Dec 22 00:44:11 Finished compiler/bootstrap/translation                     5h47m51s 103GB
Dec 22 00:44:12 Starting semantics/ffi
Dec 22 00:44:22 Finished semantics/ffi                                            9s 607MB
Dec 22 00:44:23 Starting semantics
Dec 22 00:44:25 Finished semantics                                                0s  53MB
Dec 22 00:44:26 Starting semantics/proofs
Dec 22 00:44:49 Finished semantics/proofs                                        22s 780MB
Dec 22 00:44:50 Starting semantics/alt_semantics
Dec 22 00:45:10 Finished semantics/alt_semantics                                 19s 602MB
Dec 22 00:45:11 Starting semantics/alt_semantics/proofs
Dec 22 00:55:34 Finished semantics/alt_semantics/proofs                       10m21s   2GB
Dec 22 00:55:35 Starting basis/pure
Dec 22 00:55:37 Finished basis/pure                                               0s  60MB
Dec 22 00:55:37 Starting translator
Dec 22 00:57:13 Finished translator                                            1m34s   2GB
Dec 22 00:57:14 Starting compiler/parsing
Dec 22 00:57:15 Finished compiler/parsing                                         0s  57MB
Dec 22 00:57:16 Starting characteristic
Dec 22 00:57:18 Finished characteristic                                           0s  84MB
Dec 22 00:57:19 Starting translator/monadic
Dec 22 00:57:20 Finished translator/monadic                                       0s  85MB
Dec 22 00:57:21 Starting translator/monadic/monad_base
Dec 22 00:57:23 Finished translator/monadic/monad_base                            0s  52MB
Dec 22 00:57:24 Starting basis
Dec 22 00:59:48 Finished basis                                                 2m23s   3GB
Dec 22 00:59:49 Starting compiler
Dec 22 00:59:51 Finished compiler                                                 1s 193MB
Dec 22 00:59:52 Starting compiler/inference
Dec 22 00:59:54 Finished compiler/inference                                       0s  83MB
Dec 22 00:59:55 Starting compiler/backend/reg_alloc
Dec 22 00:59:56 Finished compiler/backend/reg_alloc                               0s  52MB
Dec 22 00:59:57 Starting compiler/backend/gc
Dec 22 00:59:59 Finished compiler/backend/gc                                      1s 130MB
Dec 22 01:00:00 Starting compiler/backend
Dec 22 01:00:05 Finished compiler/backend                                         4s 242MB
Dec 22 01:00:06 Starting compiler/encoders/asm
Dec 22 01:00:07 Finished compiler/encoders/asm                                    0s  80MB
Dec 22 01:00:08 Starting compiler/encoders/x64
Dec 22 01:00:10 Finished compiler/encoders/x64                                    0s  88MB
Dec 22 01:00:11 Starting compiler/encoders/arm7
Dec 22 01:00:13 Finished compiler/encoders/arm7                                   0s  85MB
Dec 22 01:00:13 Starting compiler/encoders/arm8
Dec 22 01:00:15 Finished compiler/encoders/arm8                                   0s  84MB
Dec 22 01:00:16 Starting compiler/encoders/arm8_asl
Dec 22 03:02:16 Finished compiler/encoders/arm8_asl                         2h01m59s  40GB
Dec 22 03:02:17 Starting compiler/encoders/mips
Dec 22 03:02:19 Finished compiler/encoders/mips                                   0s  88MB
Dec 22 03:02:20 Starting compiler/encoders/riscv
Dec 22 03:02:22 Finished compiler/encoders/riscv                                  0s  88MB
Dec 22 03:02:23 Starting compiler/encoders/ag32
Dec 22 03:02:24 Finished compiler/encoders/ag32                                   0s  84MB
Dec 22 03:02:25 Starting compiler/encoders/tests
Dec 22 03:02:27 Finished compiler/encoders/tests                                  1s 111MB
Dec 22 03:02:28 Starting compiler/encoders/monadic_enc
Dec 22 03:02:30 Finished compiler/encoders/monadic_enc                            1s 124MB
Dec 22 03:02:31 Starting compiler/backend/x64
Dec 22 03:02:33 Finished compiler/backend/x64                                     1s 124MB
Dec 22 03:02:34 Starting compiler/backend/arm7
Dec 22 03:02:36 Finished compiler/backend/arm7                                    1s 123MB
Dec 22 03:02:37 Starting compiler/backend/arm8
Dec 22 03:02:39 Finished compiler/backend/arm8                                    1s 123MB
Dec 22 03:02:40 Starting compiler/backend/mips
Dec 22 03:02:42 Finished compiler/backend/mips                                    1s 123MB
Dec 22 03:02:43 Starting compiler/backend/riscv
Dec 22 03:02:45 Finished compiler/backend/riscv                                   1s 124MB
Dec 22 03:02:46 Starting compiler/backend/ag32
Dec 22 03:03:51 Finished compiler/backend/ag32                                 1m04s   3GB
Dec 22 03:03:52 Starting compiler/backend/pattern_matching
Dec 22 03:03:53 Finished compiler/backend/pattern_matching                        0s  53MB
Dec 22 03:03:54 Starting compiler/parsing/ocaml
Dec 22 03:05:37 Finished compiler/parsing/ocaml                                1m42s   1GB
Dec 22 03:05:38 Starting compiler/printing
Dec 22 03:05:40 Finished compiler/printing                                        0s  86MB
Dec 22 03:05:41 Starting compiler/parsing/proofs
Dec 22 03:05:42 Finished compiler/parsing/proofs                                  0s  61MB
Dec 22 03:05:43 Starting compiler/inference/proofs
Dec 22 03:05:45 Finished compiler/inference/proofs                                0s  86MB
Dec 22 03:05:46 Starting compiler/backend/semantics
Dec 22 03:08:51 Finished compiler/backend/semantics                            3m04s   3GB
Dec 22 03:08:52 Starting compiler/backend/reg_alloc/proofs
Dec 22 03:08:53 Finished compiler/backend/reg_alloc/proofs                        0s  84MB
Dec 22 03:08:54 Starting compiler/backend/proofs
Dec 22 03:09:41 Finished compiler/backend/proofs                                 46s   2GB
Dec 22 03:09:42 Starting compiler/backend/serialiser
Dec 22 03:09:44 Finished compiler/backend/serialiser                              1s 131MB
Dec 22 03:09:45 Starting compiler/encoders/x64/proofs
Dec 22 03:19:55 Finished compiler/encoders/x64/proofs                         10m08s   4GB
Dec 22 03:19:56 Starting compiler/encoders/arm7/proofs
Dec 22 03:33:01 Finished compiler/encoders/arm7/proofs                        13m04s   5GB
Dec 22 03:33:02 Starting compiler/encoders/arm8/proofs
Dec 22 03:39:51 Finished compiler/encoders/arm8/proofs                         6m48s   4GB
Dec 22 03:39:52 Starting compiler/encoders/arm8_asl/proofs
Dec 22 04:30:04 Finished compiler/encoders/arm8_asl/proofs                    50m11s  20GB
Dec 22 04:30:05 Starting compiler/encoders/mips/proofs
Dec 22 04:40:22 Finished compiler/encoders/mips/proofs                        10m15s   7GB
Dec 22 04:40:23 Starting compiler/encoders/riscv/proofs
Dec 22 04:48:38 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Dec 22 04:48:39 Starting compiler/encoders/ag32/proofs
Dec 22 04:51:31 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Dec 22 04:51:32 Starting compiler/backend/x64/proofs
Dec 22 04:52:03 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 22 04:52:04 Starting compiler/backend/arm7/proofs
Dec 22 04:52:38 Finished compiler/backend/arm7/proofs                            32s   2GB
Dec 22 04:52:39 Starting compiler/backend/arm8/proofs
Dec 22 04:53:12 Finished compiler/backend/arm8/proofs                            32s   2GB
Dec 22 04:53:13 Starting compiler/backend/arm8_asl
Dec 22 04:53:33 Finished compiler/backend/arm8_asl                               19s   1GB
Dec 22 04:53:34 Starting compiler/backend/mips/proofs
Dec 22 04:54:06 Finished compiler/backend/mips/proofs                            30s   2GB
Dec 22 04:54:07 Starting compiler/backend/riscv/proofs
Dec 22 04:54:38 Finished compiler/backend/riscv/proofs                           30s   2GB
Dec 22 04:54:39 Starting compiler/backend/ag32/proofs
Dec 22 05:08:34 Finished compiler/backend/ag32/proofs                         13m54s   5GB
Dec 22 05:08:35 Starting compiler/backend/cv_compute
Dec 22 05:09:48 Finished compiler/backend/cv_compute                           1m11s   2GB
Dec 22 05:09:48 Starting cv_translator
Dec 22 05:30:47 Finished cv_translator                                        20m57s   9GB
Dec 22 05:30:48 Starting candle
Dec 22 05:30:48 Finished candle                                                   0s  12MB
Dec 22 05:30:49 Starting candle/set-theory
Dec 22 05:31:24 Finished candle/set-theory                                       33s   1GB
Dec 22 05:31:25 Starting candle/syntax-lib
Dec 22 05:31:26 Finished candle/syntax-lib                                        0s  59MB
Dec 22 05:31:27 Starting candle/standard
Dec 22 05:31:28 Finished candle/standard                                          0s  12MB
Dec 22 05:31:29 Starting candle/standard/syntax
Dec 22 05:31:42 Finished candle/standard/syntax                                  11s 769MB
Dec 22 05:31:42 Starting candle/standard/semantics
Dec 22 05:33:45 Finished candle/standard/semantics                             2m01s   2GB
Dec 22 05:33:46 Starting candle/standard/monadic
Dec 22 05:33:48 Finished candle/standard/monadic                                  0s  87MB
Dec 22 05:33:49 Starting candle/standard/ml_kernel
Dec 22 05:35:33 Finished candle/standard/ml_kernel                             1m43s   4GB
Dec 22 05:35:34 Starting candle/standard/ml_kernel/lisp
Dec 22 05:35:35 Finished candle/standard/ml_kernel/lisp                           0s  45MB
Dec 22 05:35:36 Starting candle/overloading
Dec 22 05:35:37 Finished candle/overloading                                       0s  11MB
Dec 22 05:35:38 Starting candle/overloading/syntax
Dec 22 05:38:47 Finished candle/overloading/syntax                             3m08s   2GB
Dec 22 05:38:48 Starting candle/overloading/semantics
Dec 22 05:49:44 Finished candle/overloading/semantics                         10m54s   5GB
Dec 22 05:49:45 Starting candle/overloading/monadic
Dec 22 05:52:04 Finished candle/overloading/monadic                            2m17s   2GB
Dec 22 05:52:05 Starting candle/overloading/ml_kernel
Dec 22 05:59:16 Finished candle/overloading/ml_kernel                          7m10s   6GB
Dec 22 05:59:17 Starting candle/overloading/ml_checker
Dec 22 06:01:28 Finished candle/overloading/ml_checker                         2m10s   6GB
Dec 22 06:01:29 Starting candle/prover
Dec 22 06:11:08 Finished candle/prover                                         9m37s   5GB
Dec 22 06:11:09 Starting candle/prover/compute
Dec 22 06:11:11 Finished candle/prover/compute                                    1s 121MB
Dec 22 06:11:12 Starting pancake
Dec 22 06:11:33 Finished pancake                                                 20s 828MB
Dec 22 06:11:34 Starting pancake/semantics
Dec 22 06:13:42 Finished pancake/semantics                                     2m06s   2GB
Dec 22 06:13:43 Starting pancake/parser
Dec 22 06:14:06 Finished pancake/parser                                          22s 463MB
Dec 22 06:14:07 Starting pancake/proofs
Dec 22 06:30:03 Finished pancake/proofs                                       15m54s   7GB
Dec 22 06:30:04 Starting pancake/ta_progs
Dec 22 06:30:05 Finished pancake/ta_progs                                         0s  10MB
Dec 22 06:30:05 Starting compiler/dafny
Dec 22 06:32:47 Finished compiler/dafny                                        2m40s   8GB
Dec 22 06:32:48 Starting compiler/dafny/translation
Dec 22 06:51:01 Finished compiler/dafny/translation                           18m11s  25GB
Dec 22 06:51:02 Starting compiler/dafny/compilation
Dec 22 06:53:31 Finished compiler/dafny/compilation                            2m28s   7GB
Dec 22 06:53:32 Starting compiler/dafny/semantics
Dec 22 06:54:08 Finished compiler/dafny/semantics                                34s   1GB
Dec 22 06:54:09 Starting characteristic/examples
Dec 22 06:55:33 Finished characteristic/examples                               1m23s   4GB
Dec 22 06:55:34 Starting tutorial/solutions
Dec 22 06:58:00 Finished tutorial/solutions                                    2m25s   3GB
Dec 22 06:58:01 Starting translator/monadic/examples
Dec 22 07:00:56 Finished translator/monadic/examples                           2m53s   3GB
Dec 22 07:00:56 Starting examples
Dec 22 07:07:00 Finished examples                                              6m02s   5GB
Dec 22 07:07:01 Starting examples/compilation
Dec 22 07:07:02 Finished examples/compilation                                     0s  11MB
Dec 22 07:07:03 Starting examples/compilation/x64
Dec 22 07:13:37 Finished examples/compilation/x64                              6m32s   3GB
Dec 22 07:13:38 Starting examples/compilation/x64/proofs
Dec 22 07:16:02 Finished examples/compilation/x64/proofs                       2m23s   4GB
Dec 22 07:16:03 Starting examples/compilation/ag32
Dec 22 07:17:51 Finished examples/compilation/ag32                             1m47s   3GB
Dec 22 07:17:52 Starting examples/compilation/ag32/proofs
Dec 22 07:18:53 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Dec 22 07:18:54 Starting examples/lpr_checker
Dec 22 07:19:24 Finished examples/lpr_checker                                    28s   1GB
Dec 22 07:19:25 Starting examples/lpr_checker/array
Dec 22 07:45:44 Finished examples/lpr_checker/array                           26m17s  21GB
Dec 22 07:45:45 Starting examples/lpr_checker/array/compilation
Dec 22 07:54:32 Finished examples/lpr_checker/array/compilation                8m45s  37GB
Dec 22 07:54:33 Starting examples/lpr_checker/array/compilation/proofs
Dec 22 07:55:49 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Dec 22 07:55:50 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 22 07:57:02 Finished examples/lpr_checker/array/compilation/proofsARM8     1m11s   6GB
Dec 22 07:57:03 Starting .
Dec 22 07:57:06 Finished .                                                        2s 287MB
Dec 22 07:57:07 Starting examples/xlrup_checker
Dec 22 07:57:43 Finished examples/xlrup_checker                                  34s   1GB
Dec 22 07:57:44 Starting examples/xlrup_checker/array
Dec 22 08:11:00 Finished examples/xlrup_checker/array                         13m15s   8GB
Dec 22 08:11:01 Starting examples/xlrup_checker/array/compilation
Dec 22 08:12:01 Finished examples/xlrup_checker/array/compilation                59s   4GB
Dec 22 08:12:02 Starting examples/xlrup_checker/array/compilation/proofs
Dec 22 08:13:04 Finished examples/xlrup_checker/array/compilation/proofs       1m01s   4GB
Dec 22 08:13:05 Starting examples/pseudo_bool
Dec 22 08:14:38 Finished examples/pseudo_bool                                  1m32s   2GB
Dec 22 08:14:39 Starting examples/pseudo_bool/cnf_encoding
Dec 22 08:15:09 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Dec 22 08:15:10 Starting examples/pseudo_bool/graph_encoding
Dec 22 08:15:55 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 22 08:15:56 Starting examples/pseudo_bool/array
Dec 22 09:24:31 Finished examples/pseudo_bool/array                         1h08m34s  35GB
Dec 22 09:24:32 Starting examples/pseudo_bool/array/compilation
Dec 22 09:33:14 Finished examples/pseudo_bool/array/compilation                8m40s  15GB
Dec 22 09:33:15 Starting examples/pseudo_bool/array/compilation/proofs
Dec 22 09:35:50 Finished examples/pseudo_bool/array/compilation/proofs         2m34s   6GB
Dec 22 09:35:51 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 22 09:37:04 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m12s   6GB
Dec 22 09:37:05 Starting examples/opentheory
Dec 22 09:45:40 Finished examples/opentheory                                   8m34s   5GB
Dec 22 09:45:41 Starting examples/opentheory/compilation
Dec 22 09:47:06 Finished examples/opentheory/compilation                       1m23s   5GB
Dec 22 09:47:06 Starting examples/opentheory/compilation/proofs
Dec 22 09:48:11 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Dec 22 09:48:12 Starting examples/opentheory/compilation/ag32
Dec 22 09:49:41 Finished examples/opentheory/compilation/ag32                  1m27s   5GB
Dec 22 09:49:42 Starting examples/opentheory/compilation/ag32/proofs
Dec 22 09:51:19 Finished examples/opentheory/compilation/ag32/proofs           1m36s   8GB
Dec 22 09:51:20 Starting examples/sat_encodings
Dec 22 09:52:20 Finished examples/sat_encodings                                  58s 799MB
Dec 22 09:52:21 Starting examples/sat_encodings/demo
Dec 22 09:52:22 Finished examples/sat_encodings/demo                              0s  11MB
Dec 22 09:52:22 Starting examples/sat_encodings/case_studies
Dec 22 09:54:08 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Dec 22 09:54:09 Starting examples/sat_encodings/translation
Dec 22 09:57:46 Finished examples/sat_encodings/translation                    3m35s   3GB
Dec 22 09:57:47 Starting examples/sat_encodings/translation/compilation
Dec 22 09:59:33 Finished examples/sat_encodings/translation/compilation        1m45s   4GB
Dec 22 09:59:34 Starting examples/deflate
Dec 22 10:00:01 Finished examples/deflate                                        26s 786MB
Dec 22 10:00:02 Starting examples/deflate/translation
Dec 22 10:01:08 Finished examples/deflate/translation                          1m05s   4GB
Dec 22 10:01:09 Starting examples/deflate/translation/compilation
Dec 22 10:01:58 Finished examples/deflate/translation/compilation                48s   3GB
Dec 22 10:01:59 Starting examples/vipr
Dec 22 10:05:28 Finished examples/vipr                                         3m27s   3GB
Dec 22 10:05:29 Starting examples/vipr/compilation
Dec 22 10:06:24 Finished examples/vipr/compilation                               54s   4GB
Dec 22 10:06:25 Starting translator/okasaki-examples
Dec 22 10:10:29 Finished translator/okasaki-examples                           4m03s   3GB
Dec 22 10:10:30 Starting translator/other-examples
Dec 22 10:13:36 Finished translator/other-examples                             3m04s   2GB
Dec 22 10:13:36 Starting translator/other-examples/auxiliary
Dec 22 10:13:37 Finished translator/other-examples/auxiliary                      0s  11MB
Dec 22 10:13:38 Starting compiler/parsing/tests
Dec 22 10:14:14 Finished compiler/parsing/tests                                  34s   1GB
Dec 22 10:14:15 Starting compiler/inference/tests
Dec 22 10:14:51 Finished compiler/inference/tests                                35s   2GB
Dec 22 10:14:52 Starting compiler/printing/test
Dec 22 10:16:04 Finished compiler/printing/test                                1m11s   5GB
Dec 22 10:16:05 Starting icing/flover
Dec 22 10:50:32 Finished icing/flover                                         34m25s   2GB
Dec 22 10:50:33 Starting icing/flover/Infra
Dec 22 10:50:34 Finished icing/flover/Infra                                       0s  11MB
Dec 22 10:50:35 Starting icing/flover/semantics
Dec 22 10:50:36 Finished icing/flover/semantics                                   0s  12MB
Dec 22 10:50:37 Starting icing/
Dec 22 11:17:56 Finished icing/                                               27m18s   4GB
Dec 22 11:17:57 Starting icing/examples
Dec 22 11:19:31 Finished icing/examples                                        1m32s   8GB
Dec 22 11:19:32 Starting compiler/repl
Dec 22 11:27:34 Finished compiler/repl                                         8m00s   8GB
Dec 22 11:27:35 Starting unverified/sexpr-bootstrap/x64/64
Dec 22 11:31:51 Finished unverified/sexpr-bootstrap/x64/64                     4m01s  17GB
Dec 22 11:31:52 Starting unverified/sexpr-bootstrap/x64/32
Dec 22 11:35:17 Finished unverified/sexpr-bootstrap/x64/32                     3m14s  14GB
Dec 22 11:35:18 Starting compiler/benchmarks
Dec 22 11:36:04 Finished compiler/benchmarks                                     44s 712MB
Dec 22 11:36:05 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Dec 22 11:36:08 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 243MB
Dec 22 11:36:09 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Dec 22 11:36:12 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 255MB
Dec 22 11:36:13 Starting compiler/bootstrap/compilation/x64/64
Dec 22 12:00:47 Finished compiler/bootstrap/compilation/x64/64                24m21s  81GB
Dec 22 12:00:48 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 22 12:24:44 Finished compiler/bootstrap/compilation/x64/64/proofs         23m55s  48GB
Dec 22 12:24:45 Starting compiler/bootstrap/compilation/x64/32
Dec 22 12:49:24 Finished compiler/bootstrap/compilation/x64/32                24m31s  62GB
Dec 22 12:49:25 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 22 12:53:28 Finished compiler/bootstrap/compilation/x64/32/proofs          4m02s  22GB
Dec 22 12:53:29 Starting compiler/bootstrap/compilation/arm8/64
Dec 22 13:30:14 Finished compiler/bootstrap/compilation/arm8/64               36m36s  83GB
Dec 22 13:30:15 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 22 13:35:38 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m22s  29GB
Dec 22 13:35:39 Starting compiler/bootstrap/compilation/ag32/32
Dec 22 14:01:01 Finished compiler/bootstrap/compilation/ag32/32               25m21s  46GB
Dec 22 14:01:02 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 22 14:06:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m58s  30GB
Dec 22 14:06:02 SUCCESS