Job 2559

CakeML:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:a18a10ab99c90f2d4e47536b411eeee5bec72004
  some FUNPOW Tau and spin lemmas for itreeTau [Aug 16 00:45:50]
Machine:lammmington
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

Aug 20 11:24:39 Claimed job
Aug 20 11:24:45 Building HOL
Aug 20 11:38:57 Starting developers
Aug 20 11:39:01 Finished developers                                               2s 232MB
Aug 20 11:39:02 Starting developers/bin
Aug 20 11:39:12 Finished developers/bin                                           9s   1GB
Aug 20 11:39:13 Starting compiler/proofs
Aug 20 13:36:04 Finished compiler/proofs                                    1h56m49s  39GB
Aug 20 13:36:04 Starting compiler/bootstrap/translation
Aug 20 22:22:38 Finished compiler/bootstrap/translation                     8h46m33s  59GB
Aug 20 22:22:39 Starting semantics/ffi
Aug 20 22:22:48 Finished semantics/ffi                                            7s 635MB
Aug 20 22:22:49 Starting semantics
Aug 20 22:22:50 Finished semantics                                                0s  65MB
Aug 20 22:22:51 Starting semantics/proofs
Aug 20 22:23:28 Finished semantics/proofs                                        36s   2GB
Aug 20 22:23:29 Starting semantics/alt_semantics
Aug 20 22:24:18 Finished semantics/alt_semantics                                 47s   1GB
Aug 20 22:24:18 Starting semantics/alt_semantics/proofs
Aug 20 22:35:32 Finished semantics/alt_semantics/proofs                       11m12s   3GB
Aug 20 22:35:33 Starting basis/pure
Aug 20 22:35:34 Finished basis/pure                                               0s  74MB
Aug 20 22:35:35 Starting translator
Aug 20 22:37:20 Finished translator                                            1m44s   3GB
Aug 20 22:37:21 Starting compiler/parsing
Aug 20 22:37:22 Finished compiler/parsing                                         0s  73MB
Aug 20 22:37:23 Starting characteristic
Aug 20 22:37:25 Finished characteristic                                           0s  93MB
Aug 20 22:37:26 Starting translator/monadic
Aug 20 22:37:27 Finished translator/monadic                                       0s 102MB
Aug 20 22:37:28 Starting basis
Aug 20 22:41:06 Finished basis                                                 3m37s   5GB
Aug 20 22:41:07 Starting compiler/inference
Aug 20 22:41:08 Finished compiler/inference                                       0s  93MB
Aug 20 22:41:09 Starting compiler/backend/reg_alloc
Aug 20 22:41:11 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 20 22:41:11 Starting compiler/backend/gc
Aug 20 22:41:13 Finished compiler/backend/gc                                      0s 147MB
Aug 20 22:41:14 Starting compiler/backend
Aug 20 22:41:35 Finished compiler/backend                                        19s   1GB
Aug 20 22:41:35 Starting compiler/encoders/asm
Aug 20 22:41:37 Finished compiler/encoders/asm                                    0s  91MB
Aug 20 22:41:38 Starting compiler/encoders/x64
Aug 20 22:41:39 Finished compiler/encoders/x64                                    0s 102MB
Aug 20 22:41:40 Starting compiler/encoders/arm7
Aug 20 22:41:42 Finished compiler/encoders/arm7                                   0s 102MB
Aug 20 22:41:43 Starting compiler/encoders/arm8
Aug 20 22:41:44 Finished compiler/encoders/arm8                                   0s 103MB
Aug 20 22:41:45 Starting compiler/encoders/arm8_asl
Aug 21 01:07:39 Finished compiler/encoders/arm8_asl                         2h25m53s  44GB
Aug 21 01:07:40 Starting compiler/encoders/mips
Aug 21 01:07:42 Finished compiler/encoders/mips                                   0s 103MB
Aug 21 01:07:43 Starting compiler/encoders/riscv
Aug 21 01:07:44 Finished compiler/encoders/riscv                                  0s 103MB
Aug 21 01:07:45 Starting compiler/encoders/ag32
Aug 21 01:07:46 Finished compiler/encoders/ag32                                   0s  93MB
Aug 21 01:07:47 Starting compiler/backend/x64
Aug 21 01:07:49 Finished compiler/backend/x64                                     0s 144MB
Aug 21 01:07:50 Starting compiler/backend/arm7
Aug 21 01:07:52 Finished compiler/backend/arm7                                    0s 144MB
Aug 21 01:07:53 Starting compiler/backend/arm8
Aug 21 01:07:54 Finished compiler/backend/arm8                                    0s 145MB
Aug 21 01:07:55 Starting compiler/backend/mips
Aug 21 01:07:57 Finished compiler/backend/mips                                    0s 143MB
Aug 21 01:07:58 Starting compiler/backend/riscv
Aug 21 01:08:00 Finished compiler/backend/riscv                                   0s 144MB
Aug 21 01:08:01 Starting compiler/backend/ag32
Aug 21 01:09:23 Finished compiler/backend/ag32                                 1m21s   4GB
Aug 21 01:09:24 Starting compiler/parsing/proofs
Aug 21 01:09:25 Finished compiler/parsing/proofs                                  0s  74MB
Aug 21 01:09:26 Starting compiler/inference/proofs
Aug 21 01:09:27 Finished compiler/inference/proofs                                0s  91MB
Aug 21 01:09:28 Starting compiler/backend/semantics
Aug 21 01:13:15 Finished compiler/backend/semantics                            3m46s   2GB
Aug 21 01:13:16 Starting compiler/backend/reg_alloc/proofs
Aug 21 01:13:18 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
Aug 21 01:13:19 Starting compiler/backend/proofs
Aug 21 01:14:24 Finished compiler/backend/proofs                               1m04s   3GB
Aug 21 01:14:25 Starting compiler/backend/serialiser
Aug 21 01:14:27 Finished compiler/backend/serialiser                              0s 148MB
Aug 21 01:14:28 Starting compiler/encoders/x64/proofs
Aug 21 01:23:58 Finished compiler/encoders/x64/proofs                          9m29s   5GB
Aug 21 01:23:59 Starting compiler/encoders/arm7/proofs
Aug 21 01:37:04 Finished compiler/encoders/arm7/proofs                        13m04s   9GB
Aug 21 01:37:05 Starting compiler/encoders/arm8/proofs
Aug 21 01:43:42 Finished compiler/encoders/arm8/proofs                         6m35s   5GB
Aug 21 01:43:42 Starting compiler/encoders/arm8_asl/proofs
Aug 21 02:30:59 Finished compiler/encoders/arm8_asl/proofs                    47m16s   7GB
Aug 21 02:31:00 Starting compiler/encoders/mips/proofs
Aug 21 02:41:03 Finished compiler/encoders/mips/proofs                        10m01s  10GB
Aug 21 02:41:03 Starting compiler/encoders/riscv/proofs
Aug 21 02:49:12 Finished compiler/encoders/riscv/proofs                        8m07s   4GB
Aug 21 02:49:13 Starting compiler/encoders/ag32/proofs
Aug 21 02:51:38 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 21 02:51:39 Starting compiler/backend/x64/proofs
Aug 21 02:52:21 Finished compiler/backend/x64/proofs                             42s   3GB
Aug 21 02:52:22 Starting compiler/backend/arm7/proofs
Aug 21 02:53:08 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 21 02:53:09 Starting compiler/backend/arm8/proofs
Aug 21 02:53:51 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 21 02:53:52 Starting compiler/backend/arm8_asl
Aug 21 02:54:22 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 21 02:54:23 Starting compiler/backend/mips/proofs
Aug 21 02:55:09 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 21 02:55:10 Starting compiler/backend/riscv/proofs
Aug 21 02:56:03 Finished compiler/backend/riscv/proofs                           52s   4GB
Aug 21 02:56:04 Starting compiler/backend/ag32/proofs
Aug 21 03:10:22 Finished compiler/backend/ag32/proofs                         14m17s   6GB
Aug 21 03:10:23 Starting compiler/backend/cv_compute
Aug 21 03:12:06 Finished compiler/backend/cv_compute                           1m42s   3GB
Aug 21 03:12:07 Starting cv_translator
Aug 21 03:31:36 Finished cv_translator                                        19m28s  13GB
Aug 21 03:31:37 Starting candle/set-theory
Aug 21 03:32:28 Finished candle/set-theory                                       50s   1GB
Aug 21 03:32:30 Starting candle/syntax-lib
Aug 21 03:32:31 Finished candle/syntax-lib                                        0s  73MB
Aug 21 03:32:32 Starting candle/standard/syntax
Aug 21 03:32:51 Finished candle/standard/syntax                                  17s   1GB
Aug 21 03:32:52 Starting candle/standard/semantics
Aug 21 03:35:32 Finished candle/standard/semantics                             2m39s   3GB
Aug 21 03:35:32 Starting candle/standard/monadic
Aug 21 03:35:34 Finished candle/standard/monadic                                  0s 108MB
Aug 21 03:35:35 Starting candle/standard/ml_kernel
Aug 21 03:37:36 Finished candle/standard/ml_kernel                             1m59s   5GB
Aug 21 03:37:37 Starting candle/overloading/syntax
Aug 21 03:41:07 Finished candle/overloading/syntax                             3m30s   2GB
Aug 21 03:41:08 Starting candle/overloading/semantics
Aug 21 03:52:31 Finished candle/overloading/semantics                         11m22s   5GB
Aug 21 03:52:32 Starting candle/overloading/monadic
Aug 21 03:55:09 Finished candle/overloading/monadic                            2m35s   2GB
Aug 21 03:55:10 Starting candle/overloading/ml_kernel
Aug 21 04:03:01 Finished candle/overloading/ml_kernel                          7m50s   7GB
Aug 21 04:03:02 Starting candle/overloading/ml_checker
Aug 21 04:05:38 Finished candle/overloading/ml_checker                         2m35s   7GB
Aug 21 04:05:39 Starting candle/prover
Aug 21 04:16:02 Finished candle/prover                                        10m21s   5GB
Aug 21 04:16:03 Starting pancake
Aug 21 04:17:14 Finished pancake                                               1m10s   1GB
Aug 21 04:17:15 Starting pancake/ffi
Aug 21 04:17:16 Finished pancake/ffi                                              0s  24MB
Aug 21 04:17:17 Starting pancake/semantics
Aug 21 04:20:02 Finished pancake/semantics                                     2m44s   2GB
Aug 21 04:20:03 Starting pancake/parser
Aug 21 04:20:40 Finished pancake/parser                                          36s   2GB
Aug 21 04:20:41 Starting pancake/proofs
Aug 21 04:36:32 Finished pancake/proofs                                       15m50s   7GB
Aug 21 04:36:32 Starting characteristic/examples
Aug 21 04:38:11 Finished characteristic/examples                               1m38s   6GB
Aug 21 04:38:12 Starting tutorial/solutions
Aug 21 04:41:01 Finished tutorial/solutions                                    2m47s   5GB
Aug 21 04:41:02 Starting translator/monadic/examples
Aug 21 04:45:01 Finished translator/monadic/examples                           3m58s   5GB
Aug 21 04:45:02 Starting examples
Aug 21 05:00:07 Finished examples                                             15m04s   8GB
Aug 21 05:00:08 Starting examples/compilation/x64
Aug 21 05:09:37 Finished examples/compilation/x64                              9m28s   7GB
Aug 21 05:09:38 Starting examples/compilation/x64/proofs
Aug 21 05:14:12 Finished examples/compilation/x64/proofs                       4m32s   7GB
Aug 21 05:14:13 Starting examples/compilation/ag32
Aug 21 05:16:55 Finished examples/compilation/ag32                             2m40s   5GB
Aug 21 05:16:55 Starting examples/compilation/ag32/proofs
Aug 21 05:18:41 Finished examples/compilation/ag32/proofs                      1m44s   9GB
Aug 21 05:18:41 Starting examples/compilation/to_word
Aug 21 05:22:42 Finished examples/compilation/to_word                          3m59s  12GB
Aug 21 05:22:42 Starting examples/lpr_checker
Aug 21 05:24:03 Finished examples/lpr_checker                                  1m19s   2GB
Aug 21 05:24:04 Starting examples/lpr_checker/array
Aug 21 05:53:30 Finished examples/lpr_checker/array                           29m25s  29GB
Aug 21 05:53:31 Starting examples/lpr_checker/array/compilation
Aug 21 05:56:09 Finished examples/lpr_checker/array/compilation                2m37s  10GB
Aug 21 05:56:10 Starting examples/lpr_checker/array/compilation/proofs
Aug 21 05:58:05 Finished examples/lpr_checker/array/compilation/proofs         1m54s   8GB
Aug 21 05:58:06 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 21 05:59:57 Finished examples/lpr_checker/array/compilation/proofsARM8     1m49s   9GB
Aug 21 05:59:57 Starting examples/xlrup_checker
Aug 21 06:01:10 Finished examples/xlrup_checker                                1m11s   1GB
Aug 21 06:01:11 Starting examples/xlrup_checker/array
Aug 21 06:16:41 Finished examples/xlrup_checker/array                         15m29s   7GB
Aug 21 06:16:42 Starting examples/xlrup_checker/array/compilation
Aug 21 06:18:07 Finished examples/xlrup_checker/array/compilation              1m23s   6GB
Aug 21 06:18:08 Starting examples/xlrup_checker/array/compilation/proofs
Aug 21 06:19:46 Finished examples/xlrup_checker/array/compilation/proofs       1m37s   8GB
Aug 21 06:19:47 Starting examples/pseudo_bool
Aug 21 06:21:58 Finished examples/pseudo_bool                                  2m10s   2GB
Aug 21 06:21:59 Starting examples/pseudo_bool/cnf_encoding
Aug 21 06:22:37 Finished examples/pseudo_bool/cnf_encoding                       37s   1GB
Aug 21 06:22:38 Starting examples/pseudo_bool/graph_encoding
Aug 21 06:23:32 Finished examples/pseudo_bool/graph_encoding                     53s   2GB
Aug 21 06:23:33 Starting examples/pseudo_bool/array
Aug 21 07:30:35 Finished examples/pseudo_bool/array                         1h07m01s  34GB
Aug 21 07:30:36 Starting examples/pseudo_bool/array/compilation
Aug 21 07:44:09 Finished examples/pseudo_bool/array/compilation               13m32s  29GB
Aug 21 07:44:10 Starting examples/pseudo_bool/array/compilation/proofs
Aug 21 07:48:15 Finished examples/pseudo_bool/array/compilation/proofs         4m03s  10GB
Aug 21 07:48:16 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 21 07:50:04 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m46s  11GB
Aug 21 07:50:04 Starting examples/opentheory
Aug 21 08:01:17 Finished examples/opentheory                                  11m11s   7GB
Aug 21 08:01:18 Starting examples/opentheory
Aug 21 08:01:20 Finished examples/opentheory                                      0s 137MB
Aug 21 08:01:21 Starting examples/opentheory/compilation
Aug 21 08:03:29 Finished examples/opentheory/compilation                       2m07s   9GB
Aug 21 08:03:30 Starting examples/opentheory/compilation/proofs
Aug 21 08:05:21 Finished examples/opentheory/compilation/proofs                1m50s   7GB
Aug 21 08:05:22 Starting examples/opentheory/compilation/ag32
Aug 21 08:07:33 Finished examples/opentheory/compilation/ag32                  2m10s   9GB
Aug 21 08:07:34 Starting examples/opentheory/compilation/ag32/proofs
Aug 21 08:10:00 Finished examples/opentheory/compilation/ag32/proofs           2m24s  10GB
Aug 21 08:10:01 Starting examples/sat_encodings
Aug 21 08:12:59 Finished examples/sat_encodings                                2m57s   1GB
Aug 21 08:13:00 Starting examples/sat_encodings/case_studies
Aug 21 08:15:08 Finished examples/sat_encodings/case_studies                   2m07s   2GB
Aug 21 08:15:09 Starting examples/sat_encodings/translation
Aug 21 08:21:38 Finished examples/sat_encodings/translation                    6m28s   7GB
Aug 21 08:21:39 Starting examples/sat_encodings/translation/compilation
Aug 21 08:24:08 Finished examples/sat_encodings/translation/compilation        2m27s   7GB
Aug 21 08:24:09 Starting examples/deflate
Aug 21 08:25:35 Finished examples/deflate                                      1m25s   1GB
Aug 21 08:25:36 Starting examples/deflate/translation
Aug 21 08:27:19 Finished examples/deflate/translation                          1m41s   7GB
Aug 21 08:27:20 Starting examples/deflate/translation/compilation
Aug 21 08:28:27 Finished examples/deflate/translation/compilation              1m06s   6GB
Aug 21 08:28:28 Starting examples/vipr
Aug 21 08:32:56 Finished examples/vipr                                         4m26s   8GB
Aug 21 08:32:56 Starting examples/vipr/compilation
Aug 21 08:34:15 Finished examples/vipr/compilation                             1m17s   6GB
Aug 21 08:34:16 Starting translator/okasaki-examples
Aug 21 08:39:26 Finished translator/okasaki-examples                           5m09s   5GB
Aug 21 08:39:27 Starting translator/other-examples
Aug 21 08:44:38 Finished translator/other-examples                             5m10s   3GB
Aug 21 08:44:39 Starting compiler/parsing/tests
Aug 21 08:45:17 Finished compiler/parsing/tests                                  37s   1GB
Aug 21 08:45:18 Starting compiler/inference/tests
Aug 21 08:46:02 Finished compiler/inference/tests                                43s   3GB
Aug 21 08:46:03 Starting compiler/printing/test
Aug 21 08:47:38 Finished compiler/printing/test                                1m34s   6GB
Aug 21 08:47:39 Starting icing/flover
Aug 21 09:25:05 Finished icing/flover                                         37m24s   4GB
Aug 21 09:25:06 Starting icing/
Aug 21 09:53:02 Finished icing/                                               27m55s   9GB
Aug 21 09:53:02 Starting icing/examples
Aug 21 09:54:53 Finished icing/examples                                        1m49s   9GB
Aug 21 09:54:54 Starting compiler/repl
Aug 21 10:04:01 Finished compiler/repl                                         9m06s  11GB
Aug 21 10:04:02 Starting unverified/sexpr-bootstrap/x64/64
Aug 21 10:17:32 Finished unverified/sexpr-bootstrap/x64/64                    13m04s  18GB
Aug 21 10:17:33 Starting unverified/sexpr-bootstrap/x64/32
Aug 21 10:28:28 Finished unverified/sexpr-bootstrap/x64/32                    10m31s  15GB
Aug 21 10:28:29 Starting compiler/benchmarks
Aug 21 10:29:14 Finished compiler/benchmarks                                     44s 713MB
Aug 21 10:29:15 Starting compiler/bootstrap/compilation/x64/64
Aug 21 11:13:42 Finished compiler/bootstrap/compilation/x64/64                44m13s 137GB
Aug 21 11:13:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 21 11:37:12 Finished compiler/bootstrap/compilation/x64/64/proofs         23m28s  50GB
Aug 21 11:37:13 Starting compiler/bootstrap/compilation/x64/32
Aug 21 12:15:53 Finished compiler/bootstrap/compilation/x64/32                38m32s  92GB
Aug 21 12:15:54 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 21 12:21:01 Finished compiler/bootstrap/compilation/x64/32/proofs          5m05s  24GB
Aug 21 12:21:02 Starting compiler/bootstrap/compilation/arm8/64
Aug 21 13:16:28 Finished compiler/bootstrap/compilation/arm8/64               55m16s 125GB
Aug 21 13:16:28 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 21 13:22:04 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m34s  32GB
Aug 21 13:22:04 Starting compiler/bootstrap/compilation/ag32/32
Aug 21 14:02:59 Finished compiler/bootstrap/compilation/ag32/32               40m53s 111GB
Aug 21 14:03:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 21 14:08:41 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m40s  32GB
Aug 21 14:08:42 SUCCESS