Job 2788

CakeML:23b6b4fb41647bd1ca83a6007ccd0bd34ab82c40
  update README [Mar 18 17:27:19]
#1145 (update_README)
Merging into:e9cafe6795f84d7458975af3f196d67c126c9763
  Merge pull request #1144 from CakeML/issue792 [Mar 22 15:48:00]
HOL:08895ade4fd70a2b712966aafe4147ee043a8100
  Move some theorems to posetScript [Mar 20 23:38:07]
Machine:lammmington

Mar 24 08:13:42 Claimed job
Mar 24 08:13:49 Building HOL
Mar 24 08:24:45 Starting developers
Mar 24 08:24:49 Finished developers                                               3s 197MB
Mar 24 08:24:50 Starting developers/bin
Mar 24 08:24:55 Finished developers/bin                                           4s 746MB
Mar 24 08:24:56 Starting misc
Mar 24 08:25:54 Finished misc                                                    57s   2GB
Mar 24 08:25:55 Starting compiler/proofs
Mar 24 10:07:29 Finished compiler/proofs                                    1h41m31s  38GB
Mar 24 10:07:30 Starting compiler/bootstrap/translation
Mar 24 15:55:13 Finished compiler/bootstrap/translation                     5h47m41s  67GB
Mar 24 15:55:14 Starting semantics/ffi
Mar 24 15:55:24 Finished semantics/ffi                                            8s 588MB
Mar 24 15:55:25 Starting semantics
Mar 24 15:55:26 Finished semantics                                                0s  56MB
Mar 24 15:55:27 Starting semantics/proofs
Mar 24 15:55:49 Finished semantics/proofs                                        21s 853MB
Mar 24 15:55:50 Starting semantics/alt_semantics
Mar 24 15:56:11 Finished semantics/alt_semantics                                 19s 893MB
Mar 24 15:56:12 Starting semantics/alt_semantics/proofs
Mar 24 16:06:26 Finished semantics/alt_semantics/proofs                       10m13s   2GB
Mar 24 16:06:27 Starting basis/pure
Mar 24 16:06:28 Finished basis/pure                                               0s  92MB
Mar 24 16:06:29 Starting translator
Mar 24 16:08:05 Finished translator                                            1m34s   3GB
Mar 24 16:08:06 Starting compiler/parsing
Mar 24 16:08:07 Finished compiler/parsing                                         0s  58MB
Mar 24 16:08:08 Starting characteristic
Mar 24 16:08:10 Finished characteristic                                           1s 119MB
Mar 24 16:08:11 Starting translator/monadic
Mar 24 16:08:13 Finished translator/monadic                                       1s 123MB
Mar 24 16:08:14 Starting translator/monadic/monad_base
Mar 24 16:08:16 Finished translator/monadic/monad_base                            0s  55MB
Mar 24 16:08:17 Starting basis
Mar 24 16:10:35 Finished basis                                                 2m17s   3GB
Mar 24 16:10:36 Starting compiler
Mar 24 16:10:39 Finished compiler                                                 1s 219MB
Mar 24 16:10:40 Starting compiler/inference
Mar 24 16:10:42 Finished compiler/inference                                       1s 119MB
Mar 24 16:10:43 Starting compiler/backend/reg_alloc
Mar 24 16:10:44 Finished compiler/backend/reg_alloc                               0s  57MB
Mar 24 16:10:45 Starting compiler/backend/gc
Mar 24 16:10:47 Finished compiler/backend/gc                                      1s 143MB
Mar 24 16:10:48 Starting compiler/backend
Mar 24 16:10:53 Finished compiler/backend                                         4s 251MB
Mar 24 16:10:54 Starting compiler/encoders/asm
Mar 24 16:10:56 Finished compiler/encoders/asm                                    0s  84MB
Mar 24 16:10:57 Starting compiler/encoders/x64
Mar 24 16:10:59 Finished compiler/encoders/x64                                    0s  89MB
Mar 24 16:11:00 Starting compiler/encoders/arm7
Mar 24 16:11:01 Finished compiler/encoders/arm7                                   0s  93MB
Mar 24 16:11:02 Starting compiler/encoders/arm8
Mar 24 16:11:04 Finished compiler/encoders/arm8                                   0s  92MB
Mar 24 16:11:05 Starting compiler/encoders/arm8_asl
Mar 24 18:12:34 Finished compiler/encoders/arm8_asl                         2h01m27s  40GB
Mar 24 18:12:35 Starting compiler/encoders/mips
Mar 24 18:12:37 Finished compiler/encoders/mips                                   0s  89MB
Mar 24 18:12:38 Starting compiler/encoders/riscv
Mar 24 18:12:39 Finished compiler/encoders/riscv                                  0s  86MB
Mar 24 18:12:40 Starting compiler/encoders/ag32
Mar 24 18:12:42 Finished compiler/encoders/ag32                                   0s  90MB
Mar 24 18:12:43 Starting compiler/encoders/tests
Mar 24 18:12:45 Finished compiler/encoders/tests                                  1s 112MB
Mar 24 18:12:46 Starting compiler/encoders/monadic_enc
Mar 24 18:12:48 Finished compiler/encoders/monadic_enc                            1s 135MB
Mar 24 18:12:49 Starting compiler/backend/x64
Mar 24 18:12:51 Finished compiler/backend/x64                                     1s 140MB
Mar 24 18:12:52 Starting compiler/backend/arm7
Mar 24 18:12:54 Finished compiler/backend/arm7                                    1s 143MB
Mar 24 18:12:55 Starting compiler/backend/arm8
Mar 24 18:12:57 Finished compiler/backend/arm8                                    1s 143MB
Mar 24 18:12:58 Starting compiler/backend/mips
Mar 24 18:13:00 Finished compiler/backend/mips                                    1s 143MB
Mar 24 18:13:01 Starting compiler/backend/riscv
Mar 24 18:13:03 Finished compiler/backend/riscv                                   1s 140MB
Mar 24 18:13:04 Starting compiler/backend/ag32
Mar 24 18:14:10 Finished compiler/backend/ag32                                 1m05s   3GB
Mar 24 18:14:11 Starting compiler/backend/pattern_matching
Mar 24 18:14:13 Finished compiler/backend/pattern_matching                        0s  52MB
Mar 24 18:14:14 Starting compiler/parsing/ocaml
Mar 24 18:15:56 Finished compiler/parsing/ocaml                                1m41s   1GB
Mar 24 18:15:57 Starting compiler/printing
Mar 24 18:15:59 Finished compiler/printing                                        1s 112MB
Mar 24 18:16:00 Starting compiler/parsing/proofs
Mar 24 18:16:01 Finished compiler/parsing/proofs                                  0s  64MB
Mar 24 18:16:02 Starting compiler/inference/proofs
Mar 24 18:16:04 Finished compiler/inference/proofs                                1s 124MB
Mar 24 18:16:05 Starting compiler/backend/semantics
Mar 24 18:19:10 Finished compiler/backend/semantics                            3m04s   2GB
Mar 24 18:19:11 Starting compiler/backend/reg_alloc/proofs
Mar 24 18:19:13 Finished compiler/backend/reg_alloc/proofs                        1s 118MB
Mar 24 18:19:14 Starting compiler/backend/proofs
Mar 24 18:20:05 Finished compiler/backend/proofs                                 50s   4GB
Mar 24 18:20:06 Starting compiler/backend/serialiser
Mar 24 18:20:09 Finished compiler/backend/serialiser                              1s 145MB
Mar 24 18:20:09 Starting compiler/encoders/x64/proofs
Mar 24 18:30:24 Finished compiler/encoders/x64/proofs                         10m13s   4GB
Mar 24 18:30:25 Starting compiler/encoders/arm7/proofs
Mar 24 18:43:42 Finished compiler/encoders/arm7/proofs                        13m16s   9GB
Mar 24 18:43:43 Starting compiler/encoders/arm8/proofs
Mar 24 18:50:37 Finished compiler/encoders/arm8/proofs                         6m52s   4GB
Mar 24 18:50:38 Starting compiler/encoders/arm8_asl/proofs
Mar 24 19:40:20 Finished compiler/encoders/arm8_asl/proofs                    49m40s  20GB
Mar 24 19:40:21 Starting compiler/encoders/mips/proofs
Mar 24 19:50:47 Finished compiler/encoders/mips/proofs                        10m25s  10GB
Mar 24 19:50:48 Starting compiler/encoders/riscv/proofs
Mar 24 19:58:58 Finished compiler/encoders/riscv/proofs                        8m09s   3GB
Mar 24 19:58:59 Starting compiler/encoders/ag32/proofs
Mar 24 20:01:50 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Mar 24 20:01:51 Starting compiler/backend/x64/proofs
Mar 24 20:02:23 Finished compiler/backend/x64/proofs                             31s   2GB
Mar 24 20:02:24 Starting compiler/backend/arm7/proofs
Mar 24 20:02:55 Finished compiler/backend/arm7/proofs                            30s   2GB
Mar 24 20:02:56 Starting compiler/backend/arm8/proofs
Mar 24 20:03:28 Finished compiler/backend/arm8/proofs                            30s   2GB
Mar 24 20:03:29 Starting compiler/backend/arm8_asl
Mar 24 20:03:50 Finished compiler/backend/arm8_asl                               19s   1GB
Mar 24 20:03:51 Starting compiler/backend/mips/proofs
Mar 24 20:04:22 Finished compiler/backend/mips/proofs                            30s   2GB
Mar 24 20:04:23 Starting compiler/backend/riscv/proofs
Mar 24 20:04:57 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 24 20:04:58 Starting compiler/backend/ag32/proofs
Mar 24 20:18:38 Finished compiler/backend/ag32/proofs                         13m39s   5GB
Mar 24 20:18:39 Starting compiler/backend/cv_compute
Mar 24 20:19:50 Finished compiler/backend/cv_compute                           1m10s   2GB
Mar 24 20:19:51 Starting cv_translator
Mar 24 20:40:33 Finished cv_translator                                        20m39s   9GB
Mar 24 20:40:34 Starting candle
Mar 24 20:40:35 Finished candle                                                   0s  12MB
Mar 24 20:40:36 Starting candle/set-theory
Mar 24 20:41:11 Finished candle/set-theory                                       33s   1GB
Mar 24 20:41:12 Starting candle/syntax-lib
Mar 24 20:41:14 Finished candle/syntax-lib                                        0s  93MB
Mar 24 20:41:15 Starting candle/standard
Mar 24 20:41:15 Finished candle/standard                                          0s  12MB
Mar 24 20:41:16 Starting candle/standard/syntax
Mar 24 20:41:29 Finished candle/standard/syntax                                  11s 786MB
Mar 24 20:41:30 Starting candle/standard/semantics
Mar 24 20:43:29 Finished candle/standard/semantics                             1m57s   2GB
Mar 24 20:43:29 Starting candle/standard/monadic
Mar 24 20:43:31 Finished candle/standard/monadic                                  1s 125MB
Mar 24 20:43:32 Starting candle/standard/ml_kernel
Mar 24 20:45:16 Finished candle/standard/ml_kernel                             1m42s   4GB
Mar 24 20:45:17 Starting candle/standard/ml_kernel/lisp
Mar 24 20:45:18 Finished candle/standard/ml_kernel/lisp                           0s  51MB
Mar 24 20:45:19 Starting candle/overloading
Mar 24 20:45:20 Finished candle/overloading                                       0s  12MB
Mar 24 20:45:21 Starting candle/overloading/syntax
Mar 24 20:48:31 Finished candle/overloading/syntax                             3m08s   2GB
Mar 24 20:48:32 Starting candle/overloading/semantics
Mar 24 20:59:23 Finished candle/overloading/semantics                         10m50s   4GB
Mar 24 20:59:24 Starting candle/overloading/monadic
Mar 24 21:01:41 Finished candle/overloading/monadic                            2m16s   2GB
Mar 24 21:01:42 Starting candle/overloading/ml_kernel
Mar 24 21:08:49 Finished candle/overloading/ml_kernel                          7m05s   6GB
Mar 24 21:08:50 Starting candle/overloading/ml_checker
Mar 24 21:10:59 Finished candle/overloading/ml_checker                         2m07s   6GB
Mar 24 21:11:00 Starting candle/prover
Mar 24 21:20:35 Finished candle/prover                                         9m34s   5GB
Mar 24 21:20:36 Starting candle/prover/compute
Mar 24 21:20:39 Finished candle/prover/compute                                    1s 144MB
Mar 24 21:20:40 Starting pancake
Mar 24 21:21:02 Finished pancake                                                 21s 843MB
Mar 24 21:21:02 Starting pancake/semantics
Mar 24 21:23:14 Finished pancake/semantics                                     2m10s   2GB
Mar 24 21:23:14 Starting pancake/parser
Mar 24 21:23:39 Finished pancake/parser                                          23s 438MB
Mar 24 21:23:40 Starting pancake/static_checker
Mar 24 21:24:17 Finished pancake/static_checker                                  36s   1GB
Mar 24 21:24:18 Starting pancake/proofs
Mar 24 21:40:27 Finished pancake/proofs                                       16m07s   6GB
Mar 24 21:40:28 Starting pancake/ta_progs
Mar 24 21:40:29 Finished pancake/ta_progs                                         0s  12MB
Mar 24 21:40:30 Starting compiler/dafny
Mar 24 21:43:33 Finished compiler/dafny                                        3m01s  11GB
Mar 24 21:43:34 Starting compiler/dafny/translation
Mar 24 22:02:32 Finished compiler/dafny/translation                           18m57s  15GB
Mar 24 22:02:33 Starting compiler/dafny/compilation
Mar 24 22:05:34 Finished compiler/dafny/compilation                            2m59s  11GB
Mar 24 22:05:35 Starting compiler/dafny/semantics
Mar 24 22:06:11 Finished compiler/dafny/semantics                                34s   1GB
Mar 24 22:06:12 Starting characteristic/examples
Mar 24 22:07:36 Finished characteristic/examples                               1m22s   4GB
Mar 24 22:07:36 Starting tutorial/solutions
Mar 24 22:10:06 Finished tutorial/solutions                                    2m28s   6GB
Mar 24 22:10:07 Starting translator/monadic/examples
Mar 24 22:12:58 Finished translator/monadic/examples                           2m49s   4GB
Mar 24 22:12:58 Starting examples
Mar 24 22:18:57 Finished examples                                              5m57s   4GB
Mar 24 22:18:58 Starting examples/compilation
Mar 24 22:18:59 Finished examples/compilation                                     0s  12MB
Mar 24 22:19:00 Starting examples/compilation/x64
Mar 24 22:26:02 Finished examples/compilation/x64                              7m01s   4GB
Mar 24 22:26:03 Starting examples/compilation/x64/proofs
Mar 24 22:28:31 Finished examples/compilation/x64/proofs                       2m26s   4GB
Mar 24 22:28:32 Starting examples/compilation/ag32
Mar 24 22:30:29 Finished examples/compilation/ag32                             1m55s   3GB
Mar 24 22:30:30 Starting examples/compilation/ag32/proofs
Mar 24 22:31:56 Finished examples/compilation/ag32/proofs                      1m25s   5GB
Mar 24 22:31:57 Starting examples/lpr_checker
Mar 24 22:32:27 Finished examples/lpr_checker                                    28s   1GB
Mar 24 22:32:27 Starting examples/lpr_checker/array
Mar 24 22:58:41 Finished examples/lpr_checker/array                           26m12s  28GB
Mar 24 22:58:42 Starting examples/lpr_checker/array/compilation
Mar 24 23:01:01 Finished examples/lpr_checker/array/compilation                2m17s   7GB
Mar 24 23:01:02 Starting examples/lpr_checker/array/compilation/proofs
Mar 24 23:02:12 Finished examples/lpr_checker/array/compilation/proofs         1m09s   6GB
Mar 24 23:02:13 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 24 23:03:17 Finished examples/lpr_checker/array/compilation/proofsARM8     1m03s   7GB
Mar 24 23:03:18 Starting .
Mar 24 23:03:21 Finished .                                                        2s 300MB
Mar 24 23:03:22 Starting examples/xlrup_checker
Mar 24 23:03:56 Finished examples/xlrup_checker                                  32s   1GB
Mar 24 23:03:57 Starting examples/xlrup_checker/array
Mar 24 23:16:54 Finished examples/xlrup_checker/array                         12m56s  11GB
Mar 24 23:16:55 Starting examples/xlrup_checker/array/compilation
Mar 24 23:18:01 Finished examples/xlrup_checker/array/compilation              1m04s   4GB
Mar 24 23:18:02 Starting examples/xlrup_checker/array/compilation/proofs
Mar 24 23:19:00 Finished examples/xlrup_checker/array/compilation/proofs         57s   4GB
Mar 24 23:19:01 Starting examples/pseudo_bool
Mar 24 23:20:31 Finished examples/pseudo_bool                                  1m29s   2GB
Mar 24 23:20:32 Starting examples/pseudo_bool/cnf_encoding
Mar 24 23:21:03 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Mar 24 23:21:04 Starting examples/pseudo_bool/graph_encoding
Mar 24 23:21:50 Finished examples/pseudo_bool/graph_encoding                     45s   2GB
Mar 24 23:21:51 Starting examples/pseudo_bool/array
Mar 25 00:29:51 Finished examples/pseudo_bool/array                         1h07m58s  47GB
Mar 25 00:29:52 Starting examples/pseudo_bool/array/compilation
Mar 25 00:39:17 Finished examples/pseudo_bool/array/compilation                9m23s  19GB
Mar 25 00:39:17 Starting examples/pseudo_bool/array/compilation/proofs
Mar 25 00:41:52 Finished examples/pseudo_bool/array/compilation/proofs         2m33s   6GB
Mar 25 00:41:53 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 25 00:42:59 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m05s   6GB
Mar 25 00:43:00 Starting examples/opentheory
Mar 25 00:51:26 Finished examples/opentheory                                   8m24s   5GB
Mar 25 00:51:27 Starting examples/opentheory/compilation
Mar 25 00:53:02 Finished examples/opentheory/compilation                       1m33s   6GB
Mar 25 00:53:03 Starting examples/opentheory/compilation/proofs
Mar 25 00:54:06 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Mar 25 00:54:07 Starting examples/opentheory/compilation/ag32
Mar 25 00:55:44 Finished examples/opentheory/compilation/ag32                  1m36s   7GB
Mar 25 00:55:45 Starting examples/opentheory/compilation/ag32/proofs
Mar 25 00:57:21 Finished examples/opentheory/compilation/ag32/proofs           1m34s   8GB
Mar 25 00:57:22 Starting examples/sat_encodings
Mar 25 00:58:22 Finished examples/sat_encodings                                  58s 876MB
Mar 25 00:58:23 Starting examples/sat_encodings/demo
Mar 25 00:58:24 Finished examples/sat_encodings/demo                              0s  12MB
Mar 25 00:58:24 Starting examples/sat_encodings/case_studies
Mar 25 01:00:10 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Mar 25 01:00:11 Starting examples/sat_encodings/translation
Mar 25 01:03:50 Finished examples/sat_encodings/translation                    3m37s   3GB
Mar 25 01:03:51 Starting examples/sat_encodings/translation/compilation
Mar 25 01:05:46 Finished examples/sat_encodings/translation/compilation        1m54s   4GB
Mar 25 01:05:47 Starting examples/deflate
Mar 25 01:06:15 Finished examples/deflate                                        26s 770MB
Mar 25 01:06:16 Starting examples/deflate/translation
Mar 25 01:07:21 Finished examples/deflate/translation                          1m04s   4GB
Mar 25 01:07:22 Starting examples/deflate/translation/compilation
Mar 25 01:08:13 Finished examples/deflate/translation/compilation                50s   3GB
Mar 25 01:08:14 Starting examples/vipr
Mar 25 01:11:49 Finished examples/vipr                                         3m33s   7GB
Mar 25 01:11:50 Starting examples/vipr/compilation
Mar 25 01:12:46 Finished examples/vipr/compilation                               55s   4GB
Mar 25 01:12:47 Starting translator/okasaki-examples
Mar 25 01:16:52 Finished translator/okasaki-examples                           4m03s   3GB
Mar 25 01:16:53 Starting translator/other-examples
Mar 25 01:19:57 Finished translator/other-examples                             3m03s   2GB
Mar 25 01:19:58 Starting translator/other-examples/auxiliary
Mar 25 01:19:59 Finished translator/other-examples/auxiliary                      0s  13MB
Mar 25 01:20:00 Starting compiler/parsing/tests
Mar 25 01:20:35 Finished compiler/parsing/tests                                  34s   1GB
Mar 25 01:20:36 Starting compiler/inference/tests
Mar 25 01:21:12 Finished compiler/inference/tests                                34s   2GB
Mar 25 01:21:13 Starting compiler/printing/test
Mar 25 01:22:25 Finished compiler/printing/test                                1m11s   6GB
Mar 25 01:22:26 Starting icing/flover
Mar 25 01:56:16 Finished icing/flover                                         33m48s   2GB
Mar 25 01:56:17 Starting icing/flover/Infra
Mar 25 01:56:18 Finished icing/flover/Infra                                       0s  13MB
Mar 25 01:56:19 Starting icing/flover/semantics
Mar 25 01:56:20 Finished icing/flover/semantics                                   0s  15MB
Mar 25 01:56:21 Starting icing/
Mar 25 02:23:50 Finished icing/                                               27m28s   4GB
Mar 25 02:23:51 Starting icing/examples
Mar 25 02:25:25 Finished icing/examples                                        1m32s   7GB
Mar 25 02:25:26 Starting compiler/repl
Mar 25 02:33:29 Finished compiler/repl                                         8m02s   5GB
Mar 25 02:33:30 Starting unverified/sexpr-bootstrap/x64/64
Mar 25 02:37:29 Finished unverified/sexpr-bootstrap/x64/64                     3m57s  17GB
Mar 25 02:37:30 Starting unverified/sexpr-bootstrap/x64/32
Mar 25 02:40:49 Finished unverified/sexpr-bootstrap/x64/32                     3m17s  15GB
Mar 25 02:40:50 Starting compiler/benchmarks
Mar 25 02:41:36 Finished compiler/benchmarks                                     45s 711MB
Mar 25 02:41:36 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 25 02:41:40 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 256MB
Mar 25 02:41:41 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 25 02:41:44 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 258MB
Mar 25 02:41:45 Starting compiler/bootstrap/compilation/x64/64
Mar 25 03:11:59 Finished compiler/bootstrap/compilation/x64/64                30m13s  92GB
Mar 25 03:12:00 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 25 03:35:13 Finished compiler/bootstrap/compilation/x64/64/proofs         23m11s  40GB
Mar 25 03:35:14 Starting compiler/bootstrap/compilation/x64/32
Mar 25 04:04:13 Finished compiler/bootstrap/compilation/x64/32                28m57s  84GB
Mar 25 04:04:14 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 25 04:08:34 Finished compiler/bootstrap/compilation/x64/32/proofs          4m19s  24GB
Mar 25 04:08:35 Starting compiler/bootstrap/compilation/arm8/64
Mar 25 04:52:13 Finished compiler/bootstrap/compilation/arm8/64               43m36s 108GB
Mar 25 04:52:14 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 25 04:57:47 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m32s  28GB
Mar 25 04:57:48 Starting compiler/bootstrap/compilation/ag32/32
Mar 25 05:29:16 Finished compiler/bootstrap/compilation/ag32/32               31m26s  87GB
Mar 25 05:29:17 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 25 05:34:20 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m02s  30GB
Mar 25 05:34:21 SUCCESS