Job 2690

CakeML:4dea05380e66e854057dd700878ea3fb76cd1d2b
  Update NEWS.md [Oct 30 14:44:49]
HOL:a1ea6a09a473ae49be19e4cdeb39881c393f9395
  mllex: write accepting branches in source order [Oct 28 06:12:31]
Machine:pavlova
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-arm8-64.tar.gz
cake-x64-32.tar.gz

Oct 30 14:50:42 Claimed job
Oct 30 14:50:51 Building HOL
Oct 30 15:05:48 Starting developers
Oct 30 15:05:53 Finished developers                                               3s 225MB
Oct 30 15:05:54 Starting developers/bin
Oct 30 15:06:14 Finished developers/bin                                          19s   1GB
Oct 30 15:06:15 Starting compiler/proofs
Oct 30 16:53:51 Finished compiler/proofs                                    1h47m35s  37GB
Oct 30 16:53:52 Starting compiler/bootstrap/translation
Oct 31 01:52:17 Finished compiler/bootstrap/translation                     8h58m24s  59GB
Oct 31 01:52:18 Starting semantics/ffi
Oct 31 01:52:35 Finished semantics/ffi                                           16s   1GB
Oct 31 01:52:36 Starting semantics
Oct 31 01:52:37 Finished semantics                                                0s  62MB
Oct 31 01:52:38 Starting semantics/proofs
Oct 31 01:53:03 Finished semantics/proofs                                        23s 814MB
Oct 31 01:53:04 Starting semantics/alt_semantics
Oct 31 01:53:26 Finished semantics/alt_semantics                                 21s 487MB
Oct 31 01:53:27 Starting semantics/alt_semantics/proofs
Oct 31 02:03:48 Finished semantics/alt_semantics/proofs                       10m19s   3GB
Oct 31 02:03:49 Starting basis/pure
Oct 31 02:03:50 Finished basis/pure                                               0s  70MB
Oct 31 02:03:51 Starting translator
Oct 31 02:05:30 Finished translator                                            1m38s   4GB
Oct 31 02:05:31 Starting compiler/parsing
Oct 31 02:05:33 Finished compiler/parsing                                         0s  72MB
Oct 31 02:05:33 Starting characteristic
Oct 31 02:05:35 Finished characteristic                                           0s  91MB
Oct 31 02:05:36 Starting translator/monadic
Oct 31 02:05:38 Finished translator/monadic                                       0s  99MB
Oct 31 02:05:39 Starting basis
Oct 31 02:08:02 Finished basis                                                 2m21s   4GB
Oct 31 02:08:02 Starting compiler/inference
Oct 31 02:08:04 Finished compiler/inference                                       0s  95MB
Oct 31 02:08:05 Starting compiler/backend/reg_alloc
Oct 31 02:08:06 Finished compiler/backend/reg_alloc                               0s  68MB
Oct 31 02:08:07 Starting compiler/backend/gc
Oct 31 02:08:09 Finished compiler/backend/gc                                      1s 149MB
Oct 31 02:08:10 Starting compiler/backend
Oct 31 02:08:16 Finished compiler/backend                                         4s 374MB
Oct 31 02:08:17 Starting compiler/encoders/asm
Oct 31 02:08:19 Finished compiler/encoders/asm                                    0s  90MB
Oct 31 02:08:20 Starting compiler/encoders/x64
Oct 31 02:08:21 Finished compiler/encoders/x64                                    0s 103MB
Oct 31 02:08:22 Starting compiler/encoders/arm7
Oct 31 02:08:24 Finished compiler/encoders/arm7                                   0s  98MB
Oct 31 02:08:25 Starting compiler/encoders/arm8
Oct 31 02:08:26 Finished compiler/encoders/arm8                                   0s  99MB
Oct 31 02:08:27 Starting compiler/encoders/arm8_asl
Oct 31 04:24:20 Finished compiler/encoders/arm8_asl                         2h15m51s  41GB
Oct 31 04:24:21 Starting compiler/encoders/mips
Oct 31 04:24:22 Finished compiler/encoders/mips                                   0s  94MB
Oct 31 04:24:23 Starting compiler/encoders/riscv
Oct 31 04:24:25 Finished compiler/encoders/riscv                                  0s  99MB
Oct 31 04:24:26 Starting compiler/encoders/ag32
Oct 31 04:24:28 Finished compiler/encoders/ag32                                   0s  89MB
Oct 31 04:24:28 Starting compiler/backend/x64
Oct 31 04:24:30 Finished compiler/backend/x64                                     1s 140MB
Oct 31 04:24:31 Starting compiler/backend/arm7
Oct 31 04:24:33 Finished compiler/backend/arm7                                    1s 139MB
Oct 31 04:24:34 Starting compiler/backend/arm8
Oct 31 04:24:36 Finished compiler/backend/arm8                                    1s 139MB
Oct 31 04:24:37 Starting compiler/backend/mips
Oct 31 04:24:39 Finished compiler/backend/mips                                    1s 127MB
Oct 31 04:24:40 Starting compiler/backend/riscv
Oct 31 04:24:42 Finished compiler/backend/riscv                                   1s 127MB
Oct 31 04:24:43 Starting compiler/backend/ag32
Oct 31 04:25:58 Finished compiler/backend/ag32                                 1m13s   3GB
Oct 31 04:25:58 Starting compiler/parsing/proofs
Oct 31 04:26:00 Finished compiler/parsing/proofs                                  0s  74MB
Oct 31 04:26:01 Starting compiler/inference/proofs
Oct 31 04:26:03 Finished compiler/inference/proofs                                0s 100MB
Oct 31 04:26:03 Starting compiler/backend/semantics
Oct 31 04:29:21 Finished compiler/backend/semantics                            3m16s   3GB
Oct 31 04:29:22 Starting compiler/backend/reg_alloc/proofs
Oct 31 04:29:23 Finished compiler/backend/reg_alloc/proofs                        0s 100MB
Oct 31 04:29:24 Starting compiler/backend/proofs
Oct 31 04:30:19 Finished compiler/backend/proofs                                 53s   3GB
Oct 31 04:30:20 Starting compiler/backend/serialiser
Oct 31 04:30:22 Finished compiler/backend/serialiser                              1s 139MB
Oct 31 04:30:23 Starting compiler/encoders/x64/proofs
Oct 31 04:40:32 Finished compiler/encoders/x64/proofs                         10m08s   5GB
Oct 31 04:40:33 Starting compiler/encoders/arm7/proofs
Oct 31 04:53:44 Finished compiler/encoders/arm7/proofs                        13m09s  12GB
Oct 31 04:53:45 Starting compiler/encoders/arm8/proofs
Oct 31 05:00:48 Finished compiler/encoders/arm8/proofs                         7m02s   6GB
Oct 31 05:00:49 Starting compiler/encoders/arm8_asl/proofs
Oct 31 05:51:43 Finished compiler/encoders/arm8_asl/proofs                    50m53s  12GB
Oct 31 05:51:44 Starting compiler/encoders/mips/proofs
Oct 31 06:02:03 Finished compiler/encoders/mips/proofs                        10m18s  10GB
Oct 31 06:02:04 Starting compiler/encoders/riscv/proofs
Oct 31 06:11:02 Finished compiler/encoders/riscv/proofs                        8m56s   5GB
Oct 31 06:11:03 Starting compiler/encoders/ag32/proofs
Oct 31 06:13:59 Finished compiler/encoders/ag32/proofs                         2m54s   2GB
Oct 31 06:14:00 Starting compiler/backend/x64/proofs
Oct 31 06:14:47 Finished compiler/backend/x64/proofs                             45s   2GB
Oct 31 06:14:47 Starting compiler/backend/arm7/proofs
Oct 31 06:15:36 Finished compiler/backend/arm7/proofs                            47s   3GB
Oct 31 06:15:37 Starting compiler/backend/arm8/proofs
Oct 31 06:16:25 Finished compiler/backend/arm8/proofs                            47s   3GB
Oct 31 06:16:26 Starting compiler/backend/arm8_asl
Oct 31 06:16:57 Finished compiler/backend/arm8_asl                               30s   2GB
Oct 31 06:16:58 Starting compiler/backend/mips/proofs
Oct 31 06:17:48 Finished compiler/backend/mips/proofs                            49s   3GB
Oct 31 06:17:49 Starting compiler/backend/riscv/proofs
Oct 31 06:18:44 Finished compiler/backend/riscv/proofs                           54s   4GB
Oct 31 06:18:45 Starting compiler/backend/ag32/proofs
Oct 31 06:33:09 Finished compiler/backend/ag32/proofs                         14m22s   6GB
Oct 31 06:33:09 Starting compiler/backend/cv_compute
Oct 31 06:34:59 Finished compiler/backend/cv_compute                           1m48s   3GB
Oct 31 06:35:00 Starting cv_translator
Oct 31 06:54:53 Finished cv_translator                                        19m52s  11GB
Oct 31 06:54:54 Starting candle/set-theory
Oct 31 06:55:41 Finished candle/set-theory                                       46s   1GB
Oct 31 06:55:42 Starting candle/syntax-lib
Oct 31 06:55:44 Finished candle/syntax-lib                                        0s  69MB
Oct 31 06:55:45 Starting candle/standard/syntax
Oct 31 06:56:06 Finished candle/standard/syntax                                  20s   1GB
Oct 31 06:56:07 Starting candle/standard/semantics
Oct 31 06:58:54 Finished candle/standard/semantics                             2m46s   2GB
Oct 31 06:58:55 Starting candle/standard/monadic
Oct 31 06:58:57 Finished candle/standard/monadic                                  0s 106MB
Oct 31 06:58:57 Starting candle/standard/ml_kernel
Oct 31 07:01:02 Finished candle/standard/ml_kernel                             2m03s   5GB
Oct 31 07:01:03 Starting candle/overloading/syntax
Oct 31 07:04:50 Finished candle/overloading/syntax                             3m46s   3GB
Oct 31 07:04:51 Starting candle/overloading/semantics
Oct 31 07:16:43 Finished candle/overloading/semantics                         11m51s   5GB
Oct 31 07:16:44 Starting candle/overloading/monadic
Oct 31 07:19:16 Finished candle/overloading/monadic                            2m30s   2GB
Oct 31 07:19:16 Starting candle/overloading/ml_kernel
Oct 31 07:27:19 Finished candle/overloading/ml_kernel                          8m01s   7GB
Oct 31 07:27:20 Starting candle/overloading/ml_checker
Oct 31 07:30:08 Finished candle/overloading/ml_checker                         2m47s   7GB
Oct 31 07:30:09 Starting candle/prover
Oct 31 07:40:45 Finished candle/prover                                        10m34s   5GB
Oct 31 07:40:46 Starting pancake
Oct 31 07:41:13 Finished pancake                                                 26s 968MB
Oct 31 07:41:14 Starting pancake/ffi
Oct 31 07:41:15 Finished pancake/ffi                                              0s  23MB
Oct 31 07:41:16 Starting pancake/semantics
Oct 31 07:43:28 Finished pancake/semantics                                     2m10s   2GB
Oct 31 07:43:28 Starting pancake/parser
Oct 31 07:43:53 Finished pancake/parser                                          23s 574MB
Oct 31 07:43:54 Starting pancake/proofs
Oct 31 08:00:18 Finished pancake/proofs                                       16m23s  10GB
Oct 31 08:00:19 Starting compiler/dafny
Oct 31 08:02:57 Finished compiler/dafny                                        2m36s  10GB
Oct 31 08:02:58 Starting compiler/dafny/translation
Oct 31 08:32:02 Finished compiler/dafny/translation                           29m02s  25GB
Oct 31 08:32:03 Starting compiler/dafny/compilation
Oct 31 08:35:42 Finished compiler/dafny/compilation                            3m38s  15GB
Oct 31 08:35:43 Starting compiler/dafny/semantics
Oct 31 08:36:21 Finished compiler/dafny/semantics                                36s   1GB
Oct 31 08:36:22 Starting characteristic/examples
Oct 31 08:37:55 Finished characteristic/examples                               1m32s   5GB
Oct 31 08:37:56 Starting tutorial/solutions
Oct 31 08:40:51 Finished tutorial/solutions                                    2m53s   6GB
Oct 31 08:40:52 Starting translator/monadic/examples
Oct 31 08:44:00 Finished translator/monadic/examples                           3m06s   4GB
Oct 31 08:44:01 Starting examples
Oct 31 08:56:25 Finished examples                                             12m23s   5GB
Oct 31 08:56:26 Starting examples/compilation/x64
Oct 31 09:06:30 Finished examples/compilation/x64                             10m03s   7GB
Oct 31 09:06:31 Starting examples/compilation/x64/proofs
Oct 31 09:11:35 Finished examples/compilation/x64/proofs                       5m03s   8GB
Oct 31 09:11:36 Starting examples/compilation/ag32
Oct 31 09:14:25 Finished examples/compilation/ag32                             2m47s   5GB
Oct 31 09:14:25 Starting examples/compilation/ag32/proofs
Oct 31 09:16:19 Finished examples/compilation/ag32/proofs                      1m52s   8GB
Oct 31 09:16:19 Starting examples/compilation/to_word
Oct 31 09:20:38 Finished examples/compilation/to_word                          4m17s  13GB
Oct 31 09:20:39 Starting examples/lpr_checker
Oct 31 09:21:11 Finished examples/lpr_checker                                    30s   1GB
Oct 31 09:21:12 Starting examples/lpr_checker/array
Oct 31 09:47:50 Finished examples/lpr_checker/array                           26m36s  28GB
Oct 31 09:47:50 Starting examples/lpr_checker/array/compilation
Oct 31 09:50:32 Finished examples/lpr_checker/array/compilation                2m40s  10GB
Oct 31 09:50:32 Starting examples/lpr_checker/array/compilation/proofs
Oct 31 09:52:37 Finished examples/lpr_checker/array/compilation/proofs         2m03s   9GB
Oct 31 09:52:38 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 31 09:54:31 Finished examples/lpr_checker/array/compilation/proofsARM8     1m52s   8GB
Oct 31 09:54:32 Starting examples/xlrup_checker
Oct 31 09:55:08 Finished examples/xlrup_checker                                  34s   1GB
Oct 31 09:55:09 Starting examples/xlrup_checker/array
Oct 31 10:08:12 Finished examples/xlrup_checker/array                         13m02s  12GB
Oct 31 10:08:13 Starting examples/xlrup_checker/array/compilation
Oct 31 10:09:40 Finished examples/xlrup_checker/array/compilation              1m25s   6GB
Oct 31 10:09:41 Starting examples/xlrup_checker/array/compilation/proofs
Oct 31 10:11:41 Finished examples/xlrup_checker/array/compilation/proofs       1m59s   7GB
Oct 31 10:11:42 Starting examples/pseudo_bool
Oct 31 10:13:17 Finished examples/pseudo_bool                                  1m34s   2GB
Oct 31 10:13:18 Starting examples/pseudo_bool/cnf_encoding
Oct 31 10:14:01 Finished examples/pseudo_bool/cnf_encoding                       42s   1GB
Oct 31 10:14:02 Starting examples/pseudo_bool/graph_encoding
Oct 31 10:15:01 Finished examples/pseudo_bool/graph_encoding                     58s   2GB
Oct 31 10:15:02 Starting examples/pseudo_bool/array
Oct 31 11:25:12 Finished examples/pseudo_bool/array                         1h10m09s  44GB
Oct 31 11:25:13 Starting examples/pseudo_bool/array/compilation
Oct 31 11:40:00 Finished examples/pseudo_bool/array/compilation               14m46s  32GB
Oct 31 11:40:01 Starting examples/pseudo_bool/array/compilation/proofs
Oct 31 11:44:22 Finished examples/pseudo_bool/array/compilation/proofs         4m20s  10GB
Oct 31 11:44:23 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 31 11:46:30 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m06s   7GB
Oct 31 11:46:31 Starting examples/opentheory
Oct 31 11:55:24 Finished examples/opentheory                                   8m52s   5GB
Oct 31 11:55:25 Starting examples/opentheory
Oct 31 11:55:27 Finished examples/opentheory                                      1s 134MB
Oct 31 11:55:28 Starting examples/opentheory/compilation
Oct 31 11:57:36 Finished examples/opentheory/compilation                       2m07s   9GB
Oct 31 11:57:37 Starting examples/opentheory/compilation/proofs
Oct 31 11:59:32 Finished examples/opentheory/compilation/proofs                1m53s   7GB
Oct 31 11:59:33 Starting examples/opentheory/compilation/ag32
Oct 31 12:01:43 Finished examples/opentheory/compilation/ag32                  2m09s   9GB
Oct 31 12:01:44 Starting examples/opentheory/compilation/ag32/proofs
Oct 31 12:04:25 Finished examples/opentheory/compilation/ag32/proofs           2m39s  12GB
Oct 31 12:04:26 Starting examples/sat_encodings
Oct 31 12:05:30 Finished examples/sat_encodings                                1m03s 941MB
Oct 31 12:05:31 Starting examples/sat_encodings/case_studies
Oct 31 12:07:45 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 31 12:07:46 Starting examples/sat_encodings/translation
Oct 31 12:11:30 Finished examples/sat_encodings/translation                    3m43s   3GB
Oct 31 12:11:31 Starting examples/sat_encodings/translation/compilation
Oct 31 12:14:08 Finished examples/sat_encodings/translation/compilation        2m36s   7GB
Oct 31 12:14:09 Starting examples/deflate
Oct 31 12:14:37 Finished examples/deflate                                        27s 688MB
Oct 31 12:14:38 Starting examples/deflate/translation
Oct 31 12:15:39 Finished examples/deflate/translation                            59s   2GB
Oct 31 12:15:40 Starting examples/deflate/translation/compilation
Oct 31 12:16:49 Finished examples/deflate/translation/compilation              1m08s   6GB
Oct 31 12:16:50 Starting examples/vipr
Oct 31 12:20:29 Finished examples/vipr                                         3m37s   4GB
Oct 31 12:20:30 Starting examples/vipr/compilation
Oct 31 12:21:50 Finished examples/vipr/compilation                             1m19s   6GB
Oct 31 12:21:51 Starting translator/okasaki-examples
Oct 31 12:26:10 Finished translator/okasaki-examples                           4m18s   5GB
Oct 31 12:26:11 Starting translator/other-examples
Oct 31 12:31:12 Finished translator/other-examples                             5m00s   3GB
Oct 31 12:31:13 Starting compiler/parsing/tests
Oct 31 12:31:52 Finished compiler/parsing/tests                                  38s   2GB
Oct 31 12:31:53 Starting compiler/inference/tests
Oct 31 12:32:41 Finished compiler/inference/tests                                46s   3GB
Oct 31 12:32:42 Starting compiler/printing/test
Oct 31 12:34:27 Finished compiler/printing/test                                1m44s   7GB
Oct 31 12:34:28 Starting icing/flover
Oct 31 13:11:48 Finished icing/flover                                         37m18s   4GB
Oct 31 13:11:48 Starting icing/
Oct 31 13:39:38 Finished icing/                                               27m48s   9GB
Oct 31 13:39:39 Starting icing/examples
Oct 31 13:41:38 Finished icing/examples                                        1m58s   9GB
Oct 31 13:41:39 Starting compiler/repl
Oct 31 13:50:51 Finished compiler/repl                                         9m11s   9GB
Oct 31 13:50:52 Starting unverified/sexpr-bootstrap/x64/64
Oct 31 14:05:17 Finished unverified/sexpr-bootstrap/x64/64                    13m57s  17GB
Oct 31 14:05:18 Starting unverified/sexpr-bootstrap/x64/32
Oct 31 14:16:54 Finished unverified/sexpr-bootstrap/x64/32                    11m14s  14GB
Oct 31 14:16:55 Starting compiler/benchmarks
Oct 31 14:17:40 Finished compiler/benchmarks                                     44s 712MB
Oct 31 14:17:41 Starting compiler/bootstrap/compilation/x64/64
Oct 31 15:06:16 Finished compiler/bootstrap/compilation/x64/64                48m21s 137GB
Oct 31 15:06:17 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 31 15:31:51 Finished compiler/bootstrap/compilation/x64/64/proofs         25m32s  62GB
Oct 31 15:31:52 Starting compiler/bootstrap/compilation/x64/32
Oct 31 16:13:53 Finished compiler/bootstrap/compilation/x64/32                41m52s 107GB
Oct 31 16:13:53 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 31 16:19:06 Finished compiler/bootstrap/compilation/x64/32/proofs          5m11s  24GB
Oct 31 16:19:07 Starting compiler/bootstrap/compilation/arm8/64
Oct 31 17:19:41 Finished compiler/bootstrap/compilation/arm8/64             1h00m24s 138GB
Oct 31 17:19:42 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 31 17:25:57 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m14s  31GB
Oct 31 17:25:58 Starting compiler/bootstrap/compilation/ag32/32
Oct 31 18:09:26 Finished compiler/bootstrap/compilation/ag32/32               43m27s 111GB
Oct 31 18:09:27 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 31 18:15:05 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m37s  31GB
Oct 31 18:15:06 SUCCESS