Job 2341

CakeML:be19f70183bcd3ad0bc914db3efc35ffdde01f5c
  fix bootstrap/compilation proofs for ag32 [Mar 14 10:45:56]
#977 (share_mem_new2)
Merging into:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:3a51c81db857b7722efa0871ac507883adf6d440
  Remove compilerTheory (put its content at end of codegenTheory) [Mar 11 19:26:17]
Machine:pavlova

Mar 14 12:24:27 Claimed job
Mar 14 12:24:31 Reusing HOL
Mar 14 12:24:41 Starting developers
Mar 14 12:24:45 Finished developers                                               2s 217MB
Mar 14 12:24:46 Starting developers/bin
Mar 14 12:24:56 Finished developers/bin                                           9s   1GB
Mar 14 12:24:57 Starting compiler/proofs
Mar 14 14:14:26 Finished compiler/proofs                                    1h49m28s  35GB
Mar 14 14:14:27 Starting compiler/bootstrap/translation
Mar 14 22:17:44 Finished compiler/bootstrap/translation                     8h03m15s  86GB
Mar 14 22:17:45 Starting semantics/ffi
Mar 14 22:17:53 Finished semantics/ffi                                            7s 674MB
Mar 14 22:17:54 Starting semantics
Mar 14 22:17:55 Finished semantics                                                0s  66MB
Mar 14 22:17:56 Starting semantics/proofs
Mar 14 22:18:33 Finished semantics/proofs                                        36s   1GB
Mar 14 22:18:34 Starting semantics/alt_semantics
Mar 14 22:19:14 Finished semantics/alt_semantics                                 38s   1GB
Mar 14 22:19:15 Starting semantics/alt_semantics/proofs
Mar 14 22:30:16 Finished semantics/alt_semantics/proofs                       11m00s   4GB
Mar 14 22:30:17 Starting basis/pure
Mar 14 22:30:18 Finished basis/pure                                               0s  69MB
Mar 14 22:30:19 Starting translator
Mar 14 22:32:01 Finished translator                                            1m40s   3GB
Mar 14 22:32:02 Starting compiler/parsing
Mar 14 22:32:03 Finished compiler/parsing                                         0s  67MB
Mar 14 22:32:04 Starting characteristic
Mar 14 22:32:06 Finished characteristic                                           0s  88MB
Mar 14 22:32:07 Starting translator/monadic
Mar 14 22:32:08 Finished translator/monadic                                       0s  91MB
Mar 14 22:32:09 Starting basis
Mar 14 22:35:45 Finished basis                                                 3m35s   4GB
Mar 14 22:35:46 Starting compiler/inference
Mar 14 22:35:48 Finished compiler/inference                                       0s  83MB
Mar 14 22:35:48 Starting compiler/backend/reg_alloc
Mar 14 22:35:50 Finished compiler/backend/reg_alloc                               0s  67MB
Mar 14 22:35:51 Starting compiler/backend/gc
Mar 14 22:35:52 Finished compiler/backend/gc                                      0s 141MB
Mar 14 22:35:53 Starting compiler/backend
Mar 14 22:36:11 Finished compiler/backend                                        17s   1GB
Mar 14 22:36:12 Starting compiler/encoders/asm
Mar 14 22:36:14 Finished compiler/encoders/asm                                    0s  92MB
Mar 14 22:36:15 Starting compiler/encoders/x64
Mar 14 22:36:16 Finished compiler/encoders/x64                                    0s  94MB
Mar 14 22:36:17 Starting compiler/encoders/arm7
Mar 14 22:36:18 Finished compiler/encoders/arm7                                   0s  93MB
Mar 14 22:36:19 Starting compiler/encoders/arm8
Mar 14 22:36:21 Finished compiler/encoders/arm8                                   0s  93MB
Mar 14 22:36:22 Starting compiler/encoders/arm8_asl
Mar 14 22:38:38 Finished compiler/encoders/arm8_asl                            2m15s   1GB
Mar 14 22:38:39 Starting compiler/encoders/mips
Mar 14 22:38:41 Finished compiler/encoders/mips                                   0s  93MB
Mar 14 22:38:42 Starting compiler/encoders/riscv
Mar 14 22:38:43 Finished compiler/encoders/riscv                                  0s  93MB
Mar 14 22:38:44 Starting compiler/encoders/ag32
Mar 14 22:38:46 Finished compiler/encoders/ag32                                   0s  92MB
Mar 14 22:38:47 Starting compiler/backend/x64
Mar 14 22:38:48 Finished compiler/backend/x64                                     0s 130MB
Mar 14 22:38:49 Starting compiler/backend/arm7
Mar 14 22:38:51 Finished compiler/backend/arm7                                    0s 126MB
Mar 14 22:38:52 Starting compiler/backend/arm8
Mar 14 22:38:54 Finished compiler/backend/arm8                                    0s 126MB
Mar 14 22:38:55 Starting compiler/backend/mips
Mar 14 22:38:56 Finished compiler/backend/mips                                    0s 126MB
Mar 14 22:38:57 Starting compiler/backend/riscv
Mar 14 22:38:59 Finished compiler/backend/riscv                                   0s 126MB
Mar 14 22:39:00 Starting compiler/backend/ag32
Mar 14 22:40:20 Finished compiler/backend/ag32                                 1m19s   4GB
Mar 14 22:40:21 Starting compiler/parsing/proofs
Mar 14 22:40:23 Finished compiler/parsing/proofs                                  0s  78MB
Mar 14 22:40:24 Starting compiler/inference/proofs
Mar 14 22:40:25 Finished compiler/inference/proofs                                0s  89MB
Mar 14 22:40:26 Starting compiler/backend/semantics
Mar 14 22:44:09 Finished compiler/backend/semantics                            3m42s   3GB
Mar 14 22:44:10 Starting compiler/backend/reg_alloc/proofs
Mar 14 22:44:12 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Mar 14 22:44:12 Starting compiler/backend/proofs
Mar 14 22:45:16 Finished compiler/backend/proofs                               1m02s   2GB
Mar 14 22:45:17 Starting compiler/backend/serialiser
Mar 14 22:45:19 Finished compiler/backend/serialiser                              1s 193MB
Mar 14 22:45:20 Starting compiler/encoders/x64/proofs
Mar 14 22:54:46 Finished compiler/encoders/x64/proofs                          9m24s   5GB
Mar 14 22:54:47 Starting compiler/encoders/arm7/proofs
Mar 14 23:07:37 Finished compiler/encoders/arm7/proofs                        12m49s  12GB
Mar 14 23:07:38 Starting compiler/encoders/arm8/proofs
Mar 14 23:13:58 Finished compiler/encoders/arm8/proofs                         6m18s   6GB
Mar 14 23:13:59 Starting compiler/encoders/arm8_asl/proofs
Mar 14 23:27:53 Finished compiler/encoders/arm8_asl/proofs                    13m53s   4GB
Mar 14 23:27:54 Starting compiler/encoders/mips/proofs
Mar 14 23:38:07 Finished compiler/encoders/mips/proofs                        10m11s  10GB
Mar 14 23:38:08 Starting compiler/encoders/riscv/proofs
Mar 14 23:46:32 Finished compiler/encoders/riscv/proofs                        8m23s   4GB
Mar 14 23:46:33 Starting compiler/encoders/ag32/proofs
Mar 14 23:48:56 Finished compiler/encoders/ag32/proofs                         2m21s   3GB
Mar 14 23:48:56 Starting compiler/backend/x64/proofs
Mar 14 23:49:38 Finished compiler/backend/x64/proofs                             40s   2GB
Mar 14 23:49:39 Starting compiler/backend/arm7/proofs
Mar 14 23:50:27 Finished compiler/backend/arm7/proofs                            47s   3GB
Mar 14 23:50:28 Starting compiler/backend/arm8/proofs
Mar 14 23:51:08 Finished compiler/backend/arm8/proofs                            38s   3GB
Mar 14 23:51:09 Starting compiler/backend/arm8_asl
Mar 14 23:51:39 Finished compiler/backend/arm8_asl                               29s   2GB
Mar 14 23:51:40 Starting compiler/backend/mips/proofs
Mar 14 23:52:25 Finished compiler/backend/mips/proofs                            43s   3GB
Mar 14 23:52:27 Starting compiler/backend/riscv/proofs
Mar 14 23:53:18 Finished compiler/backend/riscv/proofs                           50s   3GB
Mar 14 23:53:19 Starting compiler/backend/ag32/proofs
Mar 15 00:07:01 Finished compiler/backend/ag32/proofs                         13m39s   6GB
Mar 15 00:07:02 Starting candle/set-theory
Mar 15 00:07:44 Finished candle/set-theory                                       41s   1GB
Mar 15 00:07:45 Starting candle/syntax-lib
Mar 15 00:07:47 Finished candle/syntax-lib                                        0s  73MB
Mar 15 00:07:47 Starting candle/standard/syntax
Mar 15 00:08:04 Finished candle/standard/syntax                                  15s   1GB
Mar 15 00:08:05 Starting candle/standard/semantics
Mar 15 00:10:31 Finished candle/standard/semantics                             2m24s   3GB
Mar 15 00:10:32 Starting candle/standard/monadic
Mar 15 00:10:34 Finished candle/standard/monadic                                  0s  96MB
Mar 15 00:10:34 Starting candle/standard/ml_kernel
Mar 15 00:12:26 Finished candle/standard/ml_kernel                             1m50s   6GB
Mar 15 00:12:27 Starting candle/overloading/syntax
Mar 15 00:15:47 Finished candle/overloading/syntax                             3m19s   1GB
Mar 15 00:15:48 Starting candle/overloading/semantics
Mar 15 00:27:02 Finished candle/overloading/semantics                         11m13s   5GB
Mar 15 00:27:03 Starting candle/overloading/monadic
Mar 15 00:29:44 Finished candle/overloading/monadic                            2m39s   3GB
Mar 15 00:29:45 Starting candle/overloading/ml_kernel
Mar 15 00:37:16 Finished candle/overloading/ml_kernel                          7m30s   6GB
Mar 15 00:37:17 Starting candle/overloading/ml_checker
Mar 15 00:39:49 Finished candle/overloading/ml_checker                         2m30s   7GB
Mar 15 00:39:50 Starting candle/prover
Mar 15 00:49:38 Finished candle/prover                                         9m47s   5GB
Mar 15 00:49:39 Starting pancake
Mar 15 00:50:41 Finished pancake                                               1m00s   1GB
Mar 15 00:50:42 Starting pancake/ffi
Mar 15 00:50:43 Finished pancake/ffi                                              0s  19MB
Mar 15 00:50:44 Starting pancake/semantics
Mar 15 00:53:21 Finished pancake/semantics                                     2m36s   2GB
Mar 15 00:53:22 Starting pancake/parser
Mar 15 00:53:49 Finished pancake/parser                                          25s   2GB
Mar 15 00:53:49 Starting pancake/proofs
Mar 15 01:24:33 Finished pancake/proofs                                       30m42s   9GB
Mar 15 01:24:34 Starting characteristic/examples
Mar 15 01:26:10 Finished characteristic/examples                               1m35s   6GB
Mar 15 01:26:11 Starting tutorial/solutions
Mar 15 01:41:45 Finished tutorial/solutions                                   15m32s  14GB
Mar 15 01:41:46 Starting translator/monadic/examples
Mar 15 01:45:30 Finished translator/monadic/examples                           3m42s   5GB
Mar 15 01:45:30 Starting examples
Mar 15 01:59:56 Finished examples                                             14m24s   7GB
Mar 15 01:59:57 Starting examples/compilation/x64
Mar 15 03:57:52 Finished examples/compilation/x64                           1h57m53s  29GB
Mar 15 03:57:53 Starting examples/compilation/x64/proofs
Mar 15 04:01:38 Finished examples/compilation/x64/proofs                       3m44s   6GB
Mar 15 04:01:39 Starting examples/compilation/ag32
Mar 15 04:31:53 Finished examples/compilation/ag32                            30m12s  13GB
Mar 15 04:31:54 Starting examples/compilation/ag32/proofs
Mar 15 04:33:23 Finished examples/compilation/ag32/proofs                      1m28s   7GB
Mar 15 04:33:24 Starting examples/compilation/to_word
Mar 15 04:37:22 Finished examples/compilation/to_word                          3m57s  11GB
Mar 15 04:37:23 Starting examples/lpr_checker
Mar 15 04:38:37 Finished examples/lpr_checker                                  1m13s   2GB
Mar 15 04:38:38 Starting examples/lpr_checker/array
Mar 15 05:09:44 Finished examples/lpr_checker/array                           31m04s  10GB
Mar 15 05:09:45 Starting examples/lpr_checker/array/compilation
Mar 15 05:52:07 Finished examples/lpr_checker/array/compilation               42m21s  72GB
Mar 15 05:52:08 Starting examples/lpr_checker/array/compilation/proofs
Mar 15 05:53:49 Finished examples/lpr_checker/array/compilation/proofs         1m40s   8GB
Mar 15 05:53:50 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 15 06:05:13 Finished examples/lpr_checker/array/compilation/proofsARM8    11m22s  36GB
Mar 15 06:05:14 Starting examples/xlrup_checker
Mar 15 06:06:23 Finished examples/xlrup_checker                                1m08s   1GB
Mar 15 06:06:24 Starting examples/xlrup_checker/array
Mar 15 06:22:39 Finished examples/xlrup_checker/array                         16m13s   8GB
Mar 15 06:22:39 Starting examples/xlrup_checker/array/compilation
Mar 15 06:44:54 Finished examples/xlrup_checker/array/compilation             22m13s  39GB
Mar 15 06:44:55 Starting examples/xlrup_checker/array/compilation/proofs
Mar 15 06:46:22 Finished examples/xlrup_checker/array/compilation/proofs       1m26s   6GB
Mar 15 06:46:23 Starting examples/pseudo_bool
Mar 15 06:48:27 Finished examples/pseudo_bool                                  2m02s   2GB
Mar 15 06:48:27 Starting examples/pseudo_bool/cnf_encoding
Mar 15 06:49:05 Finished examples/pseudo_bool/cnf_encoding                       36s   1GB
Mar 15 06:49:06 Starting examples/pseudo_bool/graph_encoding
Mar 15 06:49:55 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Mar 15 06:49:56 Starting examples/pseudo_bool/array
Mar 15 07:53:16 Finished examples/pseudo_bool/array                         1h03m18s  18GB
Mar 15 07:53:17 Starting examples/pseudo_bool/array/compilation
Mar 15 15:13:02 Finished examples/pseudo_bool/array/compilation             7h19m43s 124GB
Mar 15 15:13:02 Starting examples/pseudo_bool/array/compilation/proofs
Mar 15 15:16:18 Finished examples/pseudo_bool/array/compilation/proofs         3m14s   8GB
Mar 15 15:16:19 Starting examples/opentheory
Mar 15 15:26:57 Finished examples/opentheory                                  10m37s   7GB
Mar 15 15:26:58 Starting examples/opentheory
Mar 15 15:27:00 Finished examples/opentheory                                      0s 123MB
Mar 15 15:27:00 Starting examples/opentheory/compilation
Mar 15 16:03:08 Finished examples/opentheory/compilation                      36m06s  51GB
Mar 15 16:03:09 Starting examples/opentheory/compilation/proofs
Mar 15 16:04:37 Finished examples/opentheory/compilation/proofs                1m26s   6GB
Mar 15 16:04:38 Starting examples/opentheory/compilation/ag32
Mar 15 16:37:40 Finished examples/opentheory/compilation/ag32                 33m00s  59GB
Mar 15 16:37:41 Starting examples/opentheory/compilation/ag32/proofs
Mar 15 16:40:14 Finished examples/opentheory/compilation/ag32/proofs           2m32s   9GB
Mar 15 16:40:15 Starting examples/sat_encodings
Mar 15 16:42:51 Finished examples/sat_encodings                                2m35s   1GB
Mar 15 16:42:52 Starting examples/sat_encodings/case_studies
Mar 15 16:44:52 Finished examples/sat_encodings/case_studies                   1m59s   2GB
Mar 15 16:44:54 Starting examples/sat_encodings/translation
Mar 15 16:50:51 Finished examples/sat_encodings/translation                    5m56s   7GB
Mar 15 16:50:52 Starting examples/sat_encodings/translation/compilation
Mar 15 17:25:57 Finished examples/sat_encodings/translation/compilation       35m04s  42GB
Mar 15 17:25:58 Starting examples/deflate
Mar 15 17:27:14 Finished examples/deflate                                      1m14s   1GB
Mar 15 17:27:15 Starting examples/deflate/translation
Mar 15 17:28:52 Finished examples/deflate/translation                          1m36s   7GB
Mar 15 17:28:53 Starting examples/deflate/translation/compilation
Mar 15 17:46:01 Finished examples/deflate/translation/compilation             17m06s  33GB
Mar 15 17:46:02 Starting examples/vipr
Mar 15 17:50:14 Finished examples/vipr                                         4m11s   7GB
Mar 15 17:50:15 Starting examples/vipr/compilation
Mar 15 18:10:06 Finished examples/vipr/compilation                            19m49s  21GB
Mar 15 18:10:07 Starting translator/okasaki-examples
Mar 15 18:15:07 Finished translator/okasaki-examples                           4m59s   4GB
Mar 15 18:15:08 Starting translator/other-examples
Mar 15 18:19:50 Finished translator/other-examples                             4m41s   3GB
Mar 15 18:19:51 Starting compiler/parsing/tests
Mar 15 18:20:25 Finished compiler/parsing/tests                                  32s   1GB
Mar 15 18:20:25 Starting compiler/inference/tests
Mar 15 18:27:50 Finished compiler/inference/tests                              7m23s   6GB
Mar 15 18:27:51 Starting compiler/printing/test
Mar 15 18:31:20 Finished compiler/printing/test                                3m28s   6GB
Mar 15 18:31:21 Starting icing/flover
Mar 15 19:06:43 Finished icing/flover                                         35m21s   4GB
Mar 15 19:06:44 Starting icing/
Mar 15 20:01:48 Finished icing/                                               55m03s  22GB
Mar 15 20:01:49 Starting icing/examples
Mar 15 20:03:30 Finished icing/examples                                        1m40s   8GB
Mar 15 20:03:31 Starting compiler/repl
Mar 15 20:12:12 Finished compiler/repl                                         8m39s   9GB
Mar 15 20:12:12 Starting unverified/sexpr-bootstrap/x64/64
Mar 15 20:23:15 Finished unverified/sexpr-bootstrap/x64/64                    11m01s  14GB
Mar 15 20:23:15 Starting unverified/sexpr-bootstrap/x64/32
Mar 15 20:32:14 Finished unverified/sexpr-bootstrap/x64/32                     8m57s  14GB
Mar 15 20:32:15 Starting compiler/benchmarks
Mar 15 20:33:00 Finished compiler/benchmarks                                     43s 713MB
Mar 15 20:33:01 Starting compiler/bootstrap/compilation/x64/64
Mar 16 12:13:38 Finished compiler/bootstrap/compilation/x64/64             15h40m36s 179GB
Mar 16 12:13:39 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 16 12:34:29 Finished compiler/bootstrap/compilation/x64/64/proofs         20m48s  44GB
Mar 16 12:34:30 Starting compiler/bootstrap/compilation/x64/32
Mar 16 20:01:49 Finished compiler/bootstrap/compilation/x64/32              7h27m18s 124GB
Mar 16 20:01:50 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 16 20:05:26 Finished compiler/bootstrap/compilation/x64/32/proofs          3m35s  18GB
Mar 16 20:05:27 Starting compiler/bootstrap/compilation/ag32/32
Mar 17 03:53:25 Finished compiler/bootstrap/compilation/ag32/32             7h47m57s 154GB
Mar 17 03:53:26 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 17 04:01:30 Finished compiler/bootstrap/compilation/ag32/32/proofs         8m02s  52GB
Mar 17 04:01:31 SUCCESS