Job 2728

CakeML:cf888d1f25d6978a0015ae88c7b6751cf450f891
  Improve build-everything.py [Nov 27 09:24:04]
#1099 (ml_progLib_update)
Merging into:d0fd8fe2625d24ae005b57d0f413f010ed38f194
  Fix some more uses of DB [Dec 02 08:50:38]
HOL:170d36c740894aae4921820ec897176f62a29452
  Minor tweaks to hol-mode's configuration of comint [Nov 30 02:48:13]
Machine:lammmington

Dec 03 14:20:19 Claimed job
Dec 03 14:20:26 Building HOL
Dec 03 14:31:28 Starting developers
Dec 03 14:31:32 Finished developers                                               3s 227MB
Dec 03 14:31:33 Starting developers/bin
Dec 03 14:31:37 Finished developers/bin                                           4s 746MB
Dec 03 14:31:38 Starting compiler/proofs
Dec 03 16:14:57 Finished compiler/proofs                                    1h43m17s  42GB
Dec 03 16:14:58 Starting compiler/bootstrap/translation
Dec 03 22:05:13 Finished compiler/bootstrap/translation                     5h50m13s  63GB
Dec 03 22:05:14 Starting semantics/ffi
Dec 03 22:05:23 Finished semantics/ffi                                            8s 623MB
Dec 03 22:05:24 Starting semantics
Dec 03 22:05:25 Finished semantics                                                0s  53MB
Dec 03 22:05:26 Starting semantics/proofs
Dec 03 22:05:50 Finished semantics/proofs                                        22s 679MB
Dec 03 22:05:51 Starting semantics/alt_semantics
Dec 03 22:06:11 Finished semantics/alt_semantics                                 19s 896MB
Dec 03 22:06:12 Starting semantics/alt_semantics/proofs
Dec 03 22:16:28 Finished semantics/alt_semantics/proofs                       10m14s   2GB
Dec 03 22:16:29 Starting basis/pure
Dec 03 22:16:30 Finished basis/pure                                               0s  59MB
Dec 03 22:16:31 Starting translator
Dec 03 22:18:04 Finished translator                                            1m31s   2GB
Dec 03 22:18:05 Starting compiler/parsing
Dec 03 22:18:06 Finished compiler/parsing                                         0s  57MB
Dec 03 22:18:07 Starting characteristic
Dec 03 22:18:09 Finished characteristic                                           0s  84MB
Dec 03 22:18:10 Starting translator/monadic
Dec 03 22:18:11 Finished translator/monadic                                       0s  88MB
Dec 03 22:18:12 Starting basis
Dec 03 22:20:31 Finished basis                                                 2m17s   4GB
Dec 03 22:20:31 Starting compiler/inference
Dec 03 22:20:33 Finished compiler/inference                                       0s  85MB
Dec 03 22:20:34 Starting compiler/backend/reg_alloc
Dec 03 22:20:35 Finished compiler/backend/reg_alloc                               0s  56MB
Dec 03 22:20:36 Starting compiler/backend/gc
Dec 03 22:20:38 Finished compiler/backend/gc                                      1s 126MB
Dec 03 22:20:39 Starting compiler/backend
Dec 03 22:20:44 Finished compiler/backend                                         3s 256MB
Dec 03 22:20:45 Starting compiler/encoders/asm
Dec 03 22:20:47 Finished compiler/encoders/asm                                    0s  86MB
Dec 03 22:20:48 Starting compiler/encoders/x64
Dec 03 22:20:49 Finished compiler/encoders/x64                                    0s  84MB
Dec 03 22:20:50 Starting compiler/encoders/arm7
Dec 03 22:20:52 Finished compiler/encoders/arm7                                   0s  90MB
Dec 03 22:20:53 Starting compiler/encoders/arm8
Dec 03 22:20:54 Finished compiler/encoders/arm8                                   0s  89MB
Dec 03 22:20:55 Starting compiler/encoders/arm8_asl
Dec 04 00:21:41 Finished compiler/encoders/arm8_asl                         2h00m44s  38GB
Dec 04 00:21:42 Starting compiler/encoders/mips
Dec 04 00:21:44 Finished compiler/encoders/mips                                   0s  84MB
Dec 04 00:21:45 Starting compiler/encoders/riscv
Dec 04 00:21:47 Finished compiler/encoders/riscv                                  0s  84MB
Dec 04 00:21:48 Starting compiler/encoders/ag32
Dec 04 00:21:49 Finished compiler/encoders/ag32                                   0s  82MB
Dec 04 00:21:50 Starting compiler/backend/x64
Dec 04 00:21:52 Finished compiler/backend/x64                                     1s 123MB
Dec 04 00:21:53 Starting compiler/backend/arm7
Dec 04 00:21:55 Finished compiler/backend/arm7                                    1s 123MB
Dec 04 00:21:56 Starting compiler/backend/arm8
Dec 04 00:21:58 Finished compiler/backend/arm8                                    1s 123MB
Dec 04 00:21:59 Starting compiler/backend/mips
Dec 04 00:22:01 Finished compiler/backend/mips                                    1s 124MB
Dec 04 00:22:02 Starting compiler/backend/riscv
Dec 04 00:22:04 Finished compiler/backend/riscv                                   1s 123MB
Dec 04 18:05:15 Resuming compiler/backend/ag32
Dec 04 18:06:23 Finished compiler/backend/ag32                                 1m06s   3GB
Dec 04 18:06:24 Starting compiler/parsing/proofs
Dec 04 18:06:25 Finished compiler/parsing/proofs                                  0s  61MB
Dec 04 18:06:26 Starting compiler/inference/proofs
Dec 04 18:06:28 Finished compiler/inference/proofs                                0s  85MB
Dec 04 18:06:29 Starting compiler/backend/semantics
Dec 04 18:09:35 Finished compiler/backend/semantics                            3m05s   2GB
Dec 04 18:09:36 Starting compiler/backend/reg_alloc/proofs
Dec 04 18:09:38 Finished compiler/backend/reg_alloc/proofs                        0s  86MB
Dec 04 18:09:39 Starting compiler/backend/proofs
Dec 04 18:10:26 Finished compiler/backend/proofs                                 46s   2GB
Dec 04 18:10:27 Starting compiler/backend/serialiser
Dec 04 18:10:29 Finished compiler/backend/serialiser                              1s 140MB
Dec 04 18:10:30 Starting compiler/encoders/x64/proofs
Dec 04 18:20:38 Finished compiler/encoders/x64/proofs                         10m07s   5GB
Dec 04 18:20:39 Starting compiler/encoders/arm7/proofs
Dec 04 18:33:51 Finished compiler/encoders/arm7/proofs                        13m11s   8GB
Dec 04 18:33:52 Starting compiler/encoders/arm8/proofs
Dec 04 18:40:55 Finished compiler/encoders/arm8/proofs                         7m02s   4GB
Dec 04 18:40:56 Starting compiler/encoders/arm8_asl/proofs
Dec 04 19:30:33 Finished compiler/encoders/arm8_asl/proofs                    49m35s  20GB
Dec 04 19:30:34 Starting compiler/encoders/mips/proofs
Dec 04 19:40:42 Finished compiler/encoders/mips/proofs                        10m07s   3GB
Dec 04 19:40:43 Starting compiler/encoders/riscv/proofs
Dec 04 19:48:51 Finished compiler/encoders/riscv/proofs                        8m07s   4GB
Dec 04 19:48:52 Starting compiler/encoders/ag32/proofs
Dec 04 19:51:44 Finished compiler/encoders/ag32/proofs                         2m51s   2GB
Dec 04 19:51:45 Starting compiler/backend/x64/proofs
Dec 04 19:52:16 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 04 19:52:17 Starting compiler/backend/arm7/proofs
Dec 04 19:52:51 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 04 19:52:52 Starting compiler/backend/arm8/proofs
Dec 04 19:53:25 Finished compiler/backend/arm8/proofs                            31s   2GB
Dec 04 19:53:26 Starting compiler/backend/arm8_asl
Dec 04 19:53:48 Finished compiler/backend/arm8_asl                               21s   2GB
Dec 04 19:53:49 Starting compiler/backend/mips/proofs
Dec 04 19:54:22 Finished compiler/backend/mips/proofs                            31s   2GB
Dec 04 19:54:23 Starting compiler/backend/riscv/proofs
Dec 04 19:54:57 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 04 19:54:58 Starting compiler/backend/ag32/proofs
Dec 04 20:08:35 Finished compiler/backend/ag32/proofs                         13m36s   4GB
Dec 04 20:08:36 Starting compiler/backend/cv_compute
Dec 04 20:09:43 Finished compiler/backend/cv_compute                           1m06s   2GB
Dec 04 20:09:44 Starting cv_translator
Dec 04 20:27:24 Finished cv_translator                                        17m38s   8GB
Dec 04 20:27:25 Starting candle/set-theory
Dec 04 20:28:00 Finished candle/set-theory                                       34s   1GB
Dec 04 20:28:00 Starting candle/syntax-lib
Dec 04 20:28:02 Finished candle/syntax-lib                                        0s  65MB
Dec 04 20:28:03 Starting candle/standard/syntax
Dec 04 20:28:15 Finished candle/standard/syntax                                  11s 758MB
Dec 04 20:28:16 Starting candle/standard/semantics
Dec 04 20:30:17 Finished candle/standard/semantics                             1m59s   2GB
Dec 04 20:30:18 Starting candle/standard/monadic
Dec 04 20:30:19 Finished candle/standard/monadic                                  0s  92MB
Dec 04 20:30:20 Starting candle/standard/ml_kernel
Dec 04 20:32:05 Finished candle/standard/ml_kernel                             1m43s   4GB
Dec 04 20:32:06 Starting candle/overloading/syntax
Dec 04 20:35:16 Finished candle/overloading/syntax                             3m09s   1GB
Dec 04 20:35:17 Starting candle/overloading/semantics
Dec 04 20:46:11 Finished candle/overloading/semantics                         10m53s   3GB
Dec 04 20:46:12 Starting candle/overloading/monadic
Dec 04 20:48:28 Finished candle/overloading/monadic                            2m15s   2GB
Dec 04 20:48:29 Starting candle/overloading/ml_kernel
Dec 04 20:55:40 Finished candle/overloading/ml_kernel                          7m09s   6GB
Dec 04 20:55:41 Starting candle/overloading/ml_checker
Dec 04 20:58:09 Finished candle/overloading/ml_checker                         2m27s   6GB
Dec 04 20:58:10 Starting candle/prover
Dec 04 21:07:50 Finished candle/prover                                         9m38s   5GB
Dec 04 21:07:51 Starting pancake
Dec 04 21:08:13 Finished pancake                                                 21s 835MB
Dec 04 21:08:14 Starting pancake/ffi
Dec 04 21:08:15 Finished pancake/ffi                                              0s  11MB
Dec 04 21:08:15 Starting pancake/semantics
Dec 04 21:10:26 Finished pancake/semantics                                     2m09s   2GB
Dec 04 21:10:27 Starting pancake/parser
Dec 04 21:10:51 Finished pancake/parser                                          22s 469MB
Dec 04 21:10:52 Starting pancake/proofs
Dec 04 21:26:49 Finished pancake/proofs                                       15m56s   7GB
Dec 04 21:26:50 Starting compiler/dafny
Dec 04 21:29:27 Finished compiler/dafny                                        2m36s   8GB
Dec 04 21:29:28 Starting compiler/dafny/translation
Dec 04 21:46:23 Finished compiler/dafny/translation                           16m54s  20GB
Dec 04 21:46:24 Starting compiler/dafny/compilation
Dec 04 21:48:52 Finished compiler/dafny/compilation                            2m27s   8GB
Dec 04 21:48:53 Starting compiler/dafny/semantics
Dec 04 21:49:28 Finished compiler/dafny/semantics                                34s   1GB
Dec 04 21:49:29 Starting characteristic/examples
Dec 04 21:50:56 Finished characteristic/examples                               1m25s   4GB
Dec 04 21:50:56 Starting tutorial/solutions
Dec 04 21:53:20 Finished tutorial/solutions                                    2m22s   3GB
Dec 04 21:53:21 Starting translator/monadic/examples
Dec 04 21:56:16 Finished translator/monadic/examples                           2m54s   4GB
Dec 04 21:56:17 Starting examples
Dec 04 22:02:16 Finished examples                                              5m58s   3GB
Dec 04 22:02:17 Starting examples/compilation/x64
Dec 04 22:09:27 Finished examples/compilation/x64                              7m07s   4GB
Dec 04 22:09:28 Starting examples/compilation/x64/proofs
Dec 04 22:11:49 Finished examples/compilation/x64/proofs                       2m19s   3GB
Dec 04 22:11:50 Starting examples/compilation/ag32
Dec 04 22:13:36 Finished examples/compilation/ag32                             1m45s   3GB
Dec 04 22:13:37 Starting examples/compilation/ag32/proofs
Dec 04 22:14:35 Finished examples/compilation/ag32/proofs                        57s   4GB
Dec 04 22:14:36 Starting examples/compilation/to_word
Dec 04 22:17:52 Finished examples/compilation/to_word                          3m14s   9GB
Dec 04 22:17:52 Starting examples/lpr_checker
Dec 04 22:18:23 Finished examples/lpr_checker                                    29s   1GB
Dec 04 22:18:24 Starting examples/lpr_checker/array
Dec 04 22:44:56 Finished examples/lpr_checker/array                           26m31s  19GB
Dec 04 22:44:57 Starting examples/lpr_checker/array/compilation
Dec 04 22:46:47 Finished examples/lpr_checker/array/compilation                1m49s   7GB
Dec 04 22:46:48 Starting examples/lpr_checker/array/compilation/proofs
Dec 04 22:48:32 Finished examples/lpr_checker/array/compilation/proofs         1m43s   5GB
Dec 04 22:48:33 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 04 22:49:35 Finished examples/lpr_checker/array/compilation/proofsARM8     1m00s   6GB
Dec 04 22:49:36 Starting .
Dec 04 22:49:39 Finished .                                                        2s 284MB
Dec 04 22:49:40 Starting examples/xlrup_checker
Dec 04 22:50:15 Finished examples/xlrup_checker                                  33s   1GB
Dec 04 22:50:16 Starting examples/xlrup_checker/array
Dec 04 23:03:23 Finished examples/xlrup_checker/array                         13m06s  10GB
Dec 04 23:03:24 Starting examples/xlrup_checker/array/compilation
Dec 04 23:04:22 Finished examples/xlrup_checker/array/compilation                57s   4GB
Dec 04 23:04:23 Starting examples/xlrup_checker/array/compilation/proofs
Dec 04 23:05:19 Finished examples/xlrup_checker/array/compilation/proofs         54s   4GB
Dec 04 23:05:20 Starting examples/pseudo_bool
Dec 04 23:06:50 Finished examples/pseudo_bool                                  1m28s   2GB
Dec 04 23:06:51 Starting examples/pseudo_bool/cnf_encoding
Dec 04 23:07:19 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
Dec 04 23:07:20 Starting examples/pseudo_bool/graph_encoding
Dec 04 23:08:04 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 04 23:08:05 Starting examples/pseudo_bool/array
Dec 05 00:16:48 Finished examples/pseudo_bool/array                         1h08m42s  23GB
Dec 05 00:16:49 Starting examples/pseudo_bool/array/compilation
Dec 05 00:25:20 Finished examples/pseudo_bool/array/compilation                8m29s  16GB
Dec 05 00:25:21 Starting examples/pseudo_bool/array/compilation/proofs
Dec 05 00:27:53 Finished examples/pseudo_bool/array/compilation/proofs         2m31s   6GB
Dec 05 00:27:54 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 05 00:29:02 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m07s   6GB
Dec 05 00:29:03 Starting examples/opentheory
Dec 05 00:37:34 Finished examples/opentheory                                   8m30s   6GB
Dec 05 00:37:35 Starting examples/opentheory
Dec 05 00:37:37 Finished examples/opentheory                                      1s 121MB
Dec 05 00:37:38 Starting examples/opentheory/compilation
Dec 05 00:39:01 Finished examples/opentheory/compilation                       1m22s   5GB
Dec 05 00:39:02 Starting examples/opentheory/compilation/proofs
Dec 05 00:39:57 Finished examples/opentheory/compilation/proofs                  53s   4GB
Dec 05 00:39:58 Starting examples/opentheory/compilation/ag32
Dec 05 00:41:23 Finished examples/opentheory/compilation/ag32                  1m24s   6GB
Dec 05 00:41:24 Starting examples/opentheory/compilation/ag32/proofs
Dec 05 00:43:00 Finished examples/opentheory/compilation/ag32/proofs           1m34s   8GB
Dec 05 00:43:01 Starting examples/sat_encodings
Dec 05 00:44:01 Finished examples/sat_encodings                                  59s 796MB
Dec 05 00:44:01 Starting examples/sat_encodings/case_studies
Dec 05 00:45:47 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Dec 05 00:45:48 Starting examples/sat_encodings/translation
Dec 05 00:49:20 Finished examples/sat_encodings/translation                    3m31s   3GB
Dec 05 00:49:21 Starting examples/sat_encodings/translation/compilation
Dec 05 00:51:07 Finished examples/sat_encodings/translation/compilation        1m44s   4GB
Dec 05 00:51:08 Starting examples/deflate
Dec 05 00:51:35 Finished examples/deflate                                        26s 729MB
Dec 05 00:51:36 Starting examples/deflate/translation
Dec 05 00:52:30 Finished examples/deflate/translation                            53s   2GB
Dec 05 00:52:31 Starting examples/deflate/translation/compilation
Dec 05 00:53:21 Finished examples/deflate/translation/compilation                48s   3GB
Dec 05 00:53:22 Starting examples/vipr
Dec 05 00:56:50 Finished examples/vipr                                         3m27s   4GB
Dec 05 00:56:51 Starting examples/vipr/compilation
Dec 05 00:57:45 Finished examples/vipr/compilation                               52s   4GB
Dec 05 00:57:45 Starting translator/okasaki-examples
Dec 05 01:01:46 Finished translator/okasaki-examples                           3m59s   4GB
Dec 05 01:01:46 Starting translator/other-examples
Dec 05 01:04:48 Finished translator/other-examples                             3m01s   2GB
Dec 05 01:04:49 Starting compiler/parsing/tests
Dec 05 01:05:21 Finished compiler/parsing/tests                                  30s   1GB
Dec 05 01:05:22 Starting compiler/inference/tests
Dec 05 01:05:58 Finished compiler/inference/tests                                34s   2GB
Dec 05 01:05:59 Starting compiler/printing/test
Dec 05 01:07:08 Finished compiler/printing/test                                1m08s   3GB
Dec 05 01:07:09 Starting icing/flover
Dec 05 01:41:06 Finished icing/flover                                         33m55s   2GB
Dec 05 01:41:07 Starting icing/
Dec 05 02:08:08 Finished icing/                                               26m59s   4GB
Dec 05 02:08:09 Starting icing/examples
Dec 05 02:09:42 Finished icing/examples                                        1m32s   7GB
Dec 05 02:09:43 Starting compiler/repl
Dec 05 02:17:46 Finished compiler/repl                                         8m01s   7GB
Dec 05 02:17:46 Starting unverified/sexpr-bootstrap/x64/64
Dec 05 02:22:00 Finished unverified/sexpr-bootstrap/x64/64                     4m12s  17GB
Dec 05 02:22:00 Starting unverified/sexpr-bootstrap/x64/32
Dec 05 02:25:15 Finished unverified/sexpr-bootstrap/x64/32                     3m13s  15GB
Dec 05 02:25:16 Starting compiler/benchmarks
Dec 05 02:26:02 Finished compiler/benchmarks                                     44s 712MB
Dec 05 02:26:03 Starting compiler/bootstrap/compilation/x64/64
Dec 05 02:50:15 Finished compiler/bootstrap/compilation/x64/64                24m11s  89GB
Dec 05 02:50:16 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 05 03:50:34 Finished compiler/bootstrap/compilation/x64/64/proofs         24m24s  53GB
Dec 05 03:50:38 Starting compiler/bootstrap/compilation/x64/32
Dec 05 04:15:18 Finished compiler/bootstrap/compilation/x64/32                24m39s  69GB
Dec 05 04:15:19 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 05 04:19:22 Finished compiler/bootstrap/compilation/x64/32/proofs          4m02s  23GB
Dec 05 04:19:23 Starting compiler/bootstrap/compilation/arm8/64
Dec 05 04:54:49 Finished compiler/bootstrap/compilation/arm8/64               35m24s  91GB
Dec 05 04:54:50 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 05 05:00:21 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m29s  30GB
Dec 05 05:00:21 Starting compiler/bootstrap/compilation/ag32/32
Dec 05 05:26:02 Finished compiler/bootstrap/compilation/ag32/32               25m38s  73GB
Dec 05 05:26:03 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 05 05:30:57 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m53s  30GB
Dec 05 05:30:58 SUCCESS