Job 2732

CakeML:0d040a7cc1acd8174d7c79d7399f6f7f85734f8b
  Merge pull request #1099 from CakeML/ml_progLib_update [Dec 05 06:02:44]
HOL:7895fcf1ca55246f322a16d70fe5fea37717ede4
  Get Theorem syntax to store location information [Dec 03 07:35:38]
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 06 03:04:15 Claimed job
Dec 06 03:04:22 Reusing HOL
Dec 06 03:04:32 Starting developers
Dec 06 03:04:36 Finished developers                                               3s 200MB
Dec 06 03:04:37 Starting developers/bin
Dec 06 03:04:44 Finished developers/bin                                           5s 745MB
Dec 06 03:04:44 Starting compiler/proofs
Dec 06 04:43:58 Finished compiler/proofs                                    1h39m12s  40GB
Dec 06 04:44:00 Starting compiler/bootstrap/translation
Dec 06 10:46:10 Finished compiler/bootstrap/translation                     6h02m08s  67GB
Dec 06 10:46:11 Starting semantics/ffi
Dec 06 10:46:21 Finished semantics/ffi                                            9s 610MB
Dec 06 10:46:22 Starting semantics
Dec 06 10:46:24 Finished semantics                                                0s  53MB
Dec 06 10:46:25 Starting semantics/proofs
Dec 06 10:46:48 Finished semantics/proofs                                        22s 694MB
Dec 06 10:46:49 Starting semantics/alt_semantics
Dec 06 10:47:10 Finished semantics/alt_semantics                                 20s 904MB
Dec 06 10:47:11 Starting semantics/alt_semantics/proofs
Dec 06 10:57:23 Finished semantics/alt_semantics/proofs                       10m11s   2GB
Dec 06 10:57:24 Starting basis/pure
Dec 06 10:57:26 Finished basis/pure                                               0s  59MB
Dec 06 10:57:27 Starting translator
Dec 06 10:59:02 Finished translator                                            1m34s   2GB
Dec 06 10:59:03 Starting compiler/parsing
Dec 06 10:59:04 Finished compiler/parsing                                         0s  57MB
Dec 06 10:59:05 Starting characteristic
Dec 06 10:59:07 Finished characteristic                                           0s  88MB
Dec 06 10:59:08 Starting translator/monadic
Dec 06 10:59:09 Finished translator/monadic                                       0s  88MB
Dec 06 10:59:10 Starting basis
Dec 06 11:01:32 Finished basis                                                 2m21s   3GB
Dec 06 11:01:33 Starting compiler/inference
Dec 06 11:01:35 Finished compiler/inference                                       0s  85MB
Dec 06 11:01:36 Starting compiler/backend/reg_alloc
Dec 06 11:01:37 Finished compiler/backend/reg_alloc                               0s  53MB
Dec 06 11:01:38 Starting compiler/backend/gc
Dec 06 11:01:40 Finished compiler/backend/gc                                      1s 129MB
Dec 06 11:01:41 Starting compiler/backend
Dec 06 11:01:46 Finished compiler/backend                                         3s 265MB
Dec 06 11:01:47 Starting compiler/encoders/asm
Dec 06 11:01:48 Finished compiler/encoders/asm                                    0s  82MB
Dec 06 11:01:49 Starting compiler/encoders/x64
Dec 06 11:01:51 Finished compiler/encoders/x64                                    0s  91MB
Dec 06 11:01:52 Starting compiler/encoders/arm7
Dec 06 11:01:54 Finished compiler/encoders/arm7                                   0s  86MB
Dec 06 11:01:54 Starting compiler/encoders/arm8
Dec 06 11:01:56 Finished compiler/encoders/arm8                                   0s  86MB
Dec 06 11:01:57 Starting compiler/encoders/arm8_asl
Dec 06 11:02:55 Finished compiler/encoders/arm8_asl                              57s  20GB
Dec 06 11:02:56 Starting compiler/encoders/mips
Dec 06 11:02:57 Finished compiler/encoders/mips                                   0s  91MB
Dec 06 11:02:58 Starting compiler/encoders/riscv
Dec 06 11:03:00 Finished compiler/encoders/riscv                                  0s  84MB
Dec 06 11:03:01 Starting compiler/encoders/ag32
Dec 06 11:03:03 Finished compiler/encoders/ag32                                   0s  82MB
Dec 06 11:03:03 Starting compiler/backend/x64
Dec 06 11:03:06 Finished compiler/backend/x64                                     1s 128MB
Dec 06 11:03:06 Starting compiler/backend/arm7
Dec 06 11:03:09 Finished compiler/backend/arm7                                    1s 125MB
Dec 06 11:03:09 Starting compiler/backend/arm8
Dec 06 11:03:11 Finished compiler/backend/arm8                                    1s 122MB
Dec 06 11:03:12 Starting compiler/backend/mips
Dec 06 11:03:14 Finished compiler/backend/mips                                    1s 123MB
Dec 06 11:03:15 Starting compiler/backend/riscv
Dec 06 11:03:17 Finished compiler/backend/riscv                                   1s 122MB
Dec 06 11:03:18 Starting compiler/backend/ag32
Dec 06 11:04:24 Finished compiler/backend/ag32                                 1m05s   2GB
Dec 06 11:04:25 Starting compiler/parsing/proofs
Dec 06 11:04:27 Finished compiler/parsing/proofs                                  0s  61MB
Dec 06 11:04:28 Starting compiler/inference/proofs
Dec 06 11:04:29 Finished compiler/inference/proofs                                0s  86MB
Dec 06 11:04:30 Starting compiler/backend/semantics
Dec 06 11:07:39 Finished compiler/backend/semantics                            3m07s   2GB
Dec 06 11:07:40 Starting compiler/backend/reg_alloc/proofs
Dec 06 11:07:41 Finished compiler/backend/reg_alloc/proofs                        0s  88MB
Dec 06 11:07:42 Starting compiler/backend/proofs
Dec 06 11:08:30 Finished compiler/backend/proofs                                 47s   3GB
Dec 06 11:08:31 Starting compiler/backend/serialiser
Dec 06 11:08:33 Finished compiler/backend/serialiser                              1s 138MB
Dec 06 11:08:34 Starting compiler/encoders/x64/proofs
Dec 06 11:18:46 Finished compiler/encoders/x64/proofs                         10m10s   4GB
Dec 06 11:18:47 Starting compiler/encoders/arm7/proofs
Dec 06 11:31:55 Finished compiler/encoders/arm7/proofs                        13m07s   8GB
Dec 06 11:31:56 Starting compiler/encoders/arm8/proofs
Dec 06 11:39:05 Finished compiler/encoders/arm8/proofs                         7m08s   4GB
Dec 06 11:39:06 Starting compiler/encoders/arm8_asl/proofs
Dec 06 11:54:36 Finished compiler/encoders/arm8_asl/proofs                    15m28s   4GB
Dec 06 11:54:37 Starting compiler/encoders/mips/proofs
Dec 06 12:04:47 Finished compiler/encoders/mips/proofs                        10m08s   5GB
Dec 06 12:04:48 Starting compiler/encoders/riscv/proofs
Dec 06 12:12:58 Finished compiler/encoders/riscv/proofs                        8m09s   4GB
Dec 06 12:12:58 Starting compiler/encoders/ag32/proofs
Dec 06 12:15:50 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Dec 06 12:15:51 Starting compiler/backend/x64/proofs
Dec 06 12:16:23 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 06 12:16:24 Starting compiler/backend/arm7/proofs
Dec 06 12:16:56 Finished compiler/backend/arm7/proofs                            31s   2GB
Dec 06 12:16:57 Starting compiler/backend/arm8/proofs
Dec 06 12:17:27 Finished compiler/backend/arm8/proofs                            28s   2GB
Dec 06 12:17:28 Starting compiler/backend/arm8_asl
Dec 06 12:17:49 Finished compiler/backend/arm8_asl                               20s   2GB
Dec 06 12:17:50 Starting compiler/backend/mips/proofs
Dec 06 12:18:20 Finished compiler/backend/mips/proofs                            29s   2GB
Dec 06 12:18:21 Starting compiler/backend/riscv/proofs
Dec 06 12:18:55 Finished compiler/backend/riscv/proofs                           32s   2GB
Dec 06 12:18:56 Starting compiler/backend/ag32/proofs
Dec 06 12:32:36 Finished compiler/backend/ag32/proofs                         13m39s   5GB
Dec 06 12:32:37 Starting compiler/backend/cv_compute
Dec 06 12:33:44 Finished compiler/backend/cv_compute                           1m05s   1GB
Dec 06 12:33:45 Starting cv_translator
Dec 06 12:51:23 Finished cv_translator                                        17m36s   8GB
Dec 06 12:51:23 Starting candle/set-theory
Dec 06 12:51:59 Finished candle/set-theory                                       34s   1GB
Dec 06 12:52:00 Starting candle/syntax-lib
Dec 06 12:52:01 Finished candle/syntax-lib                                        0s  59MB
Dec 06 12:52:02 Starting candle/standard/syntax
Dec 06 12:52:14 Finished candle/standard/syntax                                  11s 790MB
Dec 06 12:52:15 Starting candle/standard/semantics
Dec 06 12:54:21 Finished candle/standard/semantics                             2m05s   2GB
Dec 06 12:54:22 Starting candle/standard/monadic
Dec 06 12:54:24 Finished candle/standard/monadic                                  0s  92MB
Dec 06 12:54:25 Starting candle/standard/ml_kernel
Dec 06 12:56:09 Finished candle/standard/ml_kernel                             1m43s   4GB
Dec 06 12:56:10 Starting candle/overloading/syntax
Dec 06 12:59:25 Finished candle/overloading/syntax                             3m13s   2GB
Dec 06 12:59:26 Starting candle/overloading/semantics
Dec 06 13:10:42 Finished candle/overloading/semantics                         11m15s  10GB
Dec 06 13:10:43 Starting candle/overloading/monadic
Dec 06 13:12:59 Finished candle/overloading/monadic                            2m15s   2GB
Dec 06 13:13:00 Starting candle/overloading/ml_kernel
Dec 06 13:20:11 Finished candle/overloading/ml_kernel                          7m10s   5GB
Dec 06 13:20:12 Starting candle/overloading/ml_checker
Dec 06 13:22:46 Finished candle/overloading/ml_checker                         2m32s   6GB
Dec 06 13:22:47 Starting candle/prover
Dec 06 13:32:27 Finished candle/prover                                         9m39s   5GB
Dec 06 13:32:28 Starting pancake
Dec 06 13:32:50 Finished pancake                                                 21s 825MB
Dec 06 13:32:51 Starting pancake/ffi
Dec 06 13:32:52 Finished pancake/ffi                                              0s  11MB
Dec 06 13:32:53 Starting pancake/semantics
Dec 06 13:35:05 Finished pancake/semantics                                     2m10s   1GB
Dec 06 13:35:05 Starting pancake/parser
Dec 06 13:35:30 Finished pancake/parser                                          23s 429MB
Dec 06 13:35:31 Starting pancake/proofs
Dec 06 13:51:46 Finished pancake/proofs                                       16m13s   6GB
Dec 06 13:51:47 Starting compiler/dafny
Dec 06 13:54:24 Finished compiler/dafny                                        2m36s  11GB
Dec 06 13:54:25 Starting compiler/dafny/translation
Dec 06 14:11:45 Finished compiler/dafny/translation                           17m17s  22GB
Dec 06 14:11:46 Starting compiler/dafny/compilation
Dec 06 14:14:13 Finished compiler/dafny/compilation                            2m26s   8GB
Dec 06 14:14:14 Starting compiler/dafny/semantics
Dec 06 14:14:50 Finished compiler/dafny/semantics                                35s   1GB
Dec 06 14:14:51 Starting characteristic/examples
Dec 06 14:16:16 Finished characteristic/examples                               1m24s   4GB
Dec 06 14:16:17 Starting tutorial/solutions
Dec 06 14:18:38 Finished tutorial/solutions                                    2m19s   3GB
Dec 06 14:18:38 Starting translator/monadic/examples
Dec 06 14:21:31 Finished translator/monadic/examples                           2m51s   3GB
Dec 06 14:21:32 Starting examples
Dec 06 14:27:26 Finished examples                                              5m53s   5GB
Dec 06 14:27:27 Starting examples/compilation/x64
Dec 06 14:34:31 Finished examples/compilation/x64                              7m03s   5GB
Dec 06 14:34:32 Starting examples/compilation/x64/proofs
Dec 06 14:36:52 Finished examples/compilation/x64/proofs                       2m19s   3GB
Dec 06 14:36:53 Starting examples/compilation/ag32
Dec 06 14:38:38 Finished examples/compilation/ag32                             1m44s   3GB
Dec 06 14:38:39 Starting examples/compilation/ag32/proofs
Dec 06 14:39:35 Finished examples/compilation/ag32/proofs                        54s   4GB
Dec 06 14:39:35 Starting examples/compilation/to_word
Dec 06 14:42:50 Finished examples/compilation/to_word                          3m14s  11GB
Dec 06 14:42:51 Starting examples/lpr_checker
Dec 06 14:43:21 Finished examples/lpr_checker                                    28s   1GB
Dec 06 14:43:22 Starting examples/lpr_checker/array
Dec 06 15:10:14 Finished examples/lpr_checker/array                           26m51s  28GB
Dec 06 15:10:15 Starting examples/lpr_checker/array/compilation
Dec 06 15:12:03 Finished examples/lpr_checker/array/compilation                1m47s   7GB
Dec 06 15:12:04 Starting examples/lpr_checker/array/compilation/proofs
Dec 06 15:13:14 Finished examples/lpr_checker/array/compilation/proofs         1m09s   6GB
Dec 06 15:13:15 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 06 15:14:21 Finished examples/lpr_checker/array/compilation/proofsARM8     1m04s   6GB
Dec 06 15:14:22 Starting .
Dec 06 15:14:26 Finished .                                                        2s 286MB
Dec 06 15:14:27 Starting examples/xlrup_checker
Dec 06 15:15:00 Finished examples/xlrup_checker                                  33s   1GB
Dec 06 15:15:01 Starting examples/xlrup_checker/array
Dec 06 15:28:24 Finished examples/xlrup_checker/array                         13m21s  11GB
Dec 06 15:28:25 Starting examples/xlrup_checker/array/compilation
Dec 06 15:29:23 Finished examples/xlrup_checker/array/compilation                57s   4GB
Dec 06 15:29:24 Starting examples/xlrup_checker/array/compilation/proofs
Dec 06 15:30:22 Finished examples/xlrup_checker/array/compilation/proofs         56s   4GB
Dec 06 15:30:23 Starting examples/pseudo_bool
Dec 06 15:31:52 Finished examples/pseudo_bool                                  1m28s   2GB
Dec 06 15:31:53 Starting examples/pseudo_bool/cnf_encoding
Dec 06 15:32:22 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
Dec 06 15:32:22 Starting examples/pseudo_bool/graph_encoding
Dec 06 15:33:05 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Dec 06 15:33:06 Starting examples/pseudo_bool/array
Dec 06 16:42:04 Finished examples/pseudo_bool/array                         1h08m57s  23GB
Dec 06 16:42:05 Starting examples/pseudo_bool/array/compilation
Dec 06 16:50:38 Finished examples/pseudo_bool/array/compilation                8m31s  16GB
Dec 06 16:50:39 Starting examples/pseudo_bool/array/compilation/proofs
Dec 06 16:53:13 Finished examples/pseudo_bool/array/compilation/proofs         2m32s   6GB
Dec 06 16:53:14 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 06 16:54:26 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m11s   6GB
Dec 06 16:54:27 Starting examples/opentheory
Dec 06 17:02:48 Finished examples/opentheory                                   8m20s   4GB
Dec 06 17:02:49 Starting examples/opentheory
Dec 06 17:02:51 Finished examples/opentheory                                      1s 121MB
Dec 06 17:02:52 Starting examples/opentheory/compilation
Dec 06 17:04:20 Finished examples/opentheory/compilation                       1m26s   5GB
Dec 06 17:04:20 Starting examples/opentheory/compilation/proofs
Dec 06 17:05:18 Finished examples/opentheory/compilation/proofs                  56s   3GB
Dec 06 17:05:19 Starting examples/opentheory/compilation/ag32
Dec 06 17:06:42 Finished examples/opentheory/compilation/ag32                  1m22s   5GB
Dec 06 17:06:43 Starting examples/opentheory/compilation/ag32/proofs
Dec 06 17:08:18 Finished examples/opentheory/compilation/ag32/proofs           1m33s   7GB
Dec 06 17:08:19 Starting examples/sat_encodings
Dec 06 17:09:18 Finished examples/sat_encodings                                  59s 816MB
Dec 06 17:09:19 Starting examples/sat_encodings/case_studies
Dec 06 17:11:05 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Dec 06 17:11:06 Starting examples/sat_encodings/translation
Dec 06 17:14:33 Finished examples/sat_encodings/translation                    3m25s   3GB
Dec 06 17:14:33 Starting examples/sat_encodings/translation/compilation
Dec 06 17:16:20 Finished examples/sat_encodings/translation/compilation        1m46s   4GB
Dec 06 17:16:21 Starting examples/deflate
Dec 06 17:16:49 Finished examples/deflate                                        26s 732MB
Dec 06 17:16:50 Starting examples/deflate/translation
Dec 06 17:17:46 Finished examples/deflate/translation                            55s   2GB
Dec 06 17:17:47 Starting examples/deflate/translation/compilation
Dec 06 17:18:36 Finished examples/deflate/translation/compilation                48s   3GB
Dec 06 17:18:37 Starting examples/vipr
Dec 06 17:22:14 Finished examples/vipr                                         3m35s   7GB
Dec 06 17:22:15 Starting examples/vipr/compilation
Dec 06 17:23:09 Finished examples/vipr/compilation                               53s   4GB
Dec 06 17:23:10 Starting translator/okasaki-examples
Dec 06 17:27:12 Finished translator/okasaki-examples                           4m01s   3GB
Dec 06 17:27:13 Starting translator/other-examples
Dec 06 17:28:05 Finished translator/other-examples                               51s   2GB
Dec 06 17:28:06 Starting compiler/parsing/tests
Dec 06 17:28:38 Finished compiler/parsing/tests                                  31s   1GB
Dec 06 17:28:39 Starting compiler/inference/tests
Dec 06 17:29:13 Finished compiler/inference/tests                                32s   2GB
Dec 06 17:29:14 Starting compiler/printing/test
Dec 06 17:30:26 Finished compiler/printing/test                                1m11s   5GB
Dec 06 17:30:27 Starting icing/flover
Dec 06 18:05:04 Finished icing/flover                                         34m36s   1GB
Dec 06 18:05:05 Starting icing/
Dec 06 18:32:17 Finished icing/                                               27m10s   4GB
Dec 06 18:32:17 Starting icing/examples
Dec 06 18:33:50 Finished icing/examples                                        1m31s   8GB
Dec 06 18:33:51 Starting compiler/repl
Dec 06 18:41:51 Finished compiler/repl                                         7m59s   8GB
Dec 06 18:41:52 Starting unverified/sexpr-bootstrap/x64/64
Dec 06 18:46:02 Finished unverified/sexpr-bootstrap/x64/64                     3m55s  16GB
Dec 06 18:46:02 Starting unverified/sexpr-bootstrap/x64/32
Dec 06 18:49:20 Finished unverified/sexpr-bootstrap/x64/32                     3m07s  16GB
Dec 06 18:49:21 Starting compiler/benchmarks
Dec 06 18:50:07 Finished compiler/benchmarks                                     44s 712MB
Dec 06 18:50:08 Starting compiler/bootstrap/compilation/x64/64
Dec 06 19:14:42 Finished compiler/bootstrap/compilation/x64/64                24m20s  84GB
Dec 06 19:14:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 06 19:39:15 Finished compiler/bootstrap/compilation/x64/64/proofs         24m31s  55GB
Dec 06 19:39:16 Starting compiler/bootstrap/compilation/x64/32
Dec 06 20:04:18 Finished compiler/bootstrap/compilation/x64/32                24m53s  67GB
Dec 06 20:04:19 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 06 20:08:37 Finished compiler/bootstrap/compilation/x64/32/proofs          4m17s  24GB
Dec 06 20:08:38 Starting compiler/bootstrap/compilation/arm8/64
Dec 06 20:44:51 Finished compiler/bootstrap/compilation/arm8/64               36m04s  93GB
Dec 06 20:44:52 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 06 20:50:16 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m22s  30GB
Dec 06 20:50:16 Starting compiler/bootstrap/compilation/ag32/32
Dec 06 21:14:55 Finished compiler/bootstrap/compilation/ag32/32               24m37s  49GB
Dec 06 21:14:56 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 06 21:19:53 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m56s  32GB
Dec 06 21:19:54 SUCCESS