Job 2730

CakeML:fe784de7666765cf232387d71617f0d8e1c89eb8
  Remove examples/bot + Fix Holmakefile [Nov 26 19:13:32]
#1092 (cost)
Merging into:d0fd8fe2625d24ae005b57d0f413f010ed38f194
  Fix some more uses of DB [Dec 02 08:50:38]
HOL:7895fcf1ca55246f322a16d70fe5fea37717ede4
  Get Theorem syntax to store location information [Dec 03 07:35:38]
Machine:lammmington

Dec 05 05:31:01 Claimed job
Dec 05 05:31:08 Building HOL
Dec 05 05:41:58 Starting developers
Dec 05 05:42:02 Finished developers                                               3s 189MB
Dec 05 05:42:03 Starting developers/bin
Dec 05 05:42:10 Finished developers/bin                                           5s 746MB
Dec 05 05:42:11 Starting compiler/proofs
Dec 05 07:23:57 Finished compiler/proofs                                    1h41m45s  42GB
Dec 05 07:23:58 Starting compiler/bootstrap/translation
Dec 05 16:24:28 Finished compiler/bootstrap/translation                     9h00m28s  57GB
Dec 05 16:24:28 Starting semantics/ffi
Dec 05 16:24:39 Finished semantics/ffi                                            9s 589MB
Dec 05 16:24:40 Starting semantics
Dec 05 16:24:41 Finished semantics                                                0s  53MB
Dec 05 16:24:42 Starting semantics/proofs
Dec 05 16:25:05 Finished semantics/proofs                                        22s 885MB
Dec 05 16:25:06 Starting semantics/alt_semantics
Dec 05 16:25:26 Finished semantics/alt_semantics                                 19s 898MB
Dec 05 16:25:27 Starting semantics/alt_semantics/proofs
Dec 05 16:35:40 Finished semantics/alt_semantics/proofs                       10m12s   2GB
Dec 05 16:35:41 Starting basis/pure
Dec 05 16:35:43 Finished basis/pure                                               0s  61MB
Dec 05 16:35:44 Starting translator
Dec 05 16:37:21 Finished translator                                            1m36s   2GB
Dec 05 16:37:22 Starting compiler/parsing
Dec 05 16:37:24 Finished compiler/parsing                                         0s  57MB
Dec 05 16:37:25 Starting characteristic
Dec 05 16:37:26 Finished characteristic                                           0s  82MB
Dec 05 16:37:27 Starting translator/monadic
Dec 05 16:37:29 Finished translator/monadic                                       0s  89MB
Dec 05 16:37:30 Starting basis
Dec 05 16:39:52 Finished basis                                                 2m21s   4GB
Dec 05 16:39:53 Starting compiler/inference
Dec 05 16:39:55 Finished compiler/inference                                       0s  86MB
Dec 05 16:39:56 Starting compiler/backend/reg_alloc
Dec 05 16:39:57 Finished compiler/backend/reg_alloc                               0s  53MB
Dec 05 16:39:58 Starting compiler/backend/gc
Dec 05 16:40:00 Finished compiler/backend/gc                                      1s 132MB
Dec 05 16:40:01 Starting compiler/backend
Dec 05 16:40:05 Finished compiler/backend                                         3s 242MB
Dec 05 16:40:06 Starting compiler/encoders/asm
Dec 05 16:40:08 Finished compiler/encoders/asm                                    0s  78MB
Dec 05 16:40:09 Starting compiler/encoders/x64
Dec 05 16:40:11 Finished compiler/encoders/x64                                    0s  86MB
Dec 05 16:40:11 Starting compiler/encoders/arm7
Dec 05 16:40:13 Finished compiler/encoders/arm7                                   0s  90MB
Dec 05 16:40:14 Starting compiler/encoders/arm8
Dec 05 16:40:16 Finished compiler/encoders/arm8                                   0s  88MB
Dec 05 16:40:17 Starting compiler/encoders/arm8_asl
Dec 05 18:40:29 Finished compiler/encoders/arm8_asl                         2h00m11s  41GB
Dec 05 18:40:30 Starting compiler/encoders/mips
Dec 05 18:40:32 Finished compiler/encoders/mips                                   0s  90MB
Dec 05 18:40:32 Starting compiler/encoders/riscv
Dec 05 18:40:34 Finished compiler/encoders/riscv                                  0s  90MB
Dec 05 18:40:35 Starting compiler/encoders/ag32
Dec 05 18:40:37 Finished compiler/encoders/ag32                                   0s  79MB
Dec 05 18:40:38 Starting compiler/backend/x64
Dec 05 18:40:40 Finished compiler/backend/x64                                     1s 135MB
Dec 05 18:40:41 Starting compiler/backend/arm7
Dec 05 18:40:43 Finished compiler/backend/arm7                                    1s 123MB
Dec 05 18:40:44 Starting compiler/backend/arm8
Dec 05 18:40:46 Finished compiler/backend/arm8                                    1s 123MB
Dec 05 18:40:46 Starting compiler/backend/mips
Dec 05 18:40:49 Finished compiler/backend/mips                                    1s 123MB
Dec 05 18:40:49 Starting compiler/backend/riscv
Dec 05 18:40:51 Finished compiler/backend/riscv                                   1s 121MB
Dec 05 18:40:52 Starting compiler/backend/ag32
Dec 05 18:42:01 Finished compiler/backend/ag32                                 1m07s   1GB
Dec 05 18:42:02 Starting compiler/parsing/proofs
Dec 05 18:42:03 Finished compiler/parsing/proofs                                  0s  65MB
Dec 05 18:42:04 Starting compiler/inference/proofs
Dec 05 18:42:06 Finished compiler/inference/proofs                                0s  85MB
Dec 05 18:42:07 Starting compiler/backend/semantics
Dec 05 18:45:15 Finished compiler/backend/semantics                            3m06s   2GB
Dec 05 18:45:16 Starting compiler/backend/reg_alloc/proofs
Dec 05 18:45:17 Finished compiler/backend/reg_alloc/proofs                        0s  88MB
Dec 05 18:45:18 Starting compiler/backend/proofs
Dec 05 18:46:05 Finished compiler/backend/proofs                                 45s   2GB
Dec 05 18:46:06 Starting compiler/backend/serialiser
Dec 05 18:46:08 Finished compiler/backend/serialiser                              1s 137MB
Dec 05 18:46:09 Starting compiler/encoders/x64/proofs
Dec 05 18:56:18 Finished compiler/encoders/x64/proofs                         10m08s   5GB
Dec 05 18:56:19 Starting compiler/encoders/arm7/proofs
Dec 05 19:09:10 Finished compiler/encoders/arm7/proofs                        12m50s   5GB
Dec 05 19:09:11 Starting compiler/encoders/arm8/proofs
Dec 05 19:16:10 Finished compiler/encoders/arm8/proofs                         6m57s   4GB
Dec 05 19:16:11 Starting compiler/encoders/arm8_asl/proofs
Dec 05 20:05:28 Finished compiler/encoders/arm8_asl/proofs                    49m15s  20GB
Dec 05 20:05:29 Starting compiler/encoders/mips/proofs
Dec 05 20:15:52 Finished compiler/encoders/mips/proofs                        10m22s   7GB
Dec 05 20:15:53 Starting compiler/encoders/riscv/proofs
Dec 05 20:24:06 Finished compiler/encoders/riscv/proofs                        8m11s   4GB
Dec 05 20:24:07 Starting compiler/encoders/ag32/proofs
Dec 05 20:26:58 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Dec 05 20:26:59 Starting compiler/backend/x64/proofs
Dec 05 20:27:31 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 05 20:27:32 Starting compiler/backend/arm7/proofs
Dec 05 20:28:03 Finished compiler/backend/arm7/proofs                            29s   2GB
Dec 05 20:28:03 Starting compiler/backend/arm8/proofs
Dec 05 20:28:36 Finished compiler/backend/arm8/proofs                            32s   2GB
Dec 05 20:28:37 Starting compiler/backend/arm8_asl
Dec 05 20:28:59 Finished compiler/backend/arm8_asl                               20s   2GB
Dec 05 20:28:59 Starting compiler/backend/mips/proofs
Dec 05 20:29:30 Finished compiler/backend/mips/proofs                            29s   2GB
Dec 05 20:29:31 Starting compiler/backend/riscv/proofs
Dec 05 20:30:05 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 05 20:30:05 Starting compiler/backend/ag32/proofs
Dec 05 20:43:31 Finished compiler/backend/ag32/proofs                         13m24s   4GB
Dec 05 20:43:32 Starting compiler/backend/cv_compute
Dec 05 20:44:40 Finished compiler/backend/cv_compute                           1m07s   1GB
Dec 05 20:44:41 Starting cv_translator
Dec 05 21:01:57 Finished cv_translator                                        17m14s   8GB
Dec 05 21:01:58 Starting candle/set-theory
Dec 05 21:02:33 Finished candle/set-theory                                       34s   1GB
Dec 05 21:02:34 Starting candle/syntax-lib
Dec 05 21:02:35 Finished candle/syntax-lib                                        0s  59MB
Dec 05 21:02:36 Starting candle/standard/syntax
Dec 05 21:02:49 Finished candle/standard/syntax                                  11s 776MB
Dec 05 21:02:50 Starting candle/standard/semantics
Dec 05 21:04:49 Finished candle/standard/semantics                             1m58s   2GB
Dec 05 21:04:50 Starting candle/standard/monadic
Dec 05 21:04:52 Finished candle/standard/monadic                                  0s  88MB
Dec 05 21:04:53 Starting candle/standard/ml_kernel
Dec 05 21:06:36 Finished candle/standard/ml_kernel                             1m42s   3GB
Dec 05 21:06:37 Starting candle/overloading/syntax
Dec 05 21:09:49 Finished candle/overloading/syntax                             3m10s   2GB
Dec 05 21:09:50 Starting candle/overloading/semantics
Dec 05 21:20:33 Finished candle/overloading/semantics                         10m42s   4GB
Dec 05 21:20:34 Starting candle/overloading/monadic
Dec 05 21:22:54 Finished candle/overloading/monadic                            2m19s   2GB
Dec 05 21:22:55 Starting candle/overloading/ml_kernel
Dec 05 21:30:20 Finished candle/overloading/ml_kernel                          7m24s   6GB
Dec 05 21:30:21 Starting candle/overloading/ml_checker
Dec 05 21:32:53 Finished candle/overloading/ml_checker                         2m30s   6GB
Dec 05 21:32:54 Starting candle/prover
Dec 05 21:42:10 Finished candle/prover                                         9m15s   5GB
Dec 05 21:42:11 Starting pancake
Dec 05 21:42:33 Finished pancake                                                 20s 688MB
Dec 05 21:42:33 Starting pancake/ffi
Dec 05 21:42:34 Finished pancake/ffi                                              0s  11MB
Dec 05 21:42:35 Starting pancake/semantics
Dec 05 21:44:44 Finished pancake/semantics                                     2m07s   2GB
Dec 05 21:44:45 Starting pancake/parser
Dec 05 21:45:08 Finished pancake/parser                                          22s 473MB
Dec 05 21:45:09 Starting pancake/proofs
Dec 05 22:00:56 Finished pancake/proofs                                       15m45s   7GB
Dec 05 22:00:57 Starting compiler/dafny
Dec 05 22:03:36 Finished compiler/dafny                                        2m38s   8GB
Dec 05 22:03:37 Starting compiler/dafny/translation
Dec 05 22:32:44 Finished compiler/dafny/translation                           29m06s  16GB
Dec 05 22:32:45 Starting compiler/dafny/compilation
Dec 05 22:35:17 Finished compiler/dafny/compilation                            2m30s   9GB
Dec 05 22:35:17 Starting compiler/dafny/semantics
Dec 05 22:35:54 Finished compiler/dafny/semantics                                35s   1GB
Dec 05 22:35:54 Starting characteristic/examples
Dec 05 22:37:17 Finished characteristic/examples                               1m21s   4GB
Dec 05 22:37:18 Starting tutorial/solutions
Dec 05 22:39:41 Finished tutorial/solutions                                    2m22s   3GB
Dec 05 22:39:42 Starting translator/monadic/examples
Dec 05 22:42:38 Finished translator/monadic/examples                           2m54s   4GB
Dec 05 22:42:39 Starting examples
Dec 05 22:55:04 Finished examples                                             12m24s   3GB
Dec 05 22:55:05 Starting examples/compilation/x64
Dec 05 23:02:13 Finished examples/compilation/x64                              7m06s   4GB
Dec 05 23:02:14 Starting examples/compilation/x64/proofs
Dec 05 23:04:31 Finished examples/compilation/x64/proofs                       2m16s   3GB
Dec 05 23:04:32 Starting examples/compilation/ag32
Dec 05 23:06:19 Finished examples/compilation/ag32                             1m45s   3GB
Dec 05 23:06:19 Starting examples/compilation/ag32/proofs
Dec 05 23:07:17 Finished examples/compilation/ag32/proofs                        57s   5GB
Dec 05 23:07:18 Starting examples/compilation/to_word
Dec 05 23:10:19 Finished examples/compilation/to_word                          3m00s   4GB
Dec 05 23:10:20 Starting examples/lpr_checker
Dec 05 23:10:51 Finished examples/lpr_checker                                    29s   1GB
Dec 05 23:10:52 Starting examples/lpr_checker/array
Dec 05 23:37:26 Finished examples/lpr_checker/array                           26m33s  23GB
Dec 05 23:37:27 Starting examples/lpr_checker/array/compilation
Dec 05 23:39:16 Finished examples/lpr_checker/array/compilation                1m48s   7GB
Dec 05 23:39:17 Starting examples/lpr_checker/array/compilation/proofs
Dec 05 23:40:21 Finished examples/lpr_checker/array/compilation/proofs         1m03s   6GB
Dec 05 23:40:22 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 05 23:41:26 Finished examples/lpr_checker/array/compilation/proofsARM8     1m03s   6GB
Dec 05 23:41:27 Starting .
Dec 05 23:41:31 Finished .                                                        2s 291MB
Dec 05 23:41:32 Starting examples/xlrup_checker
Dec 05 23:42:06 Finished examples/xlrup_checker                                  33s   1GB
Dec 05 23:42:06 Starting examples/xlrup_checker/array
Dec 05 23:55:18 Finished examples/xlrup_checker/array                         13m10s   9GB
Dec 05 23:55:19 Starting examples/xlrup_checker/array/compilation
Dec 05 23:56:17 Finished examples/xlrup_checker/array/compilation                57s   4GB
Dec 05 23:56:18 Starting examples/xlrup_checker/array/compilation/proofs
Dec 05 23:57:13 Finished examples/xlrup_checker/array/compilation/proofs         54s   4GB
Dec 05 23:57:14 Starting examples/pseudo_bool
Dec 05 23:58:44 Finished examples/pseudo_bool                                  1m29s   2GB
Dec 05 23:58:45 Starting examples/pseudo_bool/cnf_encoding
Dec 05 23:59:15 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Dec 05 23:59:16 Starting examples/pseudo_bool/graph_encoding
Dec 06 00:00:00 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 06 00:00:01 Starting examples/pseudo_bool/array
Dec 06 01:08:39 Finished examples/pseudo_bool/array                         1h08m36s  32GB
Dec 06 01:08:40 Starting examples/pseudo_bool/array/compilation
Dec 06 01:17:12 Finished examples/pseudo_bool/array/compilation                8m31s  15GB
Dec 06 01:17:13 Starting examples/pseudo_bool/array/compilation/proofs
Dec 06 01:19:43 Finished examples/pseudo_bool/array/compilation/proofs         2m28s   6GB
Dec 06 01:19:44 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 06 01:20:50 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m05s   6GB
Dec 06 01:20:51 Starting examples/opentheory
Dec 06 01:29:27 Finished examples/opentheory                                   8m35s   4GB
Dec 06 01:29:28 Starting examples/opentheory
Dec 06 01:29:30 Finished examples/opentheory                                      1s 121MB
Dec 06 01:29:31 Starting examples/opentheory/compilation
Dec 06 01:30:52 Finished examples/opentheory/compilation                       1m20s   5GB
Dec 06 01:30:53 Starting examples/opentheory/compilation/proofs
Dec 06 01:31:53 Finished examples/opentheory/compilation/proofs                  59s   4GB
Dec 06 01:31:54 Starting examples/opentheory/compilation/ag32
Dec 06 01:33:26 Finished examples/opentheory/compilation/ag32                  1m31s   4GB
Dec 06 01:33:27 Starting examples/opentheory/compilation/ag32/proofs
Dec 06 01:35:02 Finished examples/opentheory/compilation/ag32/proofs           1m33s   7GB
Dec 06 01:35:03 Starting examples/sat_encodings
Dec 06 01:36:01 Finished examples/sat_encodings                                  57s 873MB
Dec 06 01:36:02 Starting examples/sat_encodings/case_studies
Dec 06 01:37:46 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Dec 06 01:37:47 Starting examples/sat_encodings/translation
Dec 06 01:41:22 Finished examples/sat_encodings/translation                    3m34s   3GB
Dec 06 01:41:23 Starting examples/sat_encodings/translation/compilation
Dec 06 01:43:10 Finished examples/sat_encodings/translation/compilation        1m45s   4GB
Dec 06 01:43:11 Starting examples/deflate
Dec 06 01:43:38 Finished examples/deflate                                        26s 754MB
Dec 06 01:43:39 Starting examples/deflate/translation
Dec 06 01:44:38 Finished examples/deflate/translation                            58s   2GB
Dec 06 01:44:39 Starting examples/deflate/translation/compilation
Dec 06 01:45:25 Finished examples/deflate/translation/compilation                45s   3GB
Dec 06 01:45:26 Starting examples/vipr
Dec 06 01:48:58 Finished examples/vipr                                         3m31s   3GB
Dec 06 01:48:59 Starting examples/vipr/compilation
Dec 06 01:49:52 Finished examples/vipr/compilation                               52s   3GB
Dec 06 01:49:53 Starting translator/okasaki-examples
Dec 06 01:53:54 Finished translator/okasaki-examples                           3m59s   4GB
Dec 06 01:53:55 Starting translator/other-examples
Dec 06 01:56:57 Finished translator/other-examples                             3m00s   3GB
Dec 06 01:56:58 Starting compiler/parsing/tests
Dec 06 01:57:29 Finished compiler/parsing/tests                                  31s   1GB
Dec 06 01:57:30 Starting compiler/inference/tests
Dec 06 01:58:06 Finished compiler/inference/tests                                34s   2GB
Dec 06 01:58:07 Starting compiler/printing/test
Dec 06 01:59:32 Finished compiler/printing/test                                1m24s   3GB
Dec 06 01:59:33 Starting icing/flover
Dec 06 02:33:44 Finished icing/flover                                         34m09s   1GB
Dec 06 02:33:45 Starting icing/
Dec 06 03:01:12 Finished icing/                                               27m25s   7GB
Dec 06 03:01:12 Starting icing/examples
Dec 06 03:02:44 Finished icing/examples                                        1m30s   7GB
Dec 06 03:02:45 Starting compiler/repl
Dec 06 03:10:53 Finished compiler/repl                                         8m06s   8GB
Dec 06 03:10:53 Starting unverified/sexpr-bootstrap/x64/64
Dec 06 03:14:56 Finished unverified/sexpr-bootstrap/x64/64                     4m01s  18GB
Dec 06 03:14:57 Starting unverified/sexpr-bootstrap/x64/32
Dec 06 03:18:18 Finished unverified/sexpr-bootstrap/x64/32                     3m20s  16GB
Dec 06 03:18:19 Starting compiler/benchmarks
Dec 06 03:19:06 Finished compiler/benchmarks                                     45s 711MB
Dec 06 03:19:06 Starting compiler/bootstrap/compilation/x64/64
Dec 06 03:41:26 Finished compiler/bootstrap/compilation/x64/64                22m18s  63GB
Dec 06 03:41:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 06 04:05:10 Finished compiler/bootstrap/compilation/x64/64/proofs         23m42s  55GB
Dec 06 04:05:11 Starting compiler/bootstrap/compilation/x64/32
Dec 06 04:29:50 Finished compiler/bootstrap/compilation/x64/32                24m38s  69GB
Dec 06 04:29:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 06 04:34:02 Finished compiler/bootstrap/compilation/x64/32/proofs          4m09s  24GB
Dec 06 04:34:03 Starting compiler/bootstrap/compilation/arm8/64
Dec 06 05:10:05 Finished compiler/bootstrap/compilation/arm8/64               36m01s  92GB
Dec 06 05:10:06 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 06 05:15:05 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m58s  29GB
Dec 06 05:15:06 Starting compiler/bootstrap/compilation/ag32/32
Dec 06 05:39:40 Finished compiler/bootstrap/compilation/ag32/32               24m32s  53GB
Dec 06 05:39:41 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 06 05:44:42 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m59s  29GB
Dec 06 05:44:42 SUCCESS