Job 2737

CakeML:7fbd4c8acb17a92a3a51733e327999ba3afb8356
  Finish updates for bool in Loc values [Dec 08 08:27:31]
#1107 (noneq-refs)
Merging into:a85a9b4dbfb3eae33617cfb556784d8c3b179bdb
  Merge pull request #1097 from CakeML/remove-compilationlib [Dec 06 06:47:34]
HOL:629d43fd28ac8162ca9b1e27999602b4b9e452c1
  Holmake now attempts to build bare names which it knows loc'n of [Dec 05 10:16:35]
Machine:lammmington

Dec 08 10:24:30 Claimed job
Dec 08 10:24:33 Reusing HOL
Dec 08 10:24:44 Starting developers
Dec 08 10:24:49 Finished developers                                               3s 201MB
Dec 08 10:24:49 Starting developers/bin
Dec 08 10:24:56 Finished developers/bin                                           5s 746MB
Dec 08 10:24:56 Starting compiler/proofs
Dec 08 12:02:21 Finished compiler/proofs                                    1h37m23s  28GB
Dec 08 12:02:22 Starting compiler/bootstrap/translation
Dec 08 17:50:39 Finished compiler/bootstrap/translation                     5h48m16s  87GB
Dec 08 17:50:40 Starting semantics/ffi
Dec 08 17:50:50 Finished semantics/ffi                                            9s 589MB
Dec 08 17:50:51 Starting semantics
Dec 08 17:50:53 Finished semantics                                                0s  53MB
Dec 08 17:50:54 Starting semantics/proofs
Dec 08 17:51:17 Finished semantics/proofs                                        22s 893MB
Dec 08 17:51:18 Starting semantics/alt_semantics
Dec 08 17:51:39 Finished semantics/alt_semantics                                 19s 884MB
Dec 08 17:51:39 Starting semantics/alt_semantics/proofs
Dec 08 18:01:51 Finished semantics/alt_semantics/proofs                       10m10s   2GB
Dec 08 18:01:52 Starting basis/pure
Dec 08 18:01:53 Finished basis/pure                                               0s  61MB
Dec 08 18:01:54 Starting translator
Dec 08 18:03:27 Finished translator                                            1m31s   4GB
Dec 08 18:03:28 Starting compiler/parsing
Dec 08 18:03:29 Finished compiler/parsing                                         0s  57MB
Dec 08 18:03:30 Starting characteristic
Dec 08 18:03:32 Finished characteristic                                           0s  89MB
Dec 08 18:03:33 Starting translator/monadic
Dec 08 18:03:35 Finished translator/monadic                                       0s  86MB
Dec 08 18:03:35 Starting basis
Dec 08 18:05:54 Finished basis                                                 2m17s   3GB
Dec 08 18:05:55 Starting compiler/inference
Dec 08 18:05:56 Finished compiler/inference                                       0s  85MB
Dec 08 18:05:57 Starting compiler/backend/reg_alloc
Dec 08 18:05:59 Finished compiler/backend/reg_alloc                               0s  53MB
Dec 08 18:06:00 Starting compiler/backend/gc
Dec 08 18:06:02 Finished compiler/backend/gc                                      1s 127MB
Dec 08 18:06:03 Starting compiler/backend
Dec 08 18:06:08 Finished compiler/backend                                         4s 242MB
Dec 08 18:06:09 Starting compiler/encoders/asm
Dec 08 18:06:10 Finished compiler/encoders/asm                                    0s  86MB
Dec 08 18:06:11 Starting compiler/encoders/x64
Dec 08 18:06:13 Finished compiler/encoders/x64                                    0s  92MB
Dec 08 18:06:14 Starting compiler/encoders/arm7
Dec 08 18:06:15 Finished compiler/encoders/arm7                                   0s  85MB
Dec 08 18:06:16 Starting compiler/encoders/arm8
Dec 08 18:06:18 Finished compiler/encoders/arm8                                   0s  86MB
Dec 08 18:06:19 Starting compiler/encoders/arm8_asl
Dec 08 18:07:16 Finished compiler/encoders/arm8_asl                              56s  20GB
Dec 08 18:07:17 Starting compiler/encoders/mips
Dec 08 18:07:18 Finished compiler/encoders/mips                                   0s  88MB
Dec 08 18:07:19 Starting compiler/encoders/riscv
Dec 08 18:07:21 Finished compiler/encoders/riscv                                  0s  87MB
Dec 08 18:07:22 Starting compiler/encoders/ag32
Dec 08 18:07:23 Finished compiler/encoders/ag32                                   0s  85MB
Dec 08 18:07:24 Starting compiler/backend/x64
Dec 08 18:07:26 Finished compiler/backend/x64                                     1s 126MB
Dec 08 18:07:27 Starting compiler/backend/arm7
Dec 08 18:07:29 Finished compiler/backend/arm7                                    1s 126MB
Dec 08 18:07:30 Starting compiler/backend/arm8
Dec 08 18:07:32 Finished compiler/backend/arm8                                    1s 126MB
Dec 08 18:07:33 Starting compiler/backend/mips
Dec 08 18:07:35 Finished compiler/backend/mips                                    1s 126MB
Dec 08 18:07:36 Starting compiler/backend/riscv
Dec 08 18:07:38 Finished compiler/backend/riscv                                   1s 126MB
Dec 08 18:07:39 Starting compiler/backend/ag32
Dec 08 18:08:45 Finished compiler/backend/ag32                                 1m05s   2GB
Dec 08 18:08:46 Starting compiler/parsing/proofs
Dec 08 18:08:47 Finished compiler/parsing/proofs                                  0s  65MB
Dec 08 18:08:48 Starting compiler/inference/proofs
Dec 08 18:08:50 Finished compiler/inference/proofs                                0s  90MB
Dec 08 18:08:51 Starting compiler/backend/semantics
Dec 08 18:11:58 Finished compiler/backend/semantics                            3m05s   3GB
Dec 08 18:11:59 Starting compiler/backend/reg_alloc/proofs
Dec 08 18:12:00 Finished compiler/backend/reg_alloc/proofs                        0s  84MB
Dec 08 18:12:01 Starting compiler/backend/proofs
Dec 08 18:12:49 Finished compiler/backend/proofs                                 46s   2GB
Dec 08 18:12:50 Starting compiler/backend/serialiser
Dec 08 18:12:52 Finished compiler/backend/serialiser                              1s 136MB
Dec 08 18:12:53 Starting compiler/encoders/x64/proofs
Dec 08 18:22:55 Finished compiler/encoders/x64/proofs                         10m01s   4GB
Dec 08 18:22:56 Starting compiler/encoders/arm7/proofs
Dec 08 18:35:53 Finished compiler/encoders/arm7/proofs                        12m56s   6GB
Dec 08 18:35:54 Starting compiler/encoders/arm8/proofs
Dec 08 18:43:08 Finished compiler/encoders/arm8/proofs                         7m13s   4GB
Dec 08 18:43:09 Starting compiler/encoders/arm8_asl/proofs
Dec 08 18:58:33 Finished compiler/encoders/arm8_asl/proofs                    15m22s   3GB
Dec 08 18:58:34 Starting compiler/encoders/mips/proofs
Dec 08 19:08:34 Finished compiler/encoders/mips/proofs                         9m58s   7GB
Dec 08 19:08:35 Starting compiler/encoders/riscv/proofs
Dec 08 19:16:50 Finished compiler/encoders/riscv/proofs                        8m13s   5GB
Dec 08 19:16:51 Starting compiler/encoders/ag32/proofs
Dec 08 19:19:42 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Dec 08 19:19:43 Starting compiler/backend/x64/proofs
Dec 08 19:20:15 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 08 19:20:16 Starting compiler/backend/arm7/proofs
Dec 08 19:20:47 Finished compiler/backend/arm7/proofs                            29s   2GB
Dec 08 19:20:47 Starting compiler/backend/arm8/proofs
Dec 08 19:21:20 Finished compiler/backend/arm8/proofs                            31s   2GB
Dec 08 19:21:20 Starting compiler/backend/arm8_asl
Dec 08 19:21:43 Finished compiler/backend/arm8_asl                               21s   2GB
Dec 08 19:21:44 Starting compiler/backend/mips/proofs
Dec 08 19:22:13 Finished compiler/backend/mips/proofs                            28s   2GB
Dec 08 19:22:14 Starting compiler/backend/riscv/proofs
Dec 08 19:22:46 Finished compiler/backend/riscv/proofs                           30s   2GB
Dec 08 19:22:47 Starting compiler/backend/ag32/proofs
Dec 08 19:36:28 Finished compiler/backend/ag32/proofs                         13m40s   5GB
Dec 08 19:36:29 Starting compiler/backend/cv_compute
Dec 08 19:37:37 Finished compiler/backend/cv_compute                           1m06s   2GB
Dec 08 19:37:37 Starting cv_translator
Dec 08 19:54:58 Finished cv_translator                                        17m19s   7GB
Dec 08 19:54:59 Starting candle/set-theory
Dec 08 19:55:34 Finished candle/set-theory                                       34s   1GB
Dec 08 19:55:35 Starting candle/syntax-lib
Dec 08 19:55:37 Finished candle/syntax-lib                                        0s  59MB
Dec 08 19:55:38 Starting candle/standard/syntax
Dec 08 19:55:51 Finished candle/standard/syntax                                  12s 778MB
Dec 08 19:55:52 Starting candle/standard/semantics
Dec 08 19:57:54 Finished candle/standard/semantics                             2m00s   2GB
Dec 08 19:57:55 Starting candle/standard/monadic
Dec 08 19:57:56 Finished candle/standard/monadic                                  0s  88MB
Dec 08 19:57:57 Starting candle/standard/ml_kernel
Dec 08 19:59:40 Finished candle/standard/ml_kernel                             1m42s   4GB
Dec 08 19:59:41 Starting candle/overloading/syntax
Dec 08 20:02:53 Finished candle/overloading/syntax                             3m10s   2GB
Dec 08 20:02:54 Starting candle/overloading/semantics
Dec 08 20:13:47 Finished candle/overloading/semantics                         10m52s   6GB
Dec 08 20:13:48 Starting candle/overloading/monadic
Dec 08 20:16:07 Finished candle/overloading/monadic                            2m18s   2GB
Dec 08 20:16:08 Starting candle/overloading/ml_kernel
Dec 08 20:23:19 Finished candle/overloading/ml_kernel                          7m10s   5GB
Dec 08 20:23:20 Starting candle/overloading/ml_checker
Dec 08 20:25:54 Finished candle/overloading/ml_checker                         2m33s   6GB
Dec 08 20:25:55 Starting candle/prover
Dec 08 20:35:42 Finished candle/prover                                         9m46s   5GB
Dec 08 20:35:43 Starting pancake
Dec 08 20:36:05 Finished pancake                                                 20s 817MB
Dec 08 20:36:06 Starting pancake/ffi
Dec 08 20:36:07 Finished pancake/ffi                                              0s  11MB
Dec 08 20:36:07 Starting pancake/semantics
Dec 08 20:38:16 Finished pancake/semantics                                     2m08s   2GB
Dec 08 20:38:17 Starting pancake/parser
Dec 08 20:38:42 Finished pancake/parser                                          23s 443MB
Dec 08 20:38:43 Starting pancake/proofs
Dec 08 20:54:57 Finished pancake/proofs                                       16m12s   6GB
Dec 08 20:54:58 Starting compiler/dafny
Dec 08 20:57:44 Finished compiler/dafny                                        2m45s  11GB
Dec 08 20:57:45 Starting compiler/dafny/translation
Dec 08 21:15:14 Finished compiler/dafny/translation                           17m27s  19GB
Dec 08 21:15:15 Starting compiler/dafny/compilation
Dec 08 21:17:46 Finished compiler/dafny/compilation                            2m30s   8GB
Dec 08 21:17:47 Starting compiler/dafny/semantics
Dec 08 21:18:24 Finished compiler/dafny/semantics                                35s   1GB
Dec 08 21:18:25 Starting characteristic/examples
Dec 08 21:19:53 Finished characteristic/examples                               1m27s   4GB
Dec 08 21:19:54 Starting tutorial/solutions
Dec 08 21:22:22 Finished tutorial/solutions                                    2m27s   6GB
Dec 08 21:22:23 Starting translator/monadic/examples
Dec 08 21:25:18 Finished translator/monadic/examples                           2m54s   3GB
Dec 08 21:25:19 Starting examples
Dec 08 21:31:21 Finished examples                                              6m00s   4GB
Dec 08 21:31:21 Starting examples/compilation/x64
Dec 08 21:38:01 Finished examples/compilation/x64                              6m38s   4GB
Dec 08 21:38:02 Starting examples/compilation/x64/proofs
Dec 08 21:40:22 Finished examples/compilation/x64/proofs                       2m18s   3GB
Dec 08 21:40:23 Starting examples/compilation/ag32
Dec 08 21:42:09 Finished examples/compilation/ag32                             1m45s   3GB
Dec 08 21:42:10 Starting examples/compilation/ag32/proofs
Dec 08 21:43:08 Finished examples/compilation/ag32/proofs                        57s   4GB
Dec 08 21:43:09 Starting examples/lpr_checker
Dec 08 21:43:39 Finished examples/lpr_checker                                    28s   1GB
Dec 08 21:43:40 Starting examples/lpr_checker/array
Dec 08 22:10:21 Finished examples/lpr_checker/array                           26m40s  25GB
Dec 08 22:10:22 Starting examples/lpr_checker/array/compilation
Dec 08 22:12:10 Finished examples/lpr_checker/array/compilation                1m47s   7GB
Dec 08 22:12:11 Starting examples/lpr_checker/array/compilation/proofs
Dec 08 22:13:18 Finished examples/lpr_checker/array/compilation/proofs         1m05s   6GB
Dec 08 22:13:19 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 08 22:14:23 Finished examples/lpr_checker/array/compilation/proofsARM8     1m02s   6GB
Dec 08 22:14:24 Starting .
Dec 08 22:14:27 Finished .                                                        2s 284MB
Dec 08 22:14:28 Starting examples/xlrup_checker
Dec 08 22:15:03 Finished examples/xlrup_checker                                  33s   1GB
Dec 08 22:15:03 Starting examples/xlrup_checker/array
Dec 08 22:28:25 Finished examples/xlrup_checker/array                         13m20s  10GB
Dec 08 22:28:25 Starting examples/xlrup_checker/array/compilation
Dec 08 22:29:23 Finished examples/xlrup_checker/array/compilation                56s   4GB
Dec 08 22:29:24 Starting examples/xlrup_checker/array/compilation/proofs
Dec 08 22:30:21 Finished examples/xlrup_checker/array/compilation/proofs         55s   4GB
Dec 08 22:30:21 Starting examples/pseudo_bool
Dec 08 22:31:52 Finished examples/pseudo_bool                                  1m29s   2GB
Dec 08 22:31:53 Starting examples/pseudo_bool/cnf_encoding
Dec 08 22:32:23 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Dec 08 22:32:24 Starting examples/pseudo_bool/graph_encoding
Dec 08 22:33:09 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 08 22:33:09 Starting examples/pseudo_bool/array
Dec 08 23:42:35 Finished examples/pseudo_bool/array                         1h09m23s  47GB
Dec 08 23:42:36 Starting examples/pseudo_bool/array/compilation
Dec 08 23:51:13 Finished examples/pseudo_bool/array/compilation                8m36s  16GB
Dec 08 23:51:14 Starting examples/pseudo_bool/array/compilation/proofs
Dec 08 23:53:48 Finished examples/pseudo_bool/array/compilation/proofs         2m33s   6GB
Dec 08 23:53:49 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 08 23:54:58 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m07s   6GB
Dec 08 23:54:59 Starting examples/opentheory
Dec 09 00:03:25 Finished examples/opentheory                                   8m25s   5GB
Dec 09 00:03:26 Starting examples/opentheory
Dec 09 00:03:28 Finished examples/opentheory                                      1s 121MB
Dec 09 00:03:29 Starting examples/opentheory/compilation
Dec 09 00:04:54 Finished examples/opentheory/compilation                       1m24s   5GB
Dec 09 00:04:55 Starting examples/opentheory/compilation/proofs
Dec 09 00:05:55 Finished examples/opentheory/compilation/proofs                  59s   4GB
Dec 09 00:05:56 Starting examples/opentheory/compilation/ag32
Dec 09 00:07:26 Finished examples/opentheory/compilation/ag32                  1m29s   6GB
Dec 09 00:07:27 Starting examples/opentheory/compilation/ag32/proofs
Dec 09 00:09:02 Finished examples/opentheory/compilation/ag32/proofs           1m34s   7GB
Dec 09 00:09:03 Starting examples/sat_encodings
Dec 09 00:10:02 Finished examples/sat_encodings                                  58s 761MB
Dec 09 00:10:03 Starting examples/sat_encodings/case_studies
Dec 09 00:11:49 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Dec 09 00:11:49 Starting examples/sat_encodings/translation
Dec 09 00:15:21 Finished examples/sat_encodings/translation                    3m30s   3GB
Dec 09 00:15:22 Starting examples/sat_encodings/translation/compilation
Dec 09 00:17:08 Finished examples/sat_encodings/translation/compilation        1m44s   4GB
Dec 09 00:17:09 Starting examples/deflate
Dec 09 00:17:36 Finished examples/deflate                                        26s 726MB
Dec 09 00:17:37 Starting examples/deflate/translation
Dec 09 00:18:31 Finished examples/deflate/translation                            53s   2GB
Dec 09 00:18:32 Starting examples/deflate/translation/compilation
Dec 09 00:19:19 Finished examples/deflate/translation/compilation                46s   3GB
Dec 09 00:19:20 Starting examples/vipr
Dec 09 00:22:57 Finished examples/vipr                                         3m36s   9GB
Dec 09 00:22:58 Starting examples/vipr/compilation
Dec 09 00:23:52 Finished examples/vipr/compilation                               52s   4GB
Dec 09 00:23:53 Starting translator/okasaki-examples
Dec 09 00:27:54 Finished translator/okasaki-examples                           4m00s   3GB
Dec 09 00:27:55 Starting translator/other-examples
Dec 09 00:28:47 Finished translator/other-examples                               51s   3GB
Dec 09 00:28:48 Starting compiler/parsing/tests
Dec 09 00:29:20 Finished compiler/parsing/tests                                  30s   1GB
Dec 09 00:29:20 Starting compiler/inference/tests
Dec 09 00:29:54 Finished compiler/inference/tests                                32s   2GB
Dec 09 00:29:55 Starting compiler/printing/test
Dec 09 00:31:07 Finished compiler/printing/test                                1m11s   5GB
Dec 09 00:31:08 Starting icing/flover
Dec 09 01:05:20 Finished icing/flover                                         34m10s   1GB
Dec 09 01:05:21 Starting icing/
Dec 09 01:32:31 Finished icing/                                               27m09s   4GB
Dec 09 01:32:32 Starting icing/examples
Dec 09 01:34:04 Finished icing/examples                                        1m31s   7GB
Dec 09 01:34:05 Starting compiler/repl
Dec 09 01:42:04 Finished compiler/repl                                         7m58s   7GB
Dec 09 01:42:05 Starting unverified/sexpr-bootstrap/x64/64
Dec 09 01:45:58 Finished unverified/sexpr-bootstrap/x64/64                     3m52s  16GB
Dec 09 01:45:59 Starting unverified/sexpr-bootstrap/x64/32
Dec 09 01:49:26 Finished unverified/sexpr-bootstrap/x64/32                     3m26s  14GB
Dec 09 01:49:27 Starting compiler/benchmarks
Dec 09 01:50:13 Finished compiler/benchmarks                                     44s 711MB
Dec 09 01:50:14 Starting compiler/bootstrap/compilation/x64/64
Dec 09 02:15:54 Finished compiler/bootstrap/compilation/x64/64                25m39s  86GB
Dec 09 02:15:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 09 02:39:50 Finished compiler/bootstrap/compilation/x64/64/proofs         23m53s  51GB
Dec 09 02:39:51 Starting compiler/bootstrap/compilation/x64/32
Dec 09 03:04:41 Finished compiler/bootstrap/compilation/x64/32                24m49s  69GB
Dec 09 03:04:42 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 09 03:09:17 Finished compiler/bootstrap/compilation/x64/32/proofs          4m34s  25GB
Dec 09 03:09:18 Starting compiler/bootstrap/compilation/arm8/64
Dec 09 03:44:40 Finished compiler/bootstrap/compilation/arm8/64               35m20s  84GB
Dec 09 03:44:41 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 09 03:50:08 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m25s  29GB
Dec 09 03:50:09 Starting compiler/bootstrap/compilation/ag32/32
Dec 09 04:15:27 Finished compiler/bootstrap/compilation/ag32/32               25m17s  74GB
Dec 09 04:15:28 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 09 04:19:51 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m21s  29GB
Dec 09 04:19:52 SUCCESS