Job 2734

CakeML:37172918cd92dcc0527f90354288a2ebbf6f5406
  Merge branch 'master' into cost [Dec 06 10:06:30]
#1092 (cost)
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:pavlova

Dec 06 21:19:58 Claimed job
Dec 06 21:20:06 Building HOL
Dec 06 21:31:01 Starting developers
Dec 06 21:31:05 Finished developers                                               2s 118MB
Dec 06 21:31:06 Starting developers/bin
Dec 06 21:31:13 Finished developers/bin                                           5s 745MB
Dec 06 21:31:13 Starting compiler/proofs
Dec 06 23:12:19 Finished compiler/proofs                                    1h41m04s  31GB
Dec 06 23:12:20 Starting compiler/bootstrap/translation
Dec 07 05:04:27 Finished compiler/bootstrap/translation                     5h52m06s  95GB
Dec 07 05:04:28 Starting semantics/ffi
Dec 07 05:04:38 Finished semantics/ffi                                            9s 611MB
Dec 07 05:04:39 Starting semantics
Dec 07 05:04:40 Finished semantics                                                0s  53MB
Dec 07 05:04:41 Starting semantics/proofs
Dec 07 05:05:04 Finished semantics/proofs                                        22s 881MB
Dec 07 05:05:05 Starting semantics/alt_semantics
Dec 07 05:05:26 Finished semantics/alt_semantics                                 20s 904MB
Dec 07 05:05:27 Starting semantics/alt_semantics/proofs
Dec 07 05:15:45 Finished semantics/alt_semantics/proofs                       10m16s   2GB
Dec 07 05:15:46 Starting basis/pure
Dec 07 05:15:47 Finished basis/pure                                               0s  59MB
Dec 07 05:15:48 Starting translator
Dec 07 05:17:22 Finished translator                                            1m33s   3GB
Dec 07 05:17:23 Starting compiler/parsing
Dec 07 05:17:25 Finished compiler/parsing                                         0s  57MB
Dec 07 05:17:26 Starting characteristic
Dec 07 05:17:27 Finished characteristic                                           0s  84MB
Dec 07 05:17:28 Starting translator/monadic
Dec 07 05:17:30 Finished translator/monadic                                       0s  89MB
Dec 07 05:17:31 Starting basis
Dec 07 05:19:52 Finished basis                                                 2m19s   3GB
Dec 07 05:19:52 Starting compiler/inference
Dec 07 05:19:54 Finished compiler/inference                                       0s  85MB
Dec 07 05:19:55 Starting compiler/backend/reg_alloc
Dec 07 05:19:56 Finished compiler/backend/reg_alloc                               0s  53MB
Dec 07 05:19:57 Starting compiler/backend/gc
Dec 07 05:19:59 Finished compiler/backend/gc                                      1s 123MB
Dec 07 05:20:00 Starting compiler/backend
Dec 07 05:20:05 Finished compiler/backend                                         4s 270MB
Dec 07 05:20:06 Starting compiler/encoders/asm
Dec 07 05:20:08 Finished compiler/encoders/asm                                    0s  82MB
Dec 07 05:20:09 Starting compiler/encoders/x64
Dec 07 05:20:11 Finished compiler/encoders/x64                                    0s  91MB
Dec 07 05:20:11 Starting compiler/encoders/arm7
Dec 07 05:20:13 Finished compiler/encoders/arm7                                   0s  86MB
Dec 07 05:20:14 Starting compiler/encoders/arm8
Dec 07 05:20:16 Finished compiler/encoders/arm8                                   0s  84MB
Dec 07 05:20:17 Starting compiler/encoders/arm8_asl
Dec 07 07:18:29 Finished compiler/encoders/arm8_asl                         1h58m10s  28GB
Dec 07 07:18:29 Starting compiler/encoders/mips
Dec 07 07:18:31 Finished compiler/encoders/mips                                   0s  86MB
Dec 07 07:18:32 Starting compiler/encoders/riscv
Dec 07 07:18:34 Finished compiler/encoders/riscv                                  0s  83MB
Dec 07 07:18:35 Starting compiler/encoders/ag32
Dec 07 07:18:36 Finished compiler/encoders/ag32                                   0s  88MB
Dec 07 07:18:37 Starting compiler/backend/x64
Dec 07 07:18:39 Finished compiler/backend/x64                                     1s 123MB
Dec 07 07:18:40 Starting compiler/backend/arm7
Dec 07 07:18:42 Finished compiler/backend/arm7                                    1s 123MB
Dec 07 07:18:43 Starting compiler/backend/arm8
Dec 07 07:18:45 Finished compiler/backend/arm8                                    1s 123MB
Dec 07 07:18:46 Starting compiler/backend/mips
Dec 07 07:18:48 Finished compiler/backend/mips                                    1s 123MB
Dec 07 07:18:49 Starting compiler/backend/riscv
Dec 07 07:18:51 Finished compiler/backend/riscv                                   1s 123MB
Dec 07 07:18:52 Starting compiler/backend/ag32
Dec 07 07:19:58 Finished compiler/backend/ag32                                 1m04s   2GB
Dec 07 07:19:59 Starting compiler/parsing/proofs
Dec 07 07:20:00 Finished compiler/parsing/proofs                                  0s  64MB
Dec 07 07:20:01 Starting compiler/inference/proofs
Dec 07 07:20:03 Finished compiler/inference/proofs                                0s  86MB
Dec 07 07:20:04 Starting compiler/backend/semantics
Dec 07 07:23:11 Finished compiler/backend/semantics                            3m06s   2GB
Dec 07 07:23:12 Starting compiler/backend/reg_alloc/proofs
Dec 07 07:23:14 Finished compiler/backend/reg_alloc/proofs                        0s  85MB
Dec 07 07:23:14 Starting compiler/backend/proofs
Dec 07 07:24:04 Finished compiler/backend/proofs                                 48s   4GB
Dec 07 07:24:05 Starting compiler/backend/serialiser
Dec 07 07:24:07 Finished compiler/backend/serialiser                              1s 139MB
Dec 07 07:24:08 Starting compiler/encoders/x64/proofs
Dec 07 07:34:21 Finished compiler/encoders/x64/proofs                         10m11s   5GB
Dec 07 07:34:22 Starting compiler/encoders/arm7/proofs
Dec 07 07:47:43 Finished compiler/encoders/arm7/proofs                        13m20s  11GB
Dec 07 07:47:44 Starting compiler/encoders/arm8/proofs
Dec 07 07:54:54 Finished compiler/encoders/arm8/proofs                         7m08s   4GB
Dec 07 07:54:55 Starting compiler/encoders/arm8_asl/proofs
Dec 07 08:43:52 Finished compiler/encoders/arm8_asl/proofs                    48m56s  20GB
Dec 07 08:43:53 Starting compiler/encoders/mips/proofs
Dec 07 08:53:56 Finished compiler/encoders/mips/proofs                        10m01s   4GB
Dec 07 08:53:57 Starting compiler/encoders/riscv/proofs
Dec 07 09:02:22 Finished compiler/encoders/riscv/proofs                        8m24s   3GB
Dec 07 09:02:23 Starting compiler/encoders/ag32/proofs
Dec 07 09:05:16 Finished compiler/encoders/ag32/proofs                         2m51s   2GB
Dec 07 09:05:17 Starting compiler/backend/x64/proofs
Dec 07 09:05:48 Finished compiler/backend/x64/proofs                             29s   2GB
Dec 07 09:05:49 Starting compiler/backend/arm7/proofs
Dec 07 09:06:23 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 07 09:06:24 Starting compiler/backend/arm8/proofs
Dec 07 09:06:54 Finished compiler/backend/arm8/proofs                            28s   2GB
Dec 07 09:06:55 Starting compiler/backend/arm8_asl
Dec 07 09:07:16 Finished compiler/backend/arm8_asl                               20s   2GB
Dec 07 09:07:17 Starting compiler/backend/mips/proofs
Dec 07 09:07:48 Finished compiler/backend/mips/proofs                            30s   2GB
Dec 07 09:07:49 Starting compiler/backend/riscv/proofs
Dec 07 09:08:21 Finished compiler/backend/riscv/proofs                           30s   2GB
Dec 07 09:08:22 Starting compiler/backend/ag32/proofs
Dec 07 09:21:50 Finished compiler/backend/ag32/proofs                         13m26s   5GB
Dec 07 09:21:50 Starting compiler/backend/cv_compute
Dec 07 09:22:58 Finished compiler/backend/cv_compute                           1m06s   2GB
Dec 07 09:22:59 Starting cv_translator
Dec 07 09:40:25 Finished cv_translator                                        17m24s   8GB
Dec 07 09:40:26 Starting candle/set-theory
Dec 07 09:41:01 Finished candle/set-theory                                       33s   1GB
Dec 07 09:41:01 Starting candle/syntax-lib
Dec 07 09:41:03 Finished candle/syntax-lib                                        0s  59MB
Dec 07 09:41:04 Starting candle/standard/syntax
Dec 07 09:41:17 Finished candle/standard/syntax                                  12s 773MB
Dec 07 09:41:18 Starting candle/standard/semantics
Dec 07 09:43:18 Finished candle/standard/semantics                             1m58s   2GB
Dec 07 09:43:19 Starting candle/standard/monadic
Dec 07 09:43:20 Finished candle/standard/monadic                                  0s  92MB
Dec 07 09:43:21 Starting candle/standard/ml_kernel
Dec 07 09:45:06 Finished candle/standard/ml_kernel                             1m44s   4GB
Dec 07 09:45:07 Starting candle/overloading/syntax
Dec 07 09:48:17 Finished candle/overloading/syntax                             3m09s   2GB
Dec 07 09:48:18 Starting candle/overloading/semantics
Dec 07 09:59:10 Finished candle/overloading/semantics                         10m50s   5GB
Dec 07 09:59:11 Starting candle/overloading/monadic
Dec 07 10:01:28 Finished candle/overloading/monadic                            2m16s   2GB
Dec 07 10:01:29 Starting candle/overloading/ml_kernel
Dec 07 10:08:36 Finished candle/overloading/ml_kernel                          7m06s   5GB
Dec 07 10:08:37 Starting candle/overloading/ml_checker
Dec 07 10:11:08 Finished candle/overloading/ml_checker                         2m29s   6GB
Dec 07 10:11:09 Starting candle/prover
Dec 07 10:20:44 Finished candle/prover                                         9m34s   5GB
Dec 07 10:20:45 Starting pancake
Dec 07 10:21:07 Finished pancake                                                 20s 824MB
Dec 07 10:21:08 Starting pancake/ffi
Dec 07 10:21:09 Finished pancake/ffi                                              0s  11MB
Dec 07 10:21:09 Starting pancake/semantics
Dec 07 10:23:18 Finished pancake/semantics                                     2m07s   2GB
Dec 07 10:23:19 Starting pancake/parser
Dec 07 10:23:43 Finished pancake/parser                                          23s 411MB
Dec 07 10:23:44 Starting pancake/proofs
Dec 07 10:39:37 Finished pancake/proofs                                       15m51s   7GB
Dec 07 10:39:38 Starting compiler/dafny
Dec 07 10:42:13 Finished compiler/dafny                                        2m34s  10GB
Dec 07 10:42:14 Starting compiler/dafny/translation
Dec 07 10:59:11 Finished compiler/dafny/translation                           16m56s  16GB
Dec 07 10:59:12 Starting compiler/dafny/compilation
Dec 07 11:01:49 Finished compiler/dafny/compilation                            2m35s  10GB
Dec 07 11:01:50 Starting compiler/dafny/semantics
Dec 07 11:02:25 Finished compiler/dafny/semantics                                34s   1GB
Dec 07 11:02:26 Starting characteristic/examples
Dec 07 11:03:51 Finished characteristic/examples                               1m23s   4GB
Dec 07 11:03:52 Starting tutorial/solutions
Dec 07 11:06:14 Finished tutorial/solutions                                    2m21s   3GB
Dec 07 11:06:15 Starting translator/monadic/examples
Dec 07 11:09:05 Finished translator/monadic/examples                           2m49s   4GB
Dec 07 11:09:06 Starting examples
Dec 07 11:15:07 Finished examples                                              5m59s   4GB
Dec 07 11:15:08 Starting examples/compilation/x64
Dec 07 11:21:46 Finished examples/compilation/x64                              6m37s   4GB
Dec 07 11:21:47 Starting examples/compilation/x64/proofs
Dec 07 11:24:05 Finished examples/compilation/x64/proofs                       2m17s   3GB
Dec 07 11:24:06 Starting examples/compilation/ag32
Dec 07 11:25:51 Finished examples/compilation/ag32                             1m43s   3GB
Dec 07 11:25:52 Starting examples/compilation/ag32/proofs
Dec 07 11:26:47 Finished examples/compilation/ag32/proofs                        54s   4GB
Dec 07 11:26:48 Starting examples/lpr_checker
Dec 07 11:27:18 Finished examples/lpr_checker                                    28s   1GB
Dec 07 11:27:19 Starting examples/lpr_checker/array
Dec 07 11:54:16 Finished examples/lpr_checker/array                           26m56s  30GB
Dec 07 11:54:17 Starting examples/lpr_checker/array/compilation
Dec 07 11:56:02 Finished examples/lpr_checker/array/compilation                1m43s   7GB
Dec 07 11:56:03 Starting examples/lpr_checker/array/compilation/proofs
Dec 07 11:57:14 Finished examples/lpr_checker/array/compilation/proofs         1m10s   6GB
Dec 07 11:57:15 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 07 11:58:20 Finished examples/lpr_checker/array/compilation/proofsARM8     1m03s   6GB
Dec 07 11:58:21 Starting .
Dec 07 11:58:25 Finished .                                                        2s 284MB
Dec 07 11:58:25 Starting examples/xlrup_checker
Dec 07 11:59:00 Finished examples/xlrup_checker                                  33s   1GB
Dec 07 11:59:00 Starting examples/xlrup_checker/array
Dec 07 12:11:59 Finished examples/xlrup_checker/array                         12m57s   8GB
Dec 07 12:12:00 Starting examples/xlrup_checker/array/compilation
Dec 07 12:12:59 Finished examples/xlrup_checker/array/compilation                57s   4GB
Dec 07 12:13:00 Starting examples/xlrup_checker/array/compilation/proofs
Dec 07 12:13:56 Finished examples/xlrup_checker/array/compilation/proofs         55s   4GB
Dec 07 12:13:56 Starting examples/pseudo_bool
Dec 07 12:15:25 Finished examples/pseudo_bool                                  1m27s   2GB
Dec 07 12:15:26 Starting examples/pseudo_bool/cnf_encoding
Dec 07 12:15:56 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Dec 07 12:15:57 Starting examples/pseudo_bool/graph_encoding
Dec 07 12:16:41 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 07 12:16:42 Starting examples/pseudo_bool/array
Dec 07 13:24:52 Finished examples/pseudo_bool/array                         1h08m09s  26GB
Dec 07 13:24:53 Starting examples/pseudo_bool/array/compilation
Dec 07 13:33:27 Finished examples/pseudo_bool/array/compilation                8m32s  16GB
Dec 07 13:33:28 Starting examples/pseudo_bool/array/compilation/proofs
Dec 07 13:35:56 Finished examples/pseudo_bool/array/compilation/proofs         2m27s   6GB
Dec 07 13:35:57 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 07 13:37:08 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m09s   6GB
Dec 07 13:37:09 Starting examples/opentheory
Dec 07 13:45:45 Finished examples/opentheory                                   8m35s   6GB
Dec 07 13:45:46 Starting examples/opentheory
Dec 07 13:45:48 Finished examples/opentheory                                      1s 124MB
Dec 07 13:45:49 Starting examples/opentheory/compilation
Dec 07 13:47:09 Finished examples/opentheory/compilation                       1m19s   5GB
Dec 07 13:47:10 Starting examples/opentheory/compilation/proofs
Dec 07 13:48:11 Finished examples/opentheory/compilation/proofs                  59s   4GB
Dec 07 13:48:12 Starting examples/opentheory/compilation/ag32
Dec 07 13:49:37 Finished examples/opentheory/compilation/ag32                  1m24s   6GB
Dec 07 13:49:38 Starting examples/opentheory/compilation/ag32/proofs
Dec 07 13:51:14 Finished examples/opentheory/compilation/ag32/proofs           1m34s   8GB
Dec 07 13:51:15 Starting examples/sat_encodings
Dec 07 13:52:15 Finished examples/sat_encodings                                  58s 931MB
Dec 07 13:52:15 Starting examples/sat_encodings/case_studies
Dec 07 13:54:02 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Dec 07 13:54:03 Starting examples/sat_encodings/translation
Dec 07 13:57:35 Finished examples/sat_encodings/translation                    3m31s   3GB
Dec 07 13:57:36 Starting examples/sat_encodings/translation/compilation
Dec 07 13:59:20 Finished examples/sat_encodings/translation/compilation        1m43s   4GB
Dec 07 13:59:21 Starting examples/deflate
Dec 07 13:59:49 Finished examples/deflate                                        26s 681MB
Dec 07 13:59:50 Starting examples/deflate/translation
Dec 07 14:00:45 Finished examples/deflate/translation                            53s   2GB
Dec 07 14:00:45 Starting examples/deflate/translation/compilation
Dec 07 14:01:34 Finished examples/deflate/translation/compilation                48s   3GB
Dec 07 14:01:35 Starting examples/vipr
Dec 07 14:05:10 Finished examples/vipr                                         3m33s   7GB
Dec 07 14:05:11 Starting examples/vipr/compilation
Dec 07 14:06:05 Finished examples/vipr/compilation                               52s   4GB
Dec 07 14:06:06 Starting translator/okasaki-examples
Dec 07 14:10:06 Finished translator/okasaki-examples                           3m59s   3GB
Dec 07 14:10:07 Starting translator/other-examples
Dec 07 14:13:13 Finished translator/other-examples                             3m05s   2GB
Dec 07 14:13:14 Starting compiler/parsing/tests
Dec 07 14:13:46 Finished compiler/parsing/tests                                  30s   1GB
Dec 07 14:13:46 Starting compiler/inference/tests
Dec 07 14:14:21 Finished compiler/inference/tests                                33s   2GB
Dec 07 14:14:21 Starting compiler/printing/test
Dec 07 14:15:34 Finished compiler/printing/test                                1m11s   5GB
Dec 07 14:15:35 Starting icing/flover
Dec 07 14:49:47 Finished icing/flover                                         34m11s   2GB
Dec 07 14:49:48 Starting icing/
Dec 07 15:16:41 Finished icing/                                               26m51s   4GB
Dec 07 15:16:42 Starting icing/examples
Dec 07 15:18:06 Finished icing/examples                                        1m22s   4GB
Dec 07 15:18:06 Starting compiler/repl
Dec 07 15:25:59 Finished compiler/repl                                         7m51s   7GB
Dec 07 15:26:00 Starting unverified/sexpr-bootstrap/x64/64
Dec 07 15:29:58 Finished unverified/sexpr-bootstrap/x64/64                     3m57s  17GB
Dec 07 15:29:59 Starting unverified/sexpr-bootstrap/x64/32
Dec 07 15:33:11 Finished unverified/sexpr-bootstrap/x64/32                     3m10s  13GB
Dec 07 15:33:11 Starting compiler/benchmarks
Dec 07 15:33:57 Finished compiler/benchmarks                                     44s 711MB
Dec 07 15:33:58 Starting compiler/bootstrap/compilation/x64/64
Dec 07 15:59:05 Finished compiler/bootstrap/compilation/x64/64                25m05s  84GB
Dec 07 15:59:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 07 16:22:46 Finished compiler/bootstrap/compilation/x64/64/proofs         23m39s  45GB
Dec 07 16:22:47 Starting compiler/bootstrap/compilation/x64/32
Dec 07 16:48:09 Finished compiler/bootstrap/compilation/x64/32                25m20s  69GB
Dec 07 16:48:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 07 16:53:00 Finished compiler/bootstrap/compilation/x64/32/proofs          4m49s  23GB
Dec 07 16:53:01 Starting compiler/bootstrap/compilation/arm8/64
Dec 07 17:29:44 Finished compiler/bootstrap/compilation/arm8/64               36m41s 101GB
Dec 07 17:29:45 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 07 17:34:49 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m04s  30GB
Dec 07 17:34:50 Starting compiler/bootstrap/compilation/ag32/32
Dec 07 17:59:52 Finished compiler/bootstrap/compilation/ag32/32               25m00s  72GB
Dec 07 17:59:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 07 18:04:55 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m01s  32GB
Dec 07 18:04:56 SUCCESS