Job 2746

CakeML:c037f2878eb90a58be223829cd317683fd6e2c22
  Try removing parsingComputeLib for issue #575 [Dec 09 12:50:57]
#1111 (parsingCompute)
Merging into:bad29406cfc21b9ac36dda1a3925e67f2f78b901
  Merge pull request #1110 from CakeML/efficient-cases-peg [Dec 11 05:48:32]
HOL:81404220103cb7dac8d837073e53e07f92dca26a
  Merge pull request #1358 from HOL-Theorem-Prover/sha2 [Dec 10 12:18:19]
Machine:pavlova

Dec 11 12:01:06 Claimed job
Dec 11 12:01:14 Building HOL
Dec 11 12:12:16 Starting developers
Dec 11 12:12:20 Finished developers                                               3s 207MB
Dec 11 12:12:21 Starting developers/bin
Dec 11 12:12:28 Finished developers/bin                                           5s 746MB
Dec 11 12:12:29 Starting compiler/proofs
Dec 11 13:54:52 Finished compiler/proofs                                    1h42m22s  42GB
Dec 11 13:54:53 Starting compiler/bootstrap/translation
Dec 11 19:46:18 Finished compiler/bootstrap/translation                     5h51m24s  66GB
Dec 11 19:46:19 Starting semantics/ffi
Dec 11 19:46:29 Finished semantics/ffi                                            9s 601MB
Dec 11 19:46:30 Starting semantics
Dec 11 19:46:32 Finished semantics                                                0s  53MB
Dec 11 19:46:33 Starting semantics/proofs
Dec 11 19:46:56 Finished semantics/proofs                                        22s 838MB
Dec 11 19:46:57 Starting semantics/alt_semantics
Dec 11 19:47:18 Finished semantics/alt_semantics                                 20s 894MB
Dec 11 19:47:19 Starting semantics/alt_semantics/proofs
Dec 11 19:57:39 Finished semantics/alt_semantics/proofs                       10m18s   2GB
Dec 11 19:57:40 Starting basis/pure
Dec 11 19:57:41 Finished basis/pure                                               0s  65MB
Dec 11 19:57:42 Starting translator
Dec 11 19:59:16 Finished translator                                            1m32s   3GB
Dec 11 19:59:17 Starting compiler/parsing
Dec 11 19:59:18 Finished compiler/parsing                                         0s  57MB
Dec 11 19:59:19 Starting characteristic
Dec 11 19:59:21 Finished characteristic                                           0s  88MB
Dec 11 19:59:22 Starting translator/monadic
Dec 11 19:59:23 Finished translator/monadic                                       0s  90MB
Dec 11 19:59:24 Starting basis
Dec 11 20:01:50 Finished basis                                                 2m24s   4GB
Dec 11 20:01:51 Starting compiler/inference
Dec 11 20:01:53 Finished compiler/inference                                       0s  84MB
Dec 11 20:01:54 Starting compiler/backend/reg_alloc
Dec 11 20:01:55 Finished compiler/backend/reg_alloc                               0s  52MB
Dec 11 20:01:56 Starting compiler/backend/gc
Dec 11 20:01:58 Finished compiler/backend/gc                                      1s 123MB
Dec 11 20:01:59 Starting compiler/backend
Dec 11 20:02:04 Finished compiler/backend                                         4s 241MB
Dec 11 20:02:05 Starting compiler/encoders/asm
Dec 11 20:02:06 Finished compiler/encoders/asm                                    0s  82MB
Dec 11 20:02:07 Starting compiler/encoders/x64
Dec 11 20:02:09 Finished compiler/encoders/x64                                    0s  91MB
Dec 11 20:02:10 Starting compiler/encoders/arm7
Dec 11 20:02:12 Finished compiler/encoders/arm7                                   0s  86MB
Dec 11 20:02:13 Starting compiler/encoders/arm8
Dec 11 20:02:14 Finished compiler/encoders/arm8                                   0s  84MB
Dec 11 20:02:15 Starting compiler/encoders/arm8_asl
Dec 11 22:03:24 Finished compiler/encoders/arm8_asl                         2h01m07s  43GB
Dec 11 22:03:25 Starting compiler/encoders/mips
Dec 11 22:03:26 Finished compiler/encoders/mips                                   0s  86MB
Dec 11 22:03:27 Starting compiler/encoders/riscv
Dec 11 22:03:29 Finished compiler/encoders/riscv                                  0s  83MB
Dec 11 22:03:30 Starting compiler/encoders/ag32
Dec 11 22:03:32 Finished compiler/encoders/ag32                                   0s  80MB
Dec 11 22:03:32 Starting compiler/backend/x64
Dec 11 22:03:35 Finished compiler/backend/x64                                     1s 123MB
Dec 11 22:03:35 Starting compiler/backend/arm7
Dec 11 22:03:38 Finished compiler/backend/arm7                                    1s 123MB
Dec 11 22:03:38 Starting compiler/backend/arm8
Dec 11 22:03:40 Finished compiler/backend/arm8                                    1s 123MB
Dec 11 22:03:41 Starting compiler/backend/mips
Dec 11 22:03:43 Finished compiler/backend/mips                                    1s 123MB
Dec 11 22:03:44 Starting compiler/backend/riscv
Dec 11 22:03:46 Finished compiler/backend/riscv                                   1s 123MB
Dec 11 22:03:47 Starting compiler/backend/ag32
Dec 11 22:04:55 Finished compiler/backend/ag32                                 1m06s   2GB
Dec 11 22:04:56 Starting compiler/parsing/proofs
Dec 11 22:04:57 Finished compiler/parsing/proofs                                  0s  65MB
Dec 11 22:04:58 Starting compiler/inference/proofs
Dec 11 22:05:00 Finished compiler/inference/proofs                                0s  86MB
Dec 11 22:05:01 Starting compiler/backend/semantics
Dec 11 22:08:10 Finished compiler/backend/semantics                            3m08s   2GB
Dec 11 22:08:11 Starting compiler/backend/reg_alloc/proofs
Dec 11 22:08:13 Finished compiler/backend/reg_alloc/proofs                        0s  82MB
Dec 11 22:08:14 Starting compiler/backend/proofs
Dec 11 22:09:04 Finished compiler/backend/proofs                                 48s   2GB
Dec 11 22:09:05 Starting compiler/backend/serialiser
Dec 11 22:09:07 Finished compiler/backend/serialiser                              1s 140MB
Dec 11 22:09:08 Starting compiler/encoders/x64/proofs
Dec 11 22:19:15 Finished compiler/encoders/x64/proofs                         10m05s   4GB
Dec 11 22:19:16 Starting compiler/encoders/arm7/proofs
Dec 11 22:32:19 Finished compiler/encoders/arm7/proofs                        13m02s   7GB
Dec 11 22:32:20 Starting compiler/encoders/arm8/proofs
Dec 11 22:39:12 Finished compiler/encoders/arm8/proofs                         6m50s   3GB
Dec 11 22:39:13 Starting compiler/encoders/arm8_asl/proofs
Dec 11 23:29:02 Finished compiler/encoders/arm8_asl/proofs                    49m47s  20GB
Dec 11 23:29:02 Starting compiler/encoders/mips/proofs
Dec 11 23:39:19 Finished compiler/encoders/mips/proofs                        10m16s  10GB
Dec 11 23:39:20 Starting compiler/encoders/riscv/proofs
Dec 11 23:47:55 Finished compiler/encoders/riscv/proofs                        8m34s   3GB
Dec 11 23:47:56 Starting compiler/encoders/ag32/proofs
Dec 11 23:50:50 Finished compiler/encoders/ag32/proofs                         2m52s   2GB
Dec 11 23:50:51 Starting compiler/backend/x64/proofs
Dec 11 23:51:23 Finished compiler/backend/x64/proofs                             30s   2GB
Dec 11 23:51:23 Starting compiler/backend/arm7/proofs
Dec 11 23:51:57 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 11 23:51:58 Starting compiler/backend/arm8/proofs
Dec 11 23:52:29 Finished compiler/backend/arm8/proofs                            29s   2GB
Dec 11 23:52:30 Starting compiler/backend/arm8_asl
Dec 11 23:52:51 Finished compiler/backend/arm8_asl                               20s   2GB
Dec 11 23:52:52 Starting compiler/backend/mips/proofs
Dec 11 23:53:23 Finished compiler/backend/mips/proofs                            29s   2GB
Dec 11 23:53:23 Starting compiler/backend/riscv/proofs
Dec 11 23:53:57 Finished compiler/backend/riscv/proofs                           32s   2GB
Dec 11 23:53:58 Starting compiler/backend/ag32/proofs
Dec 12 00:07:44 Finished compiler/backend/ag32/proofs                         13m45s   5GB
Dec 12 00:07:45 Starting compiler/backend/cv_compute
Dec 12 00:08:53 Finished compiler/backend/cv_compute                           1m07s   2GB
Dec 12 00:08:54 Starting cv_translator
Dec 12 00:26:31 Finished cv_translator                                        17m36s   7GB
Dec 12 00:26:32 Starting candle/set-theory
Dec 12 00:27:08 Finished candle/set-theory                                       34s   1GB
Dec 12 00:27:09 Starting candle/syntax-lib
Dec 12 00:27:10 Finished candle/syntax-lib                                        0s  64MB
Dec 12 00:27:11 Starting candle/standard/syntax
Dec 12 00:27:23 Finished candle/standard/syntax                                  11s 773MB
Dec 12 00:27:24 Starting candle/standard/semantics
Dec 12 00:29:27 Finished candle/standard/semantics                             2m02s   2GB
Dec 12 00:29:28 Starting candle/standard/monadic
Dec 12 00:29:30 Finished candle/standard/monadic                                  0s  86MB
Dec 12 00:29:31 Starting candle/standard/ml_kernel
Dec 12 00:31:15 Finished candle/standard/ml_kernel                             1m43s   4GB
Dec 12 00:31:16 Starting candle/overloading/syntax
Dec 12 00:34:24 Finished candle/overloading/syntax                             3m06s   2GB
Dec 12 00:34:25 Starting candle/overloading/semantics
Dec 12 00:45:27 Finished candle/overloading/semantics                         11m01s   6GB
Dec 12 00:45:28 Starting candle/overloading/monadic
Dec 12 00:47:45 Finished candle/overloading/monadic                            2m15s   2GB
Dec 12 00:47:46 Starting candle/overloading/ml_kernel
Dec 12 00:55:01 Finished candle/overloading/ml_kernel                          7m14s   6GB
Dec 12 00:55:02 Starting candle/overloading/ml_checker
Dec 12 00:57:14 Finished candle/overloading/ml_checker                         2m10s   6GB
Dec 12 00:57:15 Starting candle/prover
Dec 12 01:06:53 Finished candle/prover                                         9m37s   5GB
Dec 12 01:06:54 Starting pancake
Dec 12 01:07:15 Finished pancake                                                 20s 708MB
Dec 12 01:07:16 Starting pancake/ffi
Dec 12 01:07:17 Finished pancake/ffi                                              0s  11MB
Dec 12 01:07:18 Starting pancake/semantics
Dec 12 01:09:26 Finished pancake/semantics                                     2m06s   2GB
Dec 12 01:09:27 Starting pancake/parser
Dec 12 01:09:50 Finished pancake/parser                                          22s 472MB
Dec 12 01:09:51 Starting pancake/proofs
Dec 12 01:25:54 Finished pancake/proofs                                       16m02s   6GB
Dec 12 01:25:55 Starting compiler/dafny
Dec 12 01:28:39 Finished compiler/dafny                                        2m42s  10GB
Dec 12 01:28:40 Starting compiler/dafny/translation
Dec 12 01:45:30 Finished compiler/dafny/translation                           16m49s  19GB
Dec 12 01:45:31 Starting compiler/dafny/compilation
Dec 12 01:47:57 Finished compiler/dafny/compilation                            2m24s   8GB
Dec 12 01:47:58 Starting compiler/dafny/semantics
Dec 12 01:48:33 Finished compiler/dafny/semantics                                34s   1GB
Dec 12 01:48:34 Starting characteristic/examples
Dec 12 01:50:00 Finished characteristic/examples                               1m25s   4GB
Dec 12 01:50:01 Starting tutorial/solutions
Dec 12 01:52:21 Finished tutorial/solutions                                    2m18s   3GB
Dec 12 01:52:22 Starting translator/monadic/examples
Dec 12 01:55:11 Finished translator/monadic/examples                           2m48s   4GB
Dec 12 01:55:12 Starting examples
Dec 12 02:01:18 Finished examples                                              6m04s   3GB
Dec 12 02:01:19 Starting examples/compilation/x64
Dec 12 02:07:57 Finished examples/compilation/x64                              6m36s   4GB
Dec 12 02:07:58 Starting examples/compilation/x64/proofs
Dec 12 02:10:17 Finished examples/compilation/x64/proofs                       2m18s   3GB
Dec 12 02:10:18 Starting examples/compilation/ag32
Dec 12 02:12:05 Finished examples/compilation/ag32                             1m46s   3GB
Dec 12 02:12:06 Starting examples/compilation/ag32/proofs
Dec 12 02:13:05 Finished examples/compilation/ag32/proofs                        58s   5GB
Dec 12 02:13:06 Starting examples/lpr_checker
Dec 12 02:13:36 Finished examples/lpr_checker                                    29s   1GB
Dec 12 02:13:37 Starting examples/lpr_checker/array
Dec 12 02:39:40 Finished examples/lpr_checker/array                           26m01s  25GB
Dec 12 02:39:40 Starting examples/lpr_checker/array/compilation
Dec 12 02:41:31 Finished examples/lpr_checker/array/compilation                1m49s   7GB
Dec 12 02:41:32 Starting examples/lpr_checker/array/compilation/proofs
Dec 12 02:42:45 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Dec 12 02:42:45 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 12 02:43:51 Finished examples/lpr_checker/array/compilation/proofsARM8     1m04s   6GB
Dec 12 02:43:52 Starting .
Dec 12 02:43:55 Finished .                                                        2s 282MB
Dec 12 02:43:56 Starting examples/xlrup_checker
Dec 12 02:44:31 Finished examples/xlrup_checker                                  33s   1GB
Dec 12 02:44:32 Starting examples/xlrup_checker/array
Dec 12 02:57:40 Finished examples/xlrup_checker/array                         13m07s   8GB
Dec 12 02:57:41 Starting examples/xlrup_checker/array/compilation
Dec 12 02:58:41 Finished examples/xlrup_checker/array/compilation                58s   4GB
Dec 12 02:58:42 Starting examples/xlrup_checker/array/compilation/proofs
Dec 12 02:59:40 Finished examples/xlrup_checker/array/compilation/proofs         57s   4GB
Dec 12 02:59:41 Starting examples/pseudo_bool
Dec 12 03:01:15 Finished examples/pseudo_bool                                  1m33s   2GB
Dec 12 03:01:16 Starting examples/pseudo_bool/cnf_encoding
Dec 12 03:01:46 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Dec 12 03:01:47 Starting examples/pseudo_bool/graph_encoding
Dec 12 03:02:31 Finished examples/pseudo_bool/graph_encoding                     43s   2GB
Dec 12 03:02:32 Starting examples/pseudo_bool/array
Dec 12 04:10:29 Finished examples/pseudo_bool/array                         1h07m56s  30GB
Dec 12 04:10:30 Starting examples/pseudo_bool/array/compilation
Dec 12 04:19:06 Finished examples/pseudo_bool/array/compilation                8m35s  16GB
Dec 12 04:19:07 Starting examples/pseudo_bool/array/compilation/proofs
Dec 12 04:21:40 Finished examples/pseudo_bool/array/compilation/proofs         2m31s   7GB
Dec 12 04:21:40 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 12 04:22:51 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m09s   6GB
Dec 12 04:22:52 Starting examples/opentheory
Dec 12 04:31:25 Finished examples/opentheory                                   8m31s   5GB
Dec 12 04:31:26 Starting examples/opentheory
Dec 12 04:31:27 Finished examples/opentheory                                      1s 121MB
Dec 12 04:31:28 Starting examples/opentheory/compilation
Dec 12 04:32:49 Finished examples/opentheory/compilation                       1m19s   5GB
Dec 12 04:32:50 Starting examples/opentheory/compilation/proofs
Dec 12 04:33:46 Finished examples/opentheory/compilation/proofs                  54s   4GB
Dec 12 04:33:46 Starting examples/opentheory/compilation/ag32
Dec 12 04:35:14 Finished examples/opentheory/compilation/ag32                  1m26s   6GB
Dec 12 04:35:15 Starting examples/opentheory/compilation/ag32/proofs
Dec 12 04:36:48 Finished examples/opentheory/compilation/ag32/proofs           1m31s   7GB
Dec 12 04:36:48 Starting examples/sat_encodings
Dec 12 04:37:49 Finished examples/sat_encodings                                  59s 910MB
Dec 12 04:37:50 Starting examples/sat_encodings/case_studies
Dec 12 04:39:33 Finished examples/sat_encodings/case_studies                   1m42s   1GB
Dec 12 04:39:34 Starting examples/sat_encodings/translation
Dec 12 04:42:59 Finished examples/sat_encodings/translation                    3m23s   2GB
Dec 12 04:43:00 Starting examples/sat_encodings/translation/compilation
Dec 12 04:44:46 Finished examples/sat_encodings/translation/compilation        1m45s   4GB
Dec 12 04:44:47 Starting examples/deflate
Dec 12 04:45:15 Finished examples/deflate                                        26s 753MB
Dec 12 04:45:16 Starting examples/deflate/translation
Dec 12 04:46:12 Finished examples/deflate/translation                            55s   2GB
Dec 12 04:46:13 Starting examples/deflate/translation/compilation
Dec 12 04:47:02 Finished examples/deflate/translation/compilation                48s   3GB
Dec 12 04:47:03 Starting examples/vipr
Dec 12 04:50:30 Finished examples/vipr                                         3m25s   4GB
Dec 12 04:50:30 Starting examples/vipr/compilation
Dec 12 04:51:24 Finished examples/vipr/compilation                               52s   4GB
Dec 12 04:51:25 Starting translator/okasaki-examples
Dec 12 04:55:28 Finished translator/okasaki-examples                           4m02s   3GB
Dec 12 04:55:29 Starting translator/other-examples
Dec 12 04:58:33 Finished translator/other-examples                             3m02s   3GB
Dec 12 04:58:34 Starting compiler/parsing/tests
Dec 12 04:59:09 Finished compiler/parsing/tests                                  34s   1GB
Dec 12 04:59:10 Starting compiler/inference/tests
Dec 12 04:59:45 Finished compiler/inference/tests                                34s   2GB
Dec 12 04:59:46 Starting compiler/printing/test
Dec 12 05:00:59 Finished compiler/printing/test                                1m11s   5GB
Dec 12 05:01:00 Starting icing/flover
Dec 12 05:35:25 Finished icing/flover                                         34m23s   2GB
Dec 12 05:35:26 Starting icing/
Dec 12 06:02:34 Finished icing/                                               27m07s   4GB
Dec 12 06:02:35 Starting icing/examples
Dec 12 06:04:10 Finished icing/examples                                        1m33s   7GB
Dec 12 06:04:11 Starting compiler/repl
Dec 12 06:12:07 Finished compiler/repl                                         7m54s   8GB
Dec 12 06:12:07 Starting unverified/sexpr-bootstrap/x64/64
Dec 12 06:15:52 Finished unverified/sexpr-bootstrap/x64/64                     3m43s  16GB
Dec 12 06:15:53 Starting unverified/sexpr-bootstrap/x64/32
Dec 12 06:19:06 Finished unverified/sexpr-bootstrap/x64/32                     3m12s  14GB
Dec 12 06:19:07 Starting compiler/benchmarks
Dec 12 06:19:53 Finished compiler/benchmarks                                     44s 711MB
Dec 12 06:19:54 Starting compiler/bootstrap/compilation/x64/64
Dec 12 06:43:46 Finished compiler/bootstrap/compilation/x64/64                23m50s  86GB
Dec 12 06:43:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 12 07:08:09 Finished compiler/bootstrap/compilation/x64/64/proofs         24m20s  53GB
Dec 12 07:08:09 Starting compiler/bootstrap/compilation/x64/32
Dec 12 07:33:24 Finished compiler/bootstrap/compilation/x64/32                25m13s  70GB
Dec 12 07:33:24 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 12 07:37:24 Finished compiler/bootstrap/compilation/x64/32/proofs          3m58s  23GB
Dec 12 07:37:25 Starting compiler/bootstrap/compilation/arm8/64
Dec 12 08:11:14 Finished compiler/bootstrap/compilation/arm8/64               33m47s  62GB
Dec 12 08:11:15 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 12 08:16:25 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m09s  29GB
Dec 12 08:16:26 Starting compiler/bootstrap/compilation/ag32/32
Dec 12 08:43:21 Finished compiler/bootstrap/compilation/ag32/32               26m53s  78GB
Dec 12 08:43:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 12 08:48:25 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m02s  31GB
Dec 12 08:48:26 SUCCESS