Job 2567

CakeML:ead9b9cda9adb2101af30515a1eb21e635c23a19
  Use smaller heap [Aug 22 07:50:50]
#1043 (heaps)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:5fc7a6047d48839800489adfb2c2eac7f3ffd5fc
  Add missing export [Aug 21 10:25:23]
Machine:pavlova

Aug 22 08:57:06 Claimed job
Aug 22 08:57:10 Reusing HOL
Aug 22 08:57:21 Starting developers
Aug 22 08:57:25 Finished developers                                               2s 191MB
Aug 22 08:57:26 Starting developers/bin
Aug 22 08:57:36 Finished developers/bin                                           9s   1GB
Aug 22 08:57:37 Starting compiler/proofs
Aug 22 08:59:48 Resuming compiler/proofs
Aug 22 10:41:52 Finished compiler/proofs                                    1h42m03s  45GB
Aug 22 10:41:53 Starting compiler/bootstrap/translation
Aug 22 19:29:20 Finished compiler/bootstrap/translation                     8h47m25s  75GB
Aug 22 19:29:21 Starting semantics/ffi
Aug 22 19:29:30 Finished semantics/ffi                                            7s 832MB
Aug 22 19:29:30 Starting semantics
Aug 22 19:29:32 Finished semantics                                                0s  64MB
Aug 22 19:29:33 Starting semantics/proofs
Aug 22 19:29:55 Finished semantics/proofs                                        21s 792MB
Aug 22 19:29:56 Starting semantics/alt_semantics
Aug 22 19:30:22 Finished semantics/alt_semantics                                 25s 916MB
Aug 22 19:30:23 Starting semantics/alt_semantics/proofs
Aug 22 19:40:39 Finished semantics/alt_semantics/proofs                       10m15s   2GB
Aug 22 19:40:40 Starting basis/pure
Aug 22 19:40:41 Finished basis/pure                                               0s  71MB
Aug 22 19:40:42 Starting translator
Aug 22 19:42:18 Finished translator                                            1m34s   4GB
Aug 22 19:42:19 Starting compiler/parsing
Aug 22 19:42:20 Finished compiler/parsing                                         0s  73MB
Aug 22 19:42:21 Starting characteristic
Aug 22 19:42:23 Finished characteristic                                           0s  90MB
Aug 22 19:42:24 Starting translator/monadic
Aug 22 19:42:25 Finished translator/monadic                                       0s  94MB
Aug 22 19:42:26 Starting basis
Aug 22 19:45:41 Finished basis                                                 3m13s   4GB
Aug 22 19:45:43 Starting compiler/inference
Aug 22 19:45:44 Finished compiler/inference                                       0s  99MB
Aug 22 19:45:45 Starting compiler/backend/reg_alloc
Aug 22 19:45:46 Finished compiler/backend/reg_alloc                               0s  68MB
Aug 22 19:45:47 Starting compiler/backend/gc
Aug 22 19:45:49 Finished compiler/backend/gc                                      0s 141MB
Aug 22 19:45:50 Starting compiler/backend
Aug 22 19:45:55 Finished compiler/backend                                         3s 334MB
Aug 22 19:45:56 Starting compiler/encoders/asm
Aug 22 19:45:57 Finished compiler/encoders/asm                                    0s  91MB
Aug 22 19:45:58 Starting compiler/encoders/x64
Aug 22 19:45:59 Finished compiler/encoders/x64                                    0s 104MB
Aug 22 19:46:00 Starting compiler/encoders/arm7
Aug 22 19:46:02 Finished compiler/encoders/arm7                                   0s 103MB
Aug 22 19:46:03 Starting compiler/encoders/arm8
Aug 22 19:46:04 Finished compiler/encoders/arm8                                   0s 100MB
Aug 22 19:46:05 Starting compiler/encoders/arm8_asl
Aug 22 21:59:03 Finished compiler/encoders/arm8_asl                         2h12m56s  39GB
Aug 22 21:59:04 Starting compiler/encoders/mips
Aug 22 21:59:05 Finished compiler/encoders/mips                                   0s  95MB
Aug 22 21:59:06 Starting compiler/encoders/riscv
Aug 22 21:59:08 Finished compiler/encoders/riscv                                  0s 100MB
Aug 22 21:59:09 Starting compiler/encoders/ag32
Aug 22 21:59:10 Finished compiler/encoders/ag32                                   0s  92MB
Aug 22 21:59:11 Starting compiler/backend/x64
Aug 22 21:59:13 Finished compiler/backend/x64                                     0s 133MB
Aug 22 21:59:14 Starting compiler/backend/arm7
Aug 22 21:59:15 Finished compiler/backend/arm7                                    0s 137MB
Aug 22 21:59:16 Starting compiler/backend/arm8
Aug 22 21:59:18 Finished compiler/backend/arm8                                    0s 130MB
Aug 22 21:59:19 Starting compiler/backend/mips
Aug 22 21:59:21 Finished compiler/backend/mips                                    0s 130MB
Aug 22 21:59:22 Starting compiler/backend/riscv
Aug 22 21:59:23 Finished compiler/backend/riscv                                   0s 130MB
Aug 22 21:59:24 Starting compiler/backend/ag32
Aug 22 22:00:46 Finished compiler/backend/ag32                                 1m20s   3GB
Aug 22 22:00:47 Starting compiler/parsing/proofs
Aug 22 22:00:49 Finished compiler/parsing/proofs                                  0s  75MB
Aug 22 22:00:49 Starting compiler/inference/proofs
Aug 22 22:00:51 Finished compiler/inference/proofs                                0s  93MB
Aug 22 22:00:52 Starting compiler/backend/semantics
Aug 22 22:03:59 Finished compiler/backend/semantics                            3m06s   3GB
Aug 22 22:04:00 Starting compiler/backend/reg_alloc/proofs
Aug 22 22:04:02 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Aug 22 22:04:03 Starting compiler/backend/proofs
Aug 22 22:04:55 Finished compiler/backend/proofs                                 51s   2GB
Aug 22 22:04:55 Starting compiler/backend/serialiser
Aug 22 22:04:57 Finished compiler/backend/serialiser                              0s 143MB
Aug 22 22:04:58 Starting compiler/encoders/x64/proofs
Aug 22 22:14:23 Finished compiler/encoders/x64/proofs                          9m23s   7GB
Aug 22 22:14:24 Starting compiler/encoders/arm7/proofs
Aug 22 22:27:19 Finished compiler/encoders/arm7/proofs                        12m54s  12GB
Aug 22 22:27:20 Starting compiler/encoders/arm8/proofs
Aug 22 22:34:07 Finished compiler/encoders/arm8/proofs                         6m46s   4GB
Aug 22 22:34:08 Starting compiler/encoders/arm8_asl/proofs
Aug 22 23:23:13 Finished compiler/encoders/arm8_asl/proofs                    49m03s  13GB
Aug 22 23:23:13 Starting compiler/encoders/mips/proofs
Aug 22 23:33:15 Finished compiler/encoders/mips/proofs                        10m00s   7GB
Aug 22 23:33:15 Starting compiler/encoders/riscv/proofs
Aug 22 23:41:32 Finished compiler/encoders/riscv/proofs                        8m15s   4GB
Aug 22 23:41:33 Starting compiler/encoders/ag32/proofs
Aug 22 23:43:57 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 22 23:43:58 Starting compiler/backend/x64/proofs
Aug 22 23:44:40 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 22 23:44:41 Starting compiler/backend/arm7/proofs
Aug 22 23:45:27 Finished compiler/backend/arm7/proofs                            44s   3GB
Aug 22 23:45:28 Starting compiler/backend/arm8/proofs
Aug 22 23:46:10 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 22 23:46:11 Starting compiler/backend/arm8_asl
Aug 22 23:46:42 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 22 23:46:43 Starting compiler/backend/mips/proofs
Aug 22 23:47:30 Finished compiler/backend/mips/proofs                            46s   3GB
Aug 22 23:47:31 Starting compiler/backend/riscv/proofs
Aug 22 23:48:24 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 22 23:48:25 Starting compiler/backend/ag32/proofs
Aug 23 00:02:30 Finished compiler/backend/ag32/proofs                         14m04s   6GB
Aug 23 00:02:31 Starting compiler/backend/cv_compute
Aug 23 00:04:17 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 23 00:04:18 Starting cv_translator
Aug 23 00:23:25 Finished cv_translator                                        19m06s  12GB
Aug 23 00:23:26 Starting candle/set-theory
Aug 23 00:24:15 Finished candle/set-theory                                       47s   1GB
Aug 23 00:24:16 Starting candle/syntax-lib
Aug 23 00:24:17 Finished candle/syntax-lib                                        0s  74MB
Aug 23 00:24:18 Starting candle/standard/syntax
Aug 23 00:24:37 Finished candle/standard/syntax                                  18s   1GB
Aug 23 00:24:38 Starting candle/standard/semantics
Aug 23 00:27:16 Finished candle/standard/semantics                             2m37s   3GB
Aug 23 00:27:17 Starting candle/standard/monadic
Aug 23 00:27:18 Finished candle/standard/monadic                                  0s  99MB
Aug 23 00:27:19 Starting candle/standard/ml_kernel
Aug 23 00:29:19 Finished candle/standard/ml_kernel                             1m58s   5GB
Aug 23 00:29:20 Starting candle/overloading/syntax
Aug 23 00:32:57 Finished candle/overloading/syntax                             3m36s   2GB
Aug 23 00:32:58 Starting candle/overloading/semantics
Aug 23 00:44:28 Finished candle/overloading/semantics                         11m29s   8GB
Aug 23 00:44:29 Starting candle/overloading/monadic
Aug 23 00:47:07 Finished candle/overloading/monadic                            2m37s   3GB
Aug 23 00:47:08 Starting candle/overloading/ml_kernel
Aug 23 00:54:54 Finished candle/overloading/ml_kernel                          7m45s   6GB
Aug 23 00:54:55 Starting candle/overloading/ml_checker
Aug 23 00:57:31 Finished candle/overloading/ml_checker                         2m35s   6GB
Aug 23 00:57:32 Starting candle/prover
Aug 23 01:07:44 Finished candle/prover                                        10m11s   5GB
Aug 23 01:07:45 Starting pancake
Aug 23 01:08:11 Finished pancake                                                 24s 968MB
Aug 23 01:08:12 Starting pancake/ffi
Aug 23 01:08:12 Finished pancake/ffi                                              0s  23MB
Aug 23 01:08:13 Starting pancake/semantics
Aug 23 01:10:18 Finished pancake/semantics                                     2m03s   1GB
Aug 23 01:10:19 Starting pancake/parser
Aug 23 01:10:40 Finished pancake/parser                                          19s 802MB
Aug 23 01:10:40 Starting pancake/proofs
Aug 23 01:25:44 Finished pancake/proofs                                       15m02s   7GB
Aug 23 01:25:45 Starting characteristic/examples
Aug 23 01:27:12 Finished characteristic/examples                               1m25s   5GB
Aug 23 01:27:12 Starting tutorial/solutions
Aug 23 01:29:59 Finished tutorial/solutions                                    2m45s   5GB
Aug 23 01:30:00 Starting translator/monadic/examples
Aug 23 01:33:07 Finished translator/monadic/examples                           3m06s   4GB
Aug 23 01:33:08 Starting examples
Aug 23 01:45:35 Finished examples                                             12m25s   5GB
Aug 23 01:45:36 Starting examples/compilation/x64
Aug 23 01:55:05 Finished examples/compilation/x64                              9m28s   8GB
Aug 23 01:55:06 Starting examples/compilation/x64/proofs
Aug 23 01:59:45 Finished examples/compilation/x64/proofs                       4m38s   8GB
Aug 23 01:59:46 Starting examples/compilation/ag32
Aug 23 02:02:34 Finished examples/compilation/ag32                             2m46s   5GB
Aug 23 02:02:35 Starting examples/compilation/ag32/proofs
Aug 23 02:04:23 Finished examples/compilation/ag32/proofs                      1m47s   9GB
Aug 23 02:04:24 Starting examples/compilation/to_word
Aug 23 02:08:26 Finished examples/compilation/to_word                          4m01s  11GB
Aug 23 02:08:27 Starting examples/lpr_checker
Aug 23 02:09:04 Finished examples/lpr_checker                                    35s   1GB
Aug 23 02:09:05 Starting examples/lpr_checker/array
Aug 23 02:35:08 Finished examples/lpr_checker/array                           26m02s  23GB
Aug 23 02:35:09 Starting examples/lpr_checker/array/compilation
Aug 23 02:37:42 Finished examples/lpr_checker/array/compilation                2m32s   9GB
Aug 23 02:37:43 Starting examples/lpr_checker/array/compilation/proofs
Aug 23 02:39:36 Finished examples/lpr_checker/array/compilation/proofs         1m51s   9GB
Aug 23 02:39:37 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 23 02:41:26 Finished examples/lpr_checker/array/compilation/proofsARM8     1m48s   9GB
Aug 23 02:41:26 Starting examples/xlrup_checker
Aug 23 02:42:00 Finished examples/xlrup_checker                                  33s   1GB
Aug 23 02:42:01 Starting examples/xlrup_checker/array
Aug 23 02:55:15 Finished examples/xlrup_checker/array                         13m12s  10GB
Aug 23 02:55:16 Starting examples/xlrup_checker/array/compilation
Aug 23 02:56:43 Finished examples/xlrup_checker/array/compilation              1m26s   7GB
Aug 23 02:56:44 Starting examples/xlrup_checker/array/compilation/proofs
Aug 23 02:58:29 Finished examples/xlrup_checker/array/compilation/proofs       1m44s   8GB
Aug 23 02:58:30 Starting examples/pseudo_bool
Aug 23 02:59:55 Finished examples/pseudo_bool                                  1m24s   1GB
Aug 23 02:59:56 Starting examples/pseudo_bool/cnf_encoding
Aug 23 03:00:37 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Aug 23 03:00:38 Starting examples/pseudo_bool/graph_encoding
Aug 23 03:01:30 Finished examples/pseudo_bool/graph_encoding                     51s   1GB
Aug 23 03:01:31 Starting examples/pseudo_bool/array
Aug 23 04:03:38 Finished examples/pseudo_bool/array                         1h02m05s  40GB
Aug 23 04:03:39 Starting examples/pseudo_bool/array/compilation
Aug 23 04:16:56 Finished examples/pseudo_bool/array/compilation               13m16s  28GB
Aug 23 04:16:57 Starting examples/pseudo_bool/array/compilation/proofs
Aug 23 04:20:53 Finished examples/pseudo_bool/array/compilation/proofs         3m55s  10GB
Aug 23 04:20:54 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 23 04:22:42 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m47s  10GB
Aug 23 04:22:43 Starting examples/opentheory
Aug 23 04:31:21 Finished examples/opentheory                                   8m37s   7GB
Aug 23 04:31:22 Starting examples/opentheory
Aug 23 04:31:24 Finished examples/opentheory                                      0s 131MB
Aug 23 04:31:24 Starting examples/opentheory/compilation
Aug 23 04:33:27 Finished examples/opentheory/compilation                       2m02s   9GB
Aug 23 04:33:28 Starting examples/opentheory/compilation/proofs
Aug 23 04:35:12 Finished examples/opentheory/compilation/proofs                1m42s   7GB
Aug 23 04:35:13 Starting examples/opentheory/compilation/ag32
Aug 23 04:37:20 Finished examples/opentheory/compilation/ag32                  2m07s   9GB
Aug 23 04:37:21 Starting examples/opentheory/compilation/ag32/proofs
Aug 23 04:39:44 Finished examples/opentheory/compilation/ag32/proofs           2m22s  12GB
Aug 23 04:39:45 Starting examples/sat_encodings
Aug 23 04:40:45 Finished examples/sat_encodings                                  58s 910MB
Aug 23 04:40:45 Starting examples/sat_encodings/case_studies
Aug 23 04:42:53 Finished examples/sat_encodings/case_studies                   2m07s   2GB
Aug 23 04:42:54 Starting examples/sat_encodings/translation
Aug 23 04:46:34 Finished examples/sat_encodings/translation                    3m38s   3GB
Aug 23 04:46:35 Starting examples/sat_encodings/translation/compilation
Aug 23 04:49:06 Finished examples/sat_encodings/translation/compilation        2m29s   7GB
Aug 23 04:49:06 Starting examples/deflate
Aug 23 04:49:33 Finished examples/deflate                                        25s 760MB
Aug 23 04:49:34 Starting examples/deflate/translation
Aug 23 04:50:31 Finished examples/deflate/translation                            56s   2GB
Aug 23 04:50:32 Starting examples/deflate/translation/compilation
Aug 23 04:51:39 Finished examples/deflate/translation/compilation              1m06s   5GB
Aug 23 04:51:40 Starting examples/vipr
Aug 23 04:55:05 Finished examples/vipr                                         3m24s   4GB
Aug 23 04:55:06 Starting examples/vipr/compilation
Aug 23 04:56:24 Finished examples/vipr/compilation                             1m16s   6GB
Aug 23 04:56:25 Starting translator/okasaki-examples
Aug 23 05:00:46 Finished translator/okasaki-examples                           4m19s   4GB
Aug 23 05:00:47 Starting translator/other-examples
Aug 23 05:05:59 Finished translator/other-examples                             5m11s   3GB
Aug 23 05:06:00 Starting compiler/parsing/tests
Aug 23 05:06:40 Finished compiler/parsing/tests                                  39s   2GB
Aug 23 05:06:41 Starting compiler/inference/tests
Aug 23 05:07:24 Finished compiler/inference/tests                                42s   3GB
Aug 23 05:07:25 Starting compiler/printing/test
Aug 23 05:09:01 Finished compiler/printing/test                                1m34s   6GB
Aug 23 05:09:02 Starting icing/flover
Aug 23 05:45:56 Finished icing/flover                                         36m53s   4GB
Aug 23 05:45:57 Starting icing/
Aug 23 06:13:42 Finished icing/                                               27m44s  10GB
Aug 23 06:13:43 Starting icing/examples
Aug 23 06:15:29 Finished icing/examples                                        1m44s   9GB
Aug 23 06:15:30 Starting compiler/repl
Aug 23 06:24:25 Finished compiler/repl                                         8m53s   9GB
Aug 23 06:24:26 Starting unverified/sexpr-bootstrap/x64/64
Aug 23 06:37:29 Finished unverified/sexpr-bootstrap/x64/64                    13m02s  18GB
Aug 23 06:37:30 Starting unverified/sexpr-bootstrap/x64/32
Aug 23 06:47:49 Finished unverified/sexpr-bootstrap/x64/32                    10m18s  15GB
Aug 23 06:47:50 Starting compiler/benchmarks
Aug 23 06:48:35 Finished compiler/benchmarks                                     43s 713MB
Aug 23 06:48:36 Starting compiler/bootstrap/compilation/x64/64
Aug 23 07:30:43 Finished compiler/bootstrap/compilation/x64/64                42m06s 120GB
Aug 23 07:30:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 23 07:54:49 Finished compiler/bootstrap/compilation/x64/64/proofs         24m03s  51GB
Aug 23 07:54:50 Starting compiler/bootstrap/compilation/x64/32
Aug 23 08:34:31 Finished compiler/bootstrap/compilation/x64/32                39m40s 112GB
Aug 23 08:34:32 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 23 08:39:07 Finished compiler/bootstrap/compilation/x64/32/proofs          4m33s  24GB
Aug 23 08:39:07 Starting compiler/bootstrap/compilation/arm8/64
Aug 23 09:34:50 Finished compiler/bootstrap/compilation/arm8/64               55m40s 124GB
Aug 23 09:34:51 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 23 09:40:39 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m47s  33GB
Aug 23 09:40:40 Starting compiler/bootstrap/compilation/ag32/32
Aug 23 10:19:15 Finished compiler/bootstrap/compilation/ag32/32               38m34s  96GB
Aug 23 10:19:16 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 23 10:25:03 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m45s  28GB
Aug 23 10:25:04 SUCCESS