Job 2237

CakeML:7101a3f2e0c3885412c05e63735ec6da155253ee
  Fix for adjusted Inductive syntax [Nov 08 21:36:03]
HOL:e7f2e175666a4f2e69629143d260e17e1817b475
  Minor additions to cv<->term transfer theorems [Nov 13 06:11:30]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Nov 14 13:16:45 Claimed job
Nov 14 13:16:51 Building HOL
Nov 14 13:30:30 Starting developers
Nov 14 13:30:35 Finished developers                                               5s  95MB
Nov 14 13:30:36 Starting developers/bin
Nov 14 13:30:43 Finished developers/bin                                           6s   1GB
Nov 14 13:30:43 Starting compiler/proofs
Nov 14 15:24:29 Finished compiler/proofs                                    1h53m45s  17GB
Nov 14 15:24:29 Starting compiler/bootstrap/translation
Nov 14 23:39:51 Finished compiler/bootstrap/translation                     8h15m21s  43GB
Nov 14 23:39:51 Starting semantics/ffi
Nov 14 23:39:56 Finished semantics/ffi                                            4s 385MB
Nov 14 23:39:56 Starting semantics
Nov 14 23:39:57 Finished semantics                                                1s  17MB
Nov 14 23:39:57 Starting semantics/proofs
Nov 14 23:40:30 Finished semantics/proofs                                        32s 759MB
Nov 14 23:40:30 Starting semantics/alt_semantics
Nov 14 23:41:02 Finished semantics/alt_semantics                                 31s 796MB
Nov 14 23:41:02 Starting semantics/alt_semantics/proofs
Nov 14 23:52:55 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Nov 14 23:52:55 Starting basis/pure
Nov 14 23:52:57 Finished basis/pure                                               1s  18MB
Nov 14 23:52:57 Starting translator
Nov 14 23:54:46 Finished translator                                            1m49s   1GB
Nov 14 23:54:46 Starting compiler/parsing
Nov 14 23:54:48 Finished compiler/parsing                                         1s  19MB
Nov 14 23:54:48 Starting characteristic
Nov 14 23:54:50 Finished characteristic                                           1s  23MB
Nov 14 23:54:50 Starting translator/monadic
Nov 14 23:54:52 Finished translator/monadic                                       1s  20MB
Nov 14 23:54:52 Starting basis
Nov 14 23:58:49 Finished basis                                                 3m56s   2GB
Nov 14 23:58:49 Starting compiler/inference
Nov 14 23:58:51 Finished compiler/inference                                       1s  21MB
Nov 14 23:58:51 Starting compiler/backend/reg_alloc
Nov 14 23:58:53 Finished compiler/backend/reg_alloc                               1s  18MB
Nov 14 23:58:53 Starting compiler/backend/gc
Nov 14 23:58:55 Finished compiler/backend/gc                                      2s  21MB
Nov 14 23:58:55 Starting compiler/backend
Nov 14 23:59:07 Finished compiler/backend                                        12s 821MB
Nov 14 23:59:08 Starting compiler/encoders/asm
Nov 14 23:59:09 Finished compiler/encoders/asm                                    1s  23MB
Nov 14 23:59:09 Starting compiler/encoders/x64
Nov 14 23:59:11 Finished compiler/encoders/x64                                    1s  25MB
Nov 14 23:59:11 Starting compiler/encoders/arm7
Nov 14 23:59:13 Finished compiler/encoders/arm7                                   1s  22MB
Nov 14 23:59:13 Starting compiler/encoders/arm8
Nov 14 23:59:15 Finished compiler/encoders/arm8                                   1s  24MB
Nov 14 23:59:15 Starting compiler/encoders/arm8_asl
Nov 15 02:25:56 Finished compiler/encoders/arm8_asl                         2h26m40s  45GB
Nov 15 02:25:56 Starting compiler/encoders/mips
Nov 15 02:25:58 Finished compiler/encoders/mips                                   1s  18MB
Nov 15 02:25:58 Starting compiler/encoders/riscv
Nov 15 02:26:00 Finished compiler/encoders/riscv                                  1s  22MB
Nov 15 02:26:00 Starting compiler/encoders/ag32
Nov 15 02:26:02 Finished compiler/encoders/ag32                                   1s  20MB
Nov 15 02:26:02 Starting compiler/backend/x64
Nov 15 02:26:04 Finished compiler/backend/x64                                     2s  27MB
Nov 15 02:26:04 Starting compiler/backend/arm7
Nov 15 02:26:06 Finished compiler/backend/arm7                                    2s  23MB
Nov 15 02:26:06 Starting compiler/backend/arm8
Nov 15 02:26:09 Finished compiler/backend/arm8                                    2s  25MB
Nov 15 02:26:09 Starting compiler/backend/mips
Nov 15 02:26:11 Finished compiler/backend/mips                                    2s  22MB
Nov 15 02:26:11 Starting compiler/backend/riscv
Nov 15 02:26:13 Finished compiler/backend/riscv                                   2s  27MB
Nov 15 02:26:13 Starting compiler/backend/ag32
Nov 15 02:27:38 Finished compiler/backend/ag32                                 1m24s   1GB
Nov 15 02:27:38 Starting compiler/parsing/proofs
Nov 15 02:27:40 Finished compiler/parsing/proofs                                  1s  17MB
Nov 15 02:27:40 Starting compiler/inference/proofs
Nov 15 02:27:42 Finished compiler/inference/proofs                                1s  20MB
Nov 15 02:27:42 Starting compiler/backend/semantics
Nov 15 02:28:55 Finished compiler/backend/semantics                            1m12s   1GB
Nov 15 02:28:55 Starting compiler/backend/reg_alloc/proofs
Nov 15 02:28:57 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Nov 15 02:28:57 Starting compiler/backend/proofs
Nov 15 02:29:55 Finished compiler/backend/proofs                                 58s   2GB
Nov 15 02:29:55 Starting compiler/backend/serialiser
Nov 15 02:29:58 Finished compiler/backend/serialiser                              2s  29MB
Nov 15 02:29:59 Starting compiler/encoders/x64/proofs
Nov 15 02:39:55 Finished compiler/encoders/x64/proofs                          9m56s   5GB
Nov 15 02:39:55 Starting compiler/encoders/arm7/proofs
Nov 15 02:53:49 Finished compiler/encoders/arm7/proofs                        13m54s   4GB
Nov 15 02:53:49 Starting compiler/encoders/arm8/proofs
Nov 15 03:00:39 Finished compiler/encoders/arm8/proofs                         6m49s   1GB
Nov 15 03:00:39 Starting compiler/encoders/arm8_asl/proofs
Nov 15 03:53:28 Finished compiler/encoders/arm8_asl/proofs                    52m48s   5GB
Nov 15 03:53:28 Starting compiler/encoders/mips/proofs
Nov 15 04:04:08 Finished compiler/encoders/mips/proofs                        10m39s   2GB
Nov 15 04:04:08 Starting compiler/encoders/riscv/proofs
Nov 15 04:13:04 Finished compiler/encoders/riscv/proofs                        8m55s   1GB
Nov 15 04:13:04 Starting compiler/encoders/ag32/proofs
Nov 15 04:15:35 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Nov 15 04:15:35 Starting compiler/backend/x64/proofs
Nov 15 04:16:06 Finished compiler/backend/x64/proofs                             29s   2GB
Nov 15 04:16:06 Starting compiler/backend/arm7/proofs
Nov 15 04:16:37 Finished compiler/backend/arm7/proofs                            31s   1GB
Nov 15 04:16:37 Starting compiler/backend/arm8/proofs
Nov 15 04:17:06 Finished compiler/backend/arm8/proofs                            29s   1GB
Nov 15 04:17:07 Starting compiler/backend/arm8_asl
Nov 15 04:17:30 Finished compiler/backend/arm8_asl                               23s   1GB
Nov 15 04:17:30 Starting compiler/backend/mips/proofs
Nov 15 04:18:02 Finished compiler/backend/mips/proofs                            31s   2GB
Nov 15 04:18:02 Starting compiler/backend/riscv/proofs
Nov 15 04:18:37 Finished compiler/backend/riscv/proofs                           34s   2GB
Nov 15 04:18:37 Starting compiler/backend/ag32/proofs
Nov 15 04:32:19 Finished compiler/backend/ag32/proofs                         13m41s   2GB
Nov 15 04:32:19 Starting candle/set-theory
Nov 15 04:32:59 Finished candle/set-theory                                       39s   1GB
Nov 15 04:32:59 Starting candle/syntax-lib
Nov 15 04:33:01 Finished candle/syntax-lib                                        1s  21MB
Nov 15 04:33:01 Starting candle/standard/syntax
Nov 15 04:33:12 Finished candle/standard/syntax                                  10s 681MB
Nov 15 04:33:12 Starting candle/standard/semantics
Nov 15 04:35:12 Finished candle/standard/semantics                             2m00s   1GB
Nov 15 04:35:12 Starting candle/standard/monadic
Nov 15 04:35:14 Finished candle/standard/monadic                                  1s  24MB
Nov 15 04:35:14 Starting candle/standard/ml_kernel
Nov 15 04:36:57 Finished candle/standard/ml_kernel                             1m43s   3GB
Nov 15 04:36:58 Starting candle/overloading/syntax
Nov 15 04:40:22 Finished candle/overloading/syntax                             3m24s   1GB
Nov 15 04:40:22 Starting candle/overloading/semantics
Nov 15 04:52:57 Finished candle/overloading/semantics                         12m34s   2GB
Nov 15 04:52:57 Starting candle/overloading/monadic
Nov 15 04:55:41 Finished candle/overloading/monadic                            2m43s   2GB
Nov 15 04:55:41 Starting candle/overloading/ml_kernel
Nov 15 05:03:34 Finished candle/overloading/ml_kernel                          7m53s   3GB
Nov 15 05:03:35 Starting candle/overloading/ml_checker
Nov 15 05:06:09 Finished candle/overloading/ml_checker                         2m34s   3GB
Nov 15 05:06:09 Starting candle/prover
Nov 15 05:16:16 Finished candle/prover                                        10m06s   3GB
Nov 15 05:16:16 Starting pancake
Nov 15 05:17:00 Finished pancake                                                 43s 951MB
Nov 15 05:17:00 Starting pancake/ffi
Nov 15 05:17:01 Finished pancake/ffi                                              0s  13MB
Nov 15 05:17:01 Starting pancake/semantics
Nov 15 05:19:33 Finished pancake/semantics                                     2m32s   1GB
Nov 15 05:19:33 Starting pancake/parser
Nov 15 05:19:56 Finished pancake/parser                                          23s 630MB
Nov 15 05:19:56 Starting pancake/proofs
Nov 15 05:53:25 Finished pancake/proofs                                       33m28s   7GB
Nov 15 05:53:25 Starting characteristic/examples
Nov 15 05:54:54 Finished characteristic/examples                               1m28s   2GB
Nov 15 05:54:54 Starting tutorial/solutions
Nov 15 06:09:58 Finished tutorial/solutions                                   15m04s  10GB
Nov 15 06:09:59 Starting translator/monadic/examples
Nov 15 06:14:04 Finished translator/monadic/examples                           4m05s   3GB
Nov 15 06:14:04 Starting examples
Nov 17 10:25:49 Resuming examples
Nov 17 10:27:20 Finished examples                                              1m30s   2GB
Nov 17 10:27:20 Starting examples/compilation/x64
Nov 17 12:26:38 Finished examples/compilation/x64                           1h59m17s  21GB
Nov 17 12:26:38 Starting examples/compilation/x64/proofs
Nov 17 12:29:11 Finished examples/compilation/x64/proofs                       2m33s   4GB
Nov 17 12:29:11 Starting examples/compilation/ag32
Nov 17 12:59:24 Finished examples/compilation/ag32                            30m13s   9GB
Nov 17 12:59:25 Starting examples/compilation/ag32/proofs
Nov 17 13:00:27 Finished examples/compilation/ag32/proofs                      1m02s   4GB
Nov 17 13:00:27 Starting examples/compilation/to_word
Nov 17 13:04:09 Finished examples/compilation/to_word                          3m42s   7GB
Nov 17 13:04:09 Starting examples/lpr_checker
Nov 17 13:05:15 Finished examples/lpr_checker                                  1m05s   1GB
Nov 17 13:05:15 Starting examples/lpr_checker/array
Nov 17 13:42:09 Finished examples/lpr_checker/array                           36m53s   5GB
Nov 17 13:42:09 Starting examples/lpr_checker/array/compilation
Nov 17 14:30:35 Finished examples/lpr_checker/array/compilation               48m25s  22GB
Nov 17 14:30:35 Starting examples/lpr_checker/array/compilation/proofs
Nov 17 14:32:41 Finished examples/lpr_checker/array/compilation/proofs         2m06s   3GB
Nov 17 14:32:41 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 17 14:38:49 Finished examples/lpr_checker/array/compilation/proofsARM8     6m08s  21GB
Nov 17 14:38:50 Starting examples/opentheory
Nov 17 14:50:02 Finished examples/opentheory                                  11m12s   3GB
Nov 17 14:50:02 Starting examples/opentheory
Nov 17 14:50:04 Finished examples/opentheory                                      1s  29MB
Nov 17 14:50:04 Starting examples/opentheory/compilation
Nov 17 15:27:09 Finished examples/opentheory/compilation                      37m04s  30GB
Nov 17 15:27:09 Starting examples/opentheory/compilation/proofs
Nov 17 15:28:08 Finished examples/opentheory/compilation/proofs                  59s   4GB
Nov 17 15:28:08 Starting examples/opentheory/compilation/ag32
Nov 17 16:01:41 Finished examples/opentheory/compilation/ag32                 33m32s  30GB
Nov 17 16:01:41 Starting examples/opentheory/compilation/ag32/proofs
Nov 17 16:03:38 Finished examples/opentheory/compilation/ag32/proofs           1m56s   8GB
Nov 17 16:03:38 Starting examples/sat_encodings
Nov 17 16:05:40 Finished examples/sat_encodings                                2m02s   1GB
Nov 17 16:05:40 Starting examples/sat_encodings/case_studies
Nov 17 16:07:29 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Nov 17 16:07:30 Starting examples/sat_encodings/translation
Nov 17 16:13:40 Finished examples/sat_encodings/translation                    6m10s   5GB
Nov 17 16:13:40 Starting examples/sat_encodings/translation/compilation
Nov 17 17:00:06 Finished examples/sat_encodings/translation/compilation       46m25s  21GB
Nov 17 17:00:06 Starting examples/deflate
Nov 17 17:01:07 Finished examples/deflate                                      1m00s   1GB
Nov 17 17:01:07 Starting examples/deflate/translation
Nov 17 17:02:50 Finished examples/deflate/translation                          1m42s   3GB
Nov 17 17:02:50 Starting examples/deflate/translation/compilation
Nov 17 17:22:59 Finished examples/deflate/translation/compilation             20m08s  13GB
Nov 17 17:22:59 Starting examples/vipr
Nov 17 17:27:07 Finished examples/vipr                                         4m08s   4GB
Nov 17 17:27:07 Starting examples/vipr/compilation
Nov 17 17:47:54 Finished examples/vipr/compilation                            20m46s  15GB
Nov 17 17:47:54 Starting translator/okasaki-examples
Nov 17 17:53:11 Finished translator/okasaki-examples                           5m17s   1GB
Nov 17 17:53:11 Starting translator/other-examples
Nov 17 17:55:56 Finished translator/other-examples                             2m44s   1GB
Nov 17 17:55:56 Starting compiler/parsing/tests
Nov 17 17:56:28 Finished compiler/parsing/tests                                  32s 748MB
Nov 17 17:56:28 Starting compiler/inference/tests
Nov 17 18:05:01 Finished compiler/inference/tests                              8m32s   5GB
Nov 17 18:05:01 Starting compiler/printing/test
Nov 17 18:08:56 Finished compiler/printing/test                                3m54s   3GB
Nov 17 18:08:56 Starting icing/flover
Nov 17 18:53:13 Finished icing/flover                                         44m17s   2GB
Nov 17 18:53:13 Starting icing/
Nov 17 19:48:38 Finished icing/                                               55m25s   4GB
Nov 17 19:48:39 Starting icing/examples
Nov 17 19:50:14 Finished icing/examples                                        1m34s   2GB
Nov 17 19:50:14 Starting compiler/repl
Nov 17 19:59:09 Finished compiler/repl                                         8m54s   6GB
Nov 17 19:59:09 Starting unverified/sexpr-bootstrap/x64/64
Nov 17 20:12:50 Finished unverified/sexpr-bootstrap/x64/64                    13m40s  15GB
Nov 17 20:12:50 Starting unverified/sexpr-bootstrap/x64/32
Nov 17 20:23:48 Finished unverified/sexpr-bootstrap/x64/32                    10m57s  11GB
Nov 17 20:23:48 Starting compiler/benchmarks
Nov 17 20:39:31 Finished compiler/benchmarks                                  15m42s   2GB
Nov 17 20:39:31 Starting compiler/bootstrap/compilation/x64/64
Nov 18 08:45:01 Finished compiler/bootstrap/compilation/x64/64             12h05m28s  64GB
Nov 18 08:45:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 18 09:06:37 Finished compiler/bootstrap/compilation/x64/64/proofs         21m36s  28GB
Nov 18 09:06:38 Starting compiler/bootstrap/compilation/x64/32
Nov 18 16:22:34 Finished compiler/bootstrap/compilation/x64/32              7h15m55s  64GB
Nov 18 16:22:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 18 16:25:28 Finished compiler/bootstrap/compilation/x64/32/proofs          2m53s  16GB
Nov 18 16:25:28 Starting compiler/bootstrap/compilation/ag32/32
Nov 18 23:34:16 Finished compiler/bootstrap/compilation/ag32/32             7h08m47s  64GB
Nov 18 23:34:16 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 18 23:41:24 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m07s  24GB
Nov 18 23:41:24 SUCCESS