Job 2787

CakeML:7fdf474c0bf29dd6810d02d08ec18c6dd0535974
  Fix remaining stuff [Mar 19 17:16:48]
#1142 (remove_more_misc)
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:pavlova

Mar 24 08:13:28 Claimed job
Mar 24 08:13:37 Building HOL
Mar 24 08:24:30 Starting developers
Mar 24 08:24:34 Finished developers                                               3s 193MB
Mar 24 08:24:35 Starting developers/bin
Mar 24 08:24:41 Finished developers/bin                                           5s 746MB
Mar 24 08:24:42 Starting misc
Mar 24 08:25:43 Finished misc                                                    59s   2GB
Mar 24 08:25:43 Starting compiler/proofs
Mar 24 10:13:20 Finished compiler/proofs                                    1h47m35s  49GB
Mar 24 10:13:21 Starting compiler/bootstrap/translation
Mar 24 16:04:32 Finished compiler/bootstrap/translation                     5h51m10s  99GB
Mar 24 16:04:33 Starting semantics/ffi
Mar 24 16:04:43 Finished semantics/ffi                                            9s 591MB
Mar 24 16:04:44 Starting semantics
Mar 24 16:04:45 Finished semantics                                                0s  55MB
Mar 24 16:04:46 Starting semantics/proofs
Mar 24 16:05:09 Finished semantics/proofs                                        22s 852MB
Mar 24 16:05:10 Starting semantics/alt_semantics
Mar 24 16:05:31 Finished semantics/alt_semantics                                 19s 896MB
Mar 24 16:05:32 Starting semantics/alt_semantics/proofs
Mar 24 16:15:46 Finished semantics/alt_semantics/proofs                       10m12s   2GB
Mar 24 16:15:47 Starting basis/pure
Mar 24 16:15:49 Finished basis/pure                                               0s  98MB
Mar 24 16:15:50 Starting translator
Mar 24 16:17:19 Finished translator                                            1m28s   3GB
Mar 24 16:17:20 Starting compiler/parsing
Mar 24 16:17:21 Finished compiler/parsing                                         0s  61MB
Mar 24 16:17:22 Starting characteristic
Mar 24 16:17:24 Finished characteristic                                           1s 117MB
Mar 24 16:17:25 Starting translator/monadic
Mar 24 16:17:27 Finished translator/monadic                                       1s 113MB
Mar 24 16:17:28 Starting translator/monadic/monad_base
Mar 24 16:17:29 Finished translator/monadic/monad_base                            0s  54MB
Mar 24 16:17:30 Starting basis
Mar 24 16:19:50 Finished basis                                                 2m19s   3GB
Mar 24 16:19:51 Starting compiler
Mar 24 16:19:54 Finished compiler                                                 1s 219MB
Mar 24 16:19:55 Starting compiler/inference
Mar 24 16:19:57 Finished compiler/inference                                       1s 121MB
Mar 24 16:19:58 Starting compiler/backend/reg_alloc
Mar 24 16:19:59 Finished compiler/backend/reg_alloc                               0s  58MB
Mar 24 16:20:00 Starting compiler/backend/gc
Mar 24 16:20:02 Finished compiler/backend/gc                                      1s 137MB
Mar 24 16:20:03 Starting compiler/backend
Mar 24 16:20:08 Finished compiler/backend                                         4s 265MB
Mar 24 16:20:09 Starting compiler/encoders/asm
Mar 24 16:20:11 Finished compiler/encoders/asm                                    0s  88MB
Mar 24 16:20:12 Starting compiler/encoders/x64
Mar 24 16:20:14 Finished compiler/encoders/x64                                    0s  90MB
Mar 24 16:20:14 Starting compiler/encoders/arm7
Mar 24 16:20:16 Finished compiler/encoders/arm7                                   0s  90MB
Mar 24 16:20:17 Starting compiler/encoders/arm8
Mar 24 16:20:19 Finished compiler/encoders/arm8                                   0s  89MB
Mar 24 16:20:20 Starting compiler/encoders/arm8_asl
Mar 24 18:22:58 Finished compiler/encoders/arm8_asl                         2h02m37s  40GB
Mar 24 18:22:59 Starting compiler/encoders/mips
Mar 24 18:23:01 Finished compiler/encoders/mips                                   0s  84MB
Mar 24 18:23:02 Starting compiler/encoders/riscv
Mar 24 18:23:03 Finished compiler/encoders/riscv                                  0s  87MB
Mar 24 18:23:04 Starting compiler/encoders/ag32
Mar 24 18:23:06 Finished compiler/encoders/ag32                                   0s  81MB
Mar 24 18:23:07 Starting compiler/encoders/tests
Mar 24 18:23:09 Finished compiler/encoders/tests                                  1s 107MB
Mar 24 18:23:10 Starting compiler/encoders/monadic_enc
Mar 24 18:23:12 Finished compiler/encoders/monadic_enc                            1s 133MB
Mar 24 18:23:13 Starting compiler/backend/x64
Mar 24 18:23:15 Finished compiler/backend/x64                                     1s 138MB
Mar 24 18:23:16 Starting compiler/backend/arm7
Mar 24 18:23:18 Finished compiler/backend/arm7                                    1s 142MB
Mar 24 18:23:19 Starting compiler/backend/arm8
Mar 24 18:23:21 Finished compiler/backend/arm8                                    1s 143MB
Mar 24 18:23:22 Starting compiler/backend/mips
Mar 24 18:23:24 Finished compiler/backend/mips                                    1s 143MB
Mar 24 18:23:25 Starting compiler/backend/riscv
Mar 24 18:23:27 Finished compiler/backend/riscv                                   1s 138MB
Mar 24 18:23:28 Starting compiler/backend/ag32
Mar 24 18:24:36 Finished compiler/backend/ag32                                 1m07s   3GB
Mar 24 18:24:37 Starting compiler/backend/pattern_matching
Mar 24 18:24:38 Finished compiler/backend/pattern_matching                        0s  54MB
Mar 24 18:24:39 Starting compiler/parsing/ocaml
Mar 24 18:26:21 Finished compiler/parsing/ocaml                                1m41s   1GB
Mar 24 18:26:22 Starting compiler/printing
Mar 24 18:26:24 Finished compiler/printing                                        1s 112MB
Mar 24 18:26:25 Starting compiler/parsing/proofs
Mar 24 18:26:27 Finished compiler/parsing/proofs                                  0s  62MB
Mar 24 18:26:28 Starting compiler/inference/proofs
Mar 24 18:26:30 Finished compiler/inference/proofs                                1s 113MB
Mar 24 18:26:31 Starting compiler/backend/semantics
Mar 24 18:29:40 Finished compiler/backend/semantics                            3m08s   2GB
Mar 24 18:29:40 Starting compiler/backend/reg_alloc/proofs
Mar 24 18:29:43 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Mar 24 18:29:43 Starting compiler/backend/proofs
Mar 24 18:30:33 Finished compiler/backend/proofs                                 48s   3GB
Mar 24 18:30:34 Starting compiler/backend/serialiser
Mar 24 18:30:36 Finished compiler/backend/serialiser                              1s 146MB
Mar 24 18:30:37 Starting compiler/encoders/x64/proofs
Mar 24 18:40:53 Finished compiler/encoders/x64/proofs                         10m14s   4GB
Mar 24 18:40:54 Starting compiler/encoders/arm7/proofs
Mar 24 18:54:03 Finished compiler/encoders/arm7/proofs                        13m08s   8GB
Mar 24 18:54:04 Starting compiler/encoders/arm8/proofs
Mar 24 19:01:02 Finished compiler/encoders/arm8/proofs                         6m56s   3GB
Mar 24 19:01:03 Starting compiler/encoders/arm8_asl/proofs
Mar 24 19:50:33 Finished compiler/encoders/arm8_asl/proofs                    49m27s  20GB
Mar 24 19:50:34 Starting compiler/encoders/mips/proofs
Mar 24 20:00:46 Finished compiler/encoders/mips/proofs                        10m11s   8GB
Mar 24 20:00:47 Starting compiler/encoders/riscv/proofs
Mar 24 20:09:00 Finished compiler/encoders/riscv/proofs                        8m12s   5GB
Mar 24 20:09:01 Starting compiler/encoders/ag32/proofs
Mar 24 20:11:53 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Mar 24 20:11:54 Starting compiler/backend/x64/proofs
Mar 24 20:12:24 Finished compiler/backend/x64/proofs                             29s   2GB
Mar 24 20:12:25 Starting compiler/backend/arm7/proofs
Mar 24 20:12:57 Finished compiler/backend/arm7/proofs                            30s   2GB
Mar 24 20:12:58 Starting compiler/backend/arm8/proofs
Mar 24 20:13:27 Finished compiler/backend/arm8/proofs                            28s   2GB
Mar 24 20:13:28 Starting compiler/backend/arm8_asl
Mar 24 20:13:51 Finished compiler/backend/arm8_asl                               22s   2GB
Mar 24 20:13:52 Starting compiler/backend/mips/proofs
Mar 24 20:14:24 Finished compiler/backend/mips/proofs                            30s   2GB
Mar 24 20:14:25 Starting compiler/backend/riscv/proofs
Mar 24 20:14:56 Finished compiler/backend/riscv/proofs                           30s   2GB
Mar 24 20:14:57 Starting compiler/backend/ag32/proofs
Mar 24 20:28:58 Finished compiler/backend/ag32/proofs                         13m59s   5GB
Mar 24 20:28:59 Starting compiler/backend/cv_compute
Mar 24 20:30:09 Finished compiler/backend/cv_compute                           1m09s   2GB
Mar 24 20:30:10 Starting cv_translator
Mar 24 20:51:07 Finished cv_translator                                        20m55s   8GB
Mar 24 20:51:08 Starting candle
Mar 24 20:51:09 Finished candle                                                   0s  11MB
Mar 24 20:51:10 Starting candle/set-theory
Mar 24 20:51:45 Finished candle/set-theory                                       34s   1GB
Mar 24 20:51:46 Starting candle/syntax-lib
Mar 24 20:51:48 Finished candle/syntax-lib                                        0s  90MB
Mar 24 20:51:48 Starting candle/standard
Mar 24 20:51:49 Finished candle/standard                                          0s  11MB
Mar 24 20:51:50 Starting candle/standard/syntax
Mar 24 20:52:03 Finished candle/standard/syntax                                  11s 792MB
Mar 24 20:52:04 Starting candle/standard/semantics
Mar 24 20:54:05 Finished candle/standard/semantics                             2m00s   2GB
Mar 24 20:54:06 Starting candle/standard/monadic
Mar 24 20:54:08 Finished candle/standard/monadic                                  1s 125MB
Mar 24 20:54:09 Starting candle/standard/ml_kernel
Mar 24 20:55:53 Finished candle/standard/ml_kernel                             1m43s   4GB
Mar 24 20:55:54 Starting candle/standard/ml_kernel/lisp
Mar 24 20:55:55 Finished candle/standard/ml_kernel/lisp                           0s  52MB
Mar 24 20:55:56 Starting candle/overloading
Mar 24 20:55:57 Finished candle/overloading                                       0s  11MB
Mar 24 20:55:58 Starting candle/overloading/syntax
Mar 24 20:59:10 Finished candle/overloading/syntax                             3m11s   2GB
Mar 24 20:59:11 Starting candle/overloading/semantics
Mar 24 21:10:12 Finished candle/overloading/semantics                         11m00s   4GB
Mar 24 21:10:13 Starting candle/overloading/monadic
Mar 24 21:12:32 Finished candle/overloading/monadic                            2m17s   2GB
Mar 24 21:12:33 Starting candle/overloading/ml_kernel
Mar 24 21:19:43 Finished candle/overloading/ml_kernel                          7m09s   5GB
Mar 24 21:19:44 Starting candle/overloading/ml_checker
Mar 24 21:21:53 Finished candle/overloading/ml_checker                         2m08s   5GB
Mar 24 21:21:54 Starting candle/prover
Mar 24 21:31:40 Finished candle/prover                                         9m45s   5GB
Mar 24 21:31:41 Starting candle/prover/compute
Mar 24 21:31:43 Finished candle/prover/compute                                    1s 145MB
Mar 24 21:31:44 Starting pancake
Mar 24 21:32:07 Finished pancake                                                 21s 830MB
Mar 24 21:32:07 Starting pancake/semantics
Mar 24 21:34:19 Finished pancake/semantics                                     2m10s   2GB
Mar 24 21:34:20 Starting pancake/parser
Mar 24 21:34:44 Finished pancake/parser                                          22s 445MB
Mar 24 21:34:45 Starting pancake/static_checker
Mar 24 21:35:22 Finished pancake/static_checker                                  36s   1GB
Mar 24 21:35:23 Starting pancake/proofs
Mar 24 21:51:40 Finished pancake/proofs                                       16m15s   7GB
Mar 24 21:51:40 Starting pancake/ta_progs
Mar 24 21:51:41 Finished pancake/ta_progs                                         0s  12MB
Mar 24 21:51:42 Starting compiler/dafny
Mar 24 21:54:53 Finished compiler/dafny                                        3m09s  10GB
Mar 24 21:54:54 Starting compiler/dafny/translation
Mar 24 22:14:19 Finished compiler/dafny/translation                           19m24s  22GB
Mar 24 22:14:20 Starting compiler/dafny/compilation
Mar 24 22:17:27 Finished compiler/dafny/compilation                            3m06s  11GB
Mar 24 22:17:28 Starting compiler/dafny/semantics
Mar 24 22:18:05 Finished compiler/dafny/semantics                                35s   1GB
Mar 24 22:18:06 Starting characteristic/examples
Mar 24 22:19:31 Finished characteristic/examples                               1m24s   4GB
Mar 24 22:19:32 Starting tutorial/solutions
Mar 24 22:21:59 Finished tutorial/solutions                                    2m26s   3GB
Mar 24 22:22:00 Starting translator/monadic/examples
Mar 24 22:24:54 Finished translator/monadic/examples                           2m53s   3GB
Mar 24 22:24:55 Starting examples
Mar 24 22:30:58 Finished examples                                              6m02s   4GB
Mar 24 22:30:59 Starting examples/compilation
Mar 24 22:31:00 Finished examples/compilation                                     0s  12MB
Mar 24 22:31:01 Starting examples/compilation/x64
Mar 24 22:37:58 Finished examples/compilation/x64                              6m56s   4GB
Mar 24 22:37:59 Starting examples/compilation/x64/proofs
Mar 24 22:40:22 Finished examples/compilation/x64/proofs                       2m22s   4GB
Mar 24 22:40:23 Starting examples/compilation/ag32
Mar 24 22:42:17 Finished examples/compilation/ag32                             1m52s   3GB
Mar 24 22:42:17 Starting examples/compilation/ag32/proofs
Mar 24 22:43:17 Finished examples/compilation/ag32/proofs                        58s   5GB
Mar 24 22:43:18 Starting examples/lpr_checker
Mar 24 22:43:49 Finished examples/lpr_checker                                    29s   1GB
Mar 24 22:43:49 Starting examples/lpr_checker/array
Mar 24 23:09:47 Finished examples/lpr_checker/array                           25m56s  20GB
Mar 24 23:09:48 Starting examples/lpr_checker/array/compilation
Mar 24 23:12:14 Finished examples/lpr_checker/array/compilation                2m25s   7GB
Mar 24 23:12:15 Starting examples/lpr_checker/array/compilation/proofs
Mar 24 23:13:48 Finished examples/lpr_checker/array/compilation/proofs         1m32s   6GB
Mar 24 23:13:49 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 24 23:14:57 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Mar 24 23:14:58 Starting .
Mar 24 23:15:02 Finished .                                                        2s 306MB
Mar 24 23:15:03 Starting examples/xlrup_checker
Mar 24 23:15:38 Finished examples/xlrup_checker                                  33s   1GB
Mar 24 23:15:39 Starting examples/xlrup_checker/array
Mar 24 23:28:35 Finished examples/xlrup_checker/array                         12m55s   8GB
Mar 24 23:28:36 Starting examples/xlrup_checker/array/compilation
Mar 24 23:29:38 Finished examples/xlrup_checker/array/compilation              1m01s   4GB
Mar 24 23:29:39 Starting examples/xlrup_checker/array/compilation/proofs
Mar 24 23:30:37 Finished examples/xlrup_checker/array/compilation/proofs         56s   4GB
Mar 24 23:30:38 Starting examples/pseudo_bool
Mar 24 23:32:07 Finished examples/pseudo_bool                                  1m28s   2GB
Mar 24 23:32:08 Starting examples/pseudo_bool/cnf_encoding
Mar 24 23:32:37 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Mar 24 23:32:38 Starting examples/pseudo_bool/graph_encoding
Mar 24 23:33:23 Finished examples/pseudo_bool/graph_encoding                     44s   2GB
Mar 24 23:33:24 Starting examples/pseudo_bool/array
Mar 25 00:41:53 Finished examples/pseudo_bool/array                         1h08m27s  38GB
Mar 25 00:41:54 Starting examples/pseudo_bool/array/compilation
Mar 25 00:51:27 Finished examples/pseudo_bool/array/compilation                9m31s  19GB
Mar 25 00:51:28 Starting examples/pseudo_bool/array/compilation/proofs
Mar 25 00:54:01 Finished examples/pseudo_bool/array/compilation/proofs         2m32s   6GB
Mar 25 00:54:02 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 25 00:55:12 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m09s   6GB
Mar 25 00:55:13 Starting examples/opentheory
Mar 25 01:03:42 Finished examples/opentheory                                   8m27s   5GB
Mar 25 01:03:43 Starting examples/opentheory/compilation
Mar 25 01:05:18 Finished examples/opentheory/compilation                       1m33s   6GB
Mar 25 01:05:18 Starting examples/opentheory/compilation/proofs
Mar 25 01:06:22 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Mar 25 01:06:23 Starting examples/opentheory/compilation/ag32
Mar 25 01:08:00 Finished examples/opentheory/compilation/ag32                  1m36s   7GB
Mar 25 01:08:01 Starting examples/opentheory/compilation/ag32/proofs
Mar 25 01:09:41 Finished examples/opentheory/compilation/ag32/proofs           1m38s   8GB
Mar 25 01:09:42 Starting examples/sat_encodings
Mar 25 01:10:42 Finished examples/sat_encodings                                  59s 897MB
Mar 25 01:10:43 Starting examples/sat_encodings/demo
Mar 25 01:10:44 Finished examples/sat_encodings/demo                              0s  10MB
Mar 25 01:10:45 Starting examples/sat_encodings/case_studies
Mar 25 01:12:28 Finished examples/sat_encodings/case_studies                   1m41s   1GB
Mar 25 01:12:29 Starting examples/sat_encodings/translation
Mar 25 01:16:08 Finished examples/sat_encodings/translation                    3m38s   2GB
Mar 25 01:16:09 Starting examples/sat_encodings/translation/compilation
Mar 25 01:18:03 Finished examples/sat_encodings/translation/compilation        1m53s   4GB
Mar 25 01:18:04 Starting examples/deflate
Mar 25 01:18:32 Finished examples/deflate                                        27s 705MB
Mar 25 01:18:33 Starting examples/deflate/translation
Mar 25 01:19:39 Finished examples/deflate/translation                          1m04s   4GB
Mar 25 01:19:39 Starting examples/deflate/translation/compilation
Mar 25 01:20:32 Finished examples/deflate/translation/compilation                51s   4GB
Mar 25 01:20:32 Starting examples/vipr
Mar 25 01:24:09 Finished examples/vipr                                         3m35s   7GB
Mar 25 01:24:10 Starting examples/vipr/compilation
Mar 25 01:25:07 Finished examples/vipr/compilation                               56s   4GB
Mar 25 01:25:08 Starting translator/okasaki-examples
Mar 25 01:29:08 Finished translator/okasaki-examples                           3m59s   4GB
Mar 25 01:29:09 Starting translator/other-examples
Mar 25 01:32:13 Finished translator/other-examples                             3m02s   3GB
Mar 25 01:32:14 Starting translator/other-examples/auxiliary
Mar 25 01:32:15 Finished translator/other-examples/auxiliary                      0s  13MB
Mar 25 01:32:16 Starting compiler/parsing/tests
Mar 25 01:32:51 Finished compiler/parsing/tests                                  34s   1GB
Mar 25 01:32:52 Starting compiler/inference/tests
Mar 25 01:33:28 Finished compiler/inference/tests                                35s   2GB
Mar 25 01:33:29 Starting compiler/printing/test
Mar 25 01:34:40 Finished compiler/printing/test                                1m10s   6GB
Mar 25 01:34:41 Starting icing/flover
Mar 25 02:09:05 Finished icing/flover                                         34m23s   2GB
Mar 25 02:09:06 Starting icing/flover/Infra
Mar 25 02:09:07 Finished icing/flover/Infra                                       0s  13MB
Mar 25 02:09:08 Starting icing/flover/semantics
Mar 25 02:09:09 Finished icing/flover/semantics                                   0s  15MB
Mar 25 02:09:10 Starting icing/
Mar 25 02:36:13 Finished icing/                                               27m02s   4GB
Mar 25 02:36:14 Starting icing/examples
Mar 25 02:37:47 Finished icing/examples                                        1m31s   7GB
Mar 25 02:37:48 Starting compiler/repl
Mar 25 02:45:42 Finished compiler/repl                                         7m52s   5GB
Mar 25 02:45:43 Starting unverified/sexpr-bootstrap/x64/64
Mar 25 02:49:37 Finished unverified/sexpr-bootstrap/x64/64                     3m53s  19GB
Mar 25 02:49:38 Starting unverified/sexpr-bootstrap/x64/32
Mar 25 02:53:02 Finished unverified/sexpr-bootstrap/x64/32                     3m23s  15GB
Mar 25 02:53:03 Starting compiler/benchmarks
Mar 25 02:53:48 Finished compiler/benchmarks                                     44s 711MB
Mar 25 02:53:49 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 25 02:53:53 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 256MB
Mar 25 02:53:54 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 25 02:53:57 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 251MB
Mar 25 02:53:58 Starting compiler/bootstrap/compilation/x64/64
Mar 25 03:23:22 Finished compiler/bootstrap/compilation/x64/64                29m23s 100GB
Mar 25 03:23:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 25 03:47:31 Finished compiler/bootstrap/compilation/x64/64/proofs         24m07s  58GB
Mar 25 03:47:32 Starting compiler/bootstrap/compilation/x64/32
Mar 25 04:17:29 Finished compiler/bootstrap/compilation/x64/32                29m56s  83GB
Mar 25 04:17:30 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 25 04:21:42 Finished compiler/bootstrap/compilation/x64/32/proofs          4m10s  25GB
Mar 25 04:21:43 Starting compiler/bootstrap/compilation/arm8/64
Mar 25 05:02:19 Finished compiler/bootstrap/compilation/arm8/64               40m35s 112GB
Mar 25 05:02:20 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 25 05:07:29 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m08s  29GB
Mar 25 05:07:30 Starting compiler/bootstrap/compilation/ag32/32
Mar 25 05:36:52 Finished compiler/bootstrap/compilation/ag32/32               29m21s  76GB
Mar 25 05:36:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 25 05:41:36 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m42s  29GB
Mar 25 05:41:37 SUCCESS