Job 2233

CakeML:7101a3f2e0c3885412c05e63735ec6da155253ee
  Fix for adjusted Inductive syntax [Nov 08 21:36:03]
HOL:be29184419aaa27f96bbbf8fb1b90d0e40385c33
  [emacs-mode] Handle new Inductive label syntaxes [Nov 08 03:19:35]
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 09 09:55:31 Claimed job
Nov 09 09:55:35 Building HOL
Nov 09 10:10:42 Starting developers
Nov 09 10:10:48 Finished developers                                               5s 130MB
Nov 09 10:10:48 Starting developers/bin
Nov 09 10:10:55 Finished developers/bin                                           6s   1GB
Nov 09 10:10:55 Starting compiler/proofs
Nov 09 12:07:18 Finished compiler/proofs                                    1h56m23s  20GB
Nov 09 12:07:18 Starting compiler/bootstrap/translation
Nov 09 21:01:47 Finished compiler/bootstrap/translation                     8h54m28s  36GB
Nov 09 21:01:47 Starting semantics/ffi
Nov 09 21:01:53 Finished semantics/ffi                                            6s 216MB
Nov 09 21:01:53 Starting semantics
Nov 09 21:01:55 Finished semantics                                                1s  19MB
Nov 09 21:01:55 Starting semantics/proofs
Nov 09 21:02:30 Finished semantics/proofs                                        35s   1GB
Nov 09 21:02:30 Starting semantics/alt_semantics
Nov 09 21:03:03 Finished semantics/alt_semantics                                 32s 837MB
Nov 09 21:03:03 Starting semantics/alt_semantics/proofs
Nov 09 21:15:09 Finished semantics/alt_semantics/proofs                       12m06s   2GB
Nov 09 21:15:09 Starting basis/pure
Nov 09 21:15:11 Finished basis/pure                                               1s  23MB
Nov 09 21:15:11 Starting translator
Nov 09 21:17:05 Finished translator                                            1m53s   1GB
Nov 09 21:17:05 Starting compiler/parsing
Nov 09 21:17:07 Finished compiler/parsing                                         1s  22MB
Nov 09 21:17:07 Starting characteristic
Nov 09 21:17:09 Finished characteristic                                           1s  23MB
Nov 09 21:17:09 Starting translator/monadic
Nov 09 21:17:11 Finished translator/monadic                                       1s  24MB
Nov 09 21:17:11 Starting basis
Nov 09 21:21:20 Finished basis                                                 4m09s   3GB
Nov 09 21:21:20 Starting compiler/inference
Nov 09 21:21:22 Finished compiler/inference                                       1s  19MB
Nov 09 21:21:22 Starting compiler/backend/reg_alloc
Nov 09 21:21:24 Finished compiler/backend/reg_alloc                               1s  24MB
Nov 09 21:21:24 Starting compiler/backend/gc
Nov 09 21:21:26 Finished compiler/backend/gc                                      2s  24MB
Nov 09 21:21:26 Starting compiler/backend
Nov 09 21:21:39 Finished compiler/backend                                        12s 823MB
Nov 09 21:21:39 Starting compiler/encoders/asm
Nov 09 21:21:41 Finished compiler/encoders/asm                                    1s  23MB
Nov 09 21:21:41 Starting compiler/encoders/x64
Nov 09 21:21:43 Finished compiler/encoders/x64                                    1s  23MB
Nov 09 21:21:43 Starting compiler/encoders/arm7
Nov 09 21:21:45 Finished compiler/encoders/arm7                                   1s  19MB
Nov 09 21:21:45 Starting compiler/encoders/arm8
Nov 09 21:21:47 Finished compiler/encoders/arm8                                   1s  21MB
Nov 09 21:21:47 Starting compiler/encoders/arm8_asl
Nov 10 00:10:46 Finished compiler/encoders/arm8_asl                         2h48m58s  36GB
Nov 10 00:10:46 Starting compiler/encoders/mips
Nov 10 00:10:48 Finished compiler/encoders/mips                                   1s  17MB
Nov 10 00:10:48 Starting compiler/encoders/riscv
Nov 10 00:10:50 Finished compiler/encoders/riscv                                  1s  23MB
Nov 10 00:10:50 Starting compiler/encoders/ag32
Nov 10 00:10:52 Finished compiler/encoders/ag32                                   1s  19MB
Nov 10 00:10:52 Starting compiler/backend/x64
Nov 10 00:10:54 Finished compiler/backend/x64                                     2s  22MB
Nov 10 00:10:55 Starting compiler/backend/arm7
Nov 10 00:10:57 Finished compiler/backend/arm7                                    2s  27MB
Nov 10 00:10:57 Starting compiler/backend/arm8
Nov 10 00:10:59 Finished compiler/backend/arm8                                    2s  23MB
Nov 10 00:10:59 Starting compiler/backend/mips
Nov 10 00:11:01 Finished compiler/backend/mips                                    2s  27MB
Nov 10 00:11:02 Starting compiler/backend/riscv
Nov 10 00:11:04 Finished compiler/backend/riscv                                   2s  26MB
Nov 10 00:11:04 Starting compiler/backend/ag32
Nov 10 00:12:28 Finished compiler/backend/ag32                                 1m24s   1GB
Nov 10 00:12:28 Starting compiler/parsing/proofs
Nov 10 00:12:30 Finished compiler/parsing/proofs                                  1s  20MB
Nov 10 00:12:30 Starting compiler/inference/proofs
Nov 10 00:12:32 Finished compiler/inference/proofs                                1s  25MB
Nov 10 00:12:32 Starting compiler/backend/semantics
Nov 10 00:13:45 Finished compiler/backend/semantics                            1m12s   1GB
Nov 10 00:13:45 Starting compiler/backend/reg_alloc/proofs
Nov 10 00:13:47 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Nov 10 00:13:47 Starting compiler/backend/proofs
Nov 10 00:14:49 Finished compiler/backend/proofs                               1m01s   3GB
Nov 10 00:14:49 Starting compiler/backend/serialiser
Nov 10 00:14:52 Finished compiler/backend/serialiser                              2s  32MB
Nov 10 00:14:52 Starting compiler/encoders/x64/proofs
Nov 10 00:24:39 Finished compiler/encoders/x64/proofs                          9m46s   5GB
Nov 10 00:24:39 Starting compiler/encoders/arm7/proofs
Nov 10 00:38:36 Finished compiler/encoders/arm7/proofs                        13m57s   3GB
Nov 10 00:38:36 Starting compiler/encoders/arm8/proofs
Nov 10 00:45:41 Finished compiler/encoders/arm8/proofs                         7m04s   1GB
Nov 10 00:45:41 Starting compiler/encoders/arm8_asl/proofs
Nov 10 01:38:17 Finished compiler/encoders/arm8_asl/proofs                    52m35s   6GB
Nov 10 01:38:17 Starting compiler/encoders/mips/proofs
Nov 10 01:48:41 Finished compiler/encoders/mips/proofs                        10m23s   2GB
Nov 10 01:48:41 Starting compiler/encoders/riscv/proofs
Nov 10 01:57:43 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Nov 10 01:57:43 Starting compiler/encoders/ag32/proofs
Nov 10 02:00:13 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Nov 10 02:00:13 Starting compiler/backend/x64/proofs
Nov 10 02:00:44 Finished compiler/backend/x64/proofs                             31s   2GB
Nov 10 02:00:44 Starting compiler/backend/arm7/proofs
Nov 10 02:01:16 Finished compiler/backend/arm7/proofs                            32s   2GB
Nov 10 02:01:16 Starting compiler/backend/arm8/proofs
Nov 10 02:01:47 Finished compiler/backend/arm8/proofs                            30s   1GB
Nov 10 02:01:47 Starting compiler/backend/arm8_asl
Nov 10 02:02:11 Finished compiler/backend/arm8_asl                               23s   1GB
Nov 10 02:02:11 Starting compiler/backend/mips/proofs
Nov 10 02:02:43 Finished compiler/backend/mips/proofs                            32s   2GB
Nov 10 02:02:43 Starting compiler/backend/riscv/proofs
Nov 10 02:03:18 Finished compiler/backend/riscv/proofs                           34s   2GB
Nov 10 02:03:18 Starting compiler/backend/ag32/proofs
Nov 10 02:17:03 Finished compiler/backend/ag32/proofs                         13m44s   2GB
Nov 10 02:17:03 Starting candle/set-theory
Nov 10 02:17:43 Finished candle/set-theory                                       39s   1GB
Nov 10 02:17:43 Starting candle/syntax-lib
Nov 10 02:17:44 Finished candle/syntax-lib                                        1s  18MB
Nov 10 02:17:44 Starting candle/standard/syntax
Nov 10 02:17:55 Finished candle/standard/syntax                                  10s 712MB
Nov 10 02:17:55 Starting candle/standard/semantics
Nov 10 02:19:53 Finished candle/standard/semantics                             1m57s   1GB
Nov 10 02:19:53 Starting candle/standard/monadic
Nov 10 02:19:55 Finished candle/standard/monadic                                  1s  26MB
Nov 10 02:19:55 Starting candle/standard/ml_kernel
Nov 10 02:21:35 Finished candle/standard/ml_kernel                             1m39s   3GB
Nov 10 02:21:35 Starting candle/overloading/syntax
Nov 10 02:24:58 Finished candle/overloading/syntax                             3m22s   1GB
Nov 10 02:24:58 Starting candle/overloading/semantics
Nov 10 02:37:27 Finished candle/overloading/semantics                         12m28s   2GB
Nov 10 02:37:27 Starting candle/overloading/monadic
Nov 10 02:40:11 Finished candle/overloading/monadic                            2m43s   2GB
Nov 10 02:40:11 Starting candle/overloading/ml_kernel
Nov 10 02:48:07 Finished candle/overloading/ml_kernel                          7m56s   3GB
Nov 10 02:48:08 Starting candle/overloading/ml_checker
Nov 10 02:51:12 Finished candle/overloading/ml_checker                         3m03s   2GB
Nov 10 02:51:12 Starting candle/prover
Nov 10 03:01:12 Finished candle/prover                                         9m59s   3GB
Nov 10 03:01:12 Starting pancake
Nov 10 03:01:55 Finished pancake                                                 43s 876MB
Nov 10 03:01:55 Starting pancake/ffi
Nov 10 03:01:56 Finished pancake/ffi                                              0s  13MB
Nov 10 03:01:56 Starting pancake/semantics
Nov 10 03:04:24 Finished pancake/semantics                                     2m27s   1GB
Nov 10 03:04:24 Starting pancake/parser
Nov 10 03:04:46 Finished pancake/parser                                          22s   1GB
Nov 10 03:04:47 Starting pancake/proofs
Nov 10 03:38:21 Finished pancake/proofs                                       33m34s   4GB
Nov 10 03:38:21 Starting characteristic/examples
Nov 10 03:40:01 Finished characteristic/examples                               1m39s   3GB
Nov 10 03:40:01 Starting tutorial/solutions
Nov 10 03:55:17 Finished tutorial/solutions                                   15m16s  11GB
Nov 10 03:55:17 Starting translator/monadic/examples
Nov 10 03:59:26 Finished translator/monadic/examples                           4m08s   2GB
Nov 10 03:59:26 Starting examples
Nov 10 04:15:29 Finished examples                                             16m03s   5GB
Nov 10 04:15:29 Starting examples/compilation/x64
Nov 10 06:16:04 Finished examples/compilation/x64                           2h00m34s  18GB
Nov 10 06:16:04 Starting examples/compilation/x64/proofs
Nov 10 06:18:39 Finished examples/compilation/x64/proofs                       2m35s   4GB
Nov 10 06:18:39 Starting examples/compilation/ag32
Nov 10 06:48:29 Finished examples/compilation/ag32                            29m49s  10GB
Nov 10 06:48:29 Starting examples/compilation/ag32/proofs
Nov 10 06:49:31 Finished examples/compilation/ag32/proofs                      1m01s   4GB
Nov 10 06:49:31 Starting examples/compilation/to_word
Nov 10 06:52:57 Finished examples/compilation/to_word                          3m26s   7GB
Nov 10 06:52:57 Starting examples/lpr_checker
Nov 10 06:54:03 Finished examples/lpr_checker                                  1m05s   1GB
Nov 10 06:54:03 Starting examples/lpr_checker/array
Nov 10 07:31:18 Finished examples/lpr_checker/array                           37m14s   9GB
Nov 10 07:31:18 Starting examples/lpr_checker/array/compilation
Nov 10 08:24:12 Finished examples/lpr_checker/array/compilation               52m53s  24GB
Nov 10 08:24:12 Starting examples/lpr_checker/array/compilation/proofs
Nov 10 08:26:39 Finished examples/lpr_checker/array/compilation/proofs         2m27s   3GB
Nov 10 08:26:39 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 10 08:32:47 Finished examples/lpr_checker/array/compilation/proofsARM8     6m07s  21GB
Nov 10 08:32:47 Starting examples/opentheory
Nov 10 08:43:39 Finished examples/opentheory                                  10m51s   5GB
Nov 10 08:43:39 Starting examples/opentheory
Nov 10 08:43:41 Finished examples/opentheory                                      1s  26MB
Nov 10 08:43:41 Starting examples/opentheory/compilation
Nov 10 09:21:39 Finished examples/opentheory/compilation                      37m58s  35GB
Nov 10 09:21:39 Starting examples/opentheory/compilation/proofs
Nov 10 09:22:40 Finished examples/opentheory/compilation/proofs                1m01s   5GB
Nov 10 09:22:40 Starting examples/opentheory/compilation/ag32
Nov 10 09:55:34 Finished examples/opentheory/compilation/ag32                 32m53s  31GB
Nov 10 09:55:34 Starting examples/opentheory/compilation/ag32/proofs
Nov 10 09:57:28 Finished examples/opentheory/compilation/ag32/proofs           1m54s   7GB
Nov 10 09:57:28 Starting examples/sat_encodings
Nov 10 09:59:31 Finished examples/sat_encodings                                2m02s   1GB
Nov 10 09:59:31 Starting examples/sat_encodings/case_studies
Nov 10 10:01:15 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Nov 10 10:01:15 Starting examples/sat_encodings/translation
Nov 10 10:07:19 Finished examples/sat_encodings/translation                    6m03s   4GB
Nov 10 10:07:19 Starting examples/sat_encodings/translation/compilation
Nov 10 10:52:51 Finished examples/sat_encodings/translation/compilation       45m32s  20GB
Nov 10 10:52:51 Starting examples/deflate
Nov 10 10:53:53 Finished examples/deflate                                      1m01s 990MB
Nov 10 10:53:53 Starting examples/deflate/translation
Nov 10 10:55:43 Finished examples/deflate/translation                          1m50s   3GB
Nov 10 10:55:43 Starting examples/deflate/translation/compilation
Nov 10 11:15:55 Finished examples/deflate/translation/compilation             20m11s  13GB
Nov 10 11:15:55 Starting examples/vipr
Nov 10 11:20:05 Finished examples/vipr                                         4m09s   5GB
Nov 10 11:20:05 Starting examples/vipr/compilation
Nov 10 11:40:32 Finished examples/vipr/compilation                            20m26s  16GB
Nov 10 11:40:32 Starting translator/okasaki-examples
Nov 10 11:45:43 Finished translator/okasaki-examples                           5m10s   1GB
Nov 10 11:45:43 Starting translator/other-examples
Nov 10 11:48:27 Finished translator/other-examples                             2m44s   1GB
Nov 10 11:48:27 Starting compiler/parsing/tests
Nov 10 11:48:59 Finished compiler/parsing/tests                                  31s 761MB
Nov 10 11:48:59 Starting compiler/inference/tests
Nov 10 11:57:23 Finished compiler/inference/tests                              8m23s   6GB
Nov 10 11:57:23 Starting compiler/printing/test
Nov 10 12:01:22 Finished compiler/printing/test                                3m58s   3GB
Nov 10 12:01:22 Starting icing/flover
Nov 10 12:45:15 Finished icing/flover                                         43m52s   2GB
Nov 10 12:45:15 Starting icing/
Nov 10 13:40:54 Finished icing/                                               55m39s   7GB
Nov 10 13:40:54 Starting icing/examples
Nov 10 13:42:28 Finished icing/examples                                        1m33s   3GB
Nov 10 13:42:28 Starting compiler/repl
Nov 10 13:51:12 Finished compiler/repl                                         8m43s   6GB
Nov 10 13:51:12 Starting unverified/sexpr-bootstrap/x64/64
Nov 10 14:04:49 Finished unverified/sexpr-bootstrap/x64/64                    13m36s  17GB
Nov 10 14:04:49 Starting unverified/sexpr-bootstrap/x64/32
Nov 10 14:16:01 Finished unverified/sexpr-bootstrap/x64/32                    11m11s  14GB
Nov 10 14:16:01 Starting compiler/benchmarks
Nov 10 14:31:41 Finished compiler/benchmarks                                  15m39s   2GB
Nov 10 14:31:41 Starting compiler/bootstrap/compilation/x64/64
Nov 11 02:54:17 Finished compiler/bootstrap/compilation/x64/64             12h22m35s  64GB
Nov 11 02:54:17 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 11 03:14:42 Finished compiler/bootstrap/compilation/x64/64/proofs         20m24s  27GB
Nov 11 03:14:42 Starting compiler/bootstrap/compilation/x64/32
Nov 11 10:31:23 Finished compiler/bootstrap/compilation/x64/32              7h16m40s  64GB
Nov 11 10:31:23 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 11 10:34:47 Finished compiler/bootstrap/compilation/x64/32/proofs          3m24s  18GB
Nov 11 10:34:48 Starting compiler/bootstrap/compilation/ag32/32
Nov 11 18:13:58 Finished compiler/bootstrap/compilation/ag32/32             7h39m09s  64GB
Nov 11 18:13:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 11 18:27:38 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m40s  22GB
Nov 11 18:27:39 SUCCESS