Job 1804

CakeML:f18f45a1f5d90a31c62adc297d68971f6e948c43
  Fix following change in Define in HOL [Feb 25 21:10:34]
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern [Feb 25 06:46:55]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 26 03:00:02 Claimed job
Feb 26 03:00:06 Reusing HOL
Feb 26 03:00:45 Starting developers
Feb 26 03:00:50 Finished developers                                               4s  99MB
Feb 26 03:00:50 Starting developers/bin
Feb 26 03:00:56 Finished developers/bin                                           5s 670MB
Feb 26 03:00:56 Starting semantics/ffi
Feb 26 03:01:07 Finished semantics/ffi                                           11s 221MB
Feb 26 03:01:07 Starting semantics
Feb 26 03:03:27 Finished semantics                                             2m19s   1GB
Feb 26 03:03:27 Starting semantics/proofs
Feb 26 03:07:38 Finished semantics/proofs                                      4m11s 883MB
Feb 26 03:07:38 Starting semantics/alt_semantics
Feb 26 03:07:57 Finished semantics/alt_semantics                                 18s 500MB
Feb 26 03:07:57 Starting semantics/alt_semantics/proofs
Feb 26 03:10:44 Finished semantics/alt_semantics/proofs                        2m46s 740MB
Feb 26 03:10:44 Starting basis/pure
Feb 26 03:11:53 Finished basis/pure                                            1m08s   1GB
Feb 26 03:11:53 Starting translator
Feb 26 03:15:30 Finished translator                                            3m36s   1GB
Feb 26 03:15:30 Starting compiler/parsing
Feb 26 03:17:06 Finished compiler/parsing                                      1m35s   2GB
Feb 26 03:17:06 Starting characteristic
Feb 26 03:24:06 Finished characteristic                                        7m00s   2GB
Feb 26 03:24:06 Starting translator/monadic
Feb 26 03:26:14 Finished translator/monadic                                    2m05s   1GB
Feb 26 03:26:14 Starting basis
Feb 26 04:24:02 Finished basis                                                57m47s   3GB
Feb 26 04:24:02 Starting compiler/inference
Feb 26 04:25:35 Finished compiler/inference                                    1m32s   1GB
Feb 26 04:25:35 Starting compiler/backend/reg_alloc
Feb 26 04:27:39 Finished compiler/backend/reg_alloc                            2m02s   1GB
Feb 26 04:27:39 Starting compiler/backend/gc
Feb 26 04:33:13 Finished compiler/backend/gc                                   5m33s   1GB
Feb 26 04:33:13 Starting compiler/backend
Feb 26 04:40:36 Finished compiler/backend                                      7m22s   2GB
Feb 26 04:40:37 Starting compiler/encoders/asm
Feb 26 04:41:12 Finished compiler/encoders/asm                                   34s   1GB
Feb 26 04:41:12 Starting compiler/encoders/x64
Feb 26 04:41:46 Finished compiler/encoders/x64                                   33s   1GB
Feb 26 04:41:46 Starting compiler/encoders/arm7
Feb 26 04:42:48 Finished compiler/encoders/arm7                                1m01s 919MB
Feb 26 04:42:48 Starting compiler/encoders/arm8
Feb 26 04:43:08 Finished compiler/encoders/arm8                                  19s 774MB
Feb 26 04:43:08 Starting compiler/encoders/arm8_asl
Feb 26 04:46:17 Finished compiler/encoders/arm8_asl                            3m09s 924MB
Feb 26 04:46:17 Starting compiler/encoders/mips
Feb 26 04:46:43 Finished compiler/encoders/mips                                  25s 865MB
Feb 26 04:46:43 Starting compiler/encoders/riscv
Feb 26 04:47:05 Finished compiler/encoders/riscv                                 22s 842MB
Feb 26 04:47:05 Starting compiler/encoders/ag32
Feb 26 04:47:31 Finished compiler/encoders/ag32                                  25s 732MB
Feb 26 04:47:31 Starting compiler/backend/x64
Feb 26 04:47:56 Finished compiler/backend/x64                                    25s   1GB
Feb 26 04:47:56 Starting compiler/backend/arm7
Feb 26 04:48:24 Finished compiler/backend/arm7                                   27s   1GB
Feb 26 04:48:24 Starting compiler/backend/arm8
Feb 26 04:48:50 Finished compiler/backend/arm8                                   25s   1GB
Feb 26 04:48:50 Starting compiler/backend/mips
Feb 26 04:49:17 Finished compiler/backend/mips                                   26s   1GB
Feb 26 04:49:17 Starting compiler/backend/riscv
Feb 26 04:49:43 Finished compiler/backend/riscv                                  25s   1GB
Feb 26 04:49:43 Starting compiler/backend/ag32
Feb 26 04:51:26 Finished compiler/backend/ag32                                 1m42s   1GB
Feb 26 04:51:26 Starting compiler/parsing/proofs
Feb 26 04:56:09 Finished compiler/parsing/proofs                               4m42s   1GB
Feb 26 04:56:09 Starting compiler/inference/proofs
Feb 26 04:59:31 Finished compiler/inference/proofs                             3m21s 957MB
Feb 26 04:59:31 Starting compiler/backend/semantics
Feb 26 05:41:24 Finished compiler/backend/semantics                           41m51s   1GB
Feb 26 05:41:24 Starting compiler/backend/reg_alloc/proofs
Feb 26 05:45:52 Finished compiler/backend/reg_alloc/proofs                     4m27s 619MB
Feb 26 05:45:53 Starting compiler/backend/proofs
Feb 26 06:58:45 Finished compiler/backend/proofs                            1h12m52s   7GB
Feb 26 06:58:46 Starting compiler/backend/serialiser
Feb 26 07:00:36 Finished compiler/backend/serialiser                           1m50s   2GB
Feb 26 07:00:37 Starting compiler/encoders/x64/proofs
Feb 26 07:12:38 Finished compiler/encoders/x64/proofs                         12m00s   1GB
Feb 26 07:12:38 Starting compiler/encoders/arm7/proofs
Feb 26 07:27:32 Finished compiler/encoders/arm7/proofs                        14m54s   4GB
Feb 26 07:27:32 Starting compiler/encoders/arm8/proofs
Feb 26 07:34:58 Finished compiler/encoders/arm8/proofs                         7m25s   1GB
Feb 26 07:34:58 Starting compiler/encoders/arm8_asl/proofs
Feb 26 07:52:10 Finished compiler/encoders/arm8_asl/proofs                    17m11s   2GB
Feb 26 07:52:10 Starting compiler/encoders/mips/proofs
Feb 26 08:03:40 Finished compiler/encoders/mips/proofs                        11m29s   2GB
Feb 26 08:03:41 Starting compiler/encoders/riscv/proofs
Feb 26 08:14:13 Finished compiler/encoders/riscv/proofs                       10m31s 975MB
Feb 26 08:14:13 Starting compiler/encoders/ag32/proofs
Feb 26 08:17:26 Finished compiler/encoders/ag32/proofs                         3m12s 517MB
Feb 26 08:17:26 Starting compiler/backend/x64/proofs
Feb 26 08:18:18 Finished compiler/backend/x64/proofs                             51s 942MB
Feb 26 08:18:18 Starting compiler/backend/arm7/proofs
Feb 26 08:18:50 Finished compiler/backend/arm7/proofs                            31s   1GB
Feb 26 08:18:50 Starting compiler/backend/arm8/proofs
Feb 26 08:19:21 Finished compiler/backend/arm8/proofs                            30s   1GB
Feb 26 08:19:21 Starting compiler/backend/arm8_asl
Feb 26 08:19:47 Finished compiler/backend/arm8_asl                               26s   1GB
Feb 26 08:19:48 Starting compiler/backend/mips/proofs
Feb 26 08:20:21 Finished compiler/backend/mips/proofs                            33s   1GB
Feb 26 08:20:21 Starting compiler/backend/riscv/proofs
Feb 26 08:20:55 Finished compiler/backend/riscv/proofs                           33s   1GB
Feb 26 08:20:55 Starting compiler/backend/ag32/proofs
Feb 26 08:37:51 Finished compiler/backend/ag32/proofs                         16m55s   2GB
Feb 26 08:37:51 Starting compiler/proofs
Feb 26 08:40:30 Finished compiler/proofs                                       2m38s   3GB
Feb 26 08:40:30 Starting candle/set-theory
Feb 26 08:41:14 Finished candle/set-theory                                       43s 970MB
Feb 26 08:41:14 Starting candle/syntax-lib
Feb 26 08:41:30 Finished candle/syntax-lib                                       15s 551MB
Feb 26 08:41:31 Starting candle/standard/syntax
Feb 26 08:44:03 Finished candle/standard/syntax                                2m32s   1GB
Feb 26 08:44:03 Starting candle/standard/semantics
Feb 26 08:46:20 Finished candle/standard/semantics                             2m16s   1GB
Feb 26 08:46:20 Starting candle/standard/monadic
Feb 26 08:48:47 Finished candle/standard/monadic                               2m27s   1GB
Feb 26 08:48:48 Starting candle/standard/ml_kernel
Feb 26 08:57:11 Finished candle/standard/ml_kernel                             8m23s   2GB
Feb 26 08:57:12 Starting candle/overloading/syntax
Feb 26 09:01:10 Finished candle/overloading/syntax                             3m57s   1GB
Feb 26 09:01:10 Starting candle/overloading/semantics
Feb 26 09:14:49 Finished candle/overloading/semantics                         13m37s   2GB
Feb 26 09:14:49 Starting candle/overloading/monadic
Feb 26 09:17:49 Finished candle/overloading/monadic                            2m59s   1GB
Feb 26 09:17:49 Starting candle/overloading/ml_kernel
Feb 26 09:26:13 Finished candle/overloading/ml_kernel                          8m24s   3GB
Feb 26 09:26:13 Starting candle/overloading/ml_checker
Feb 26 09:28:55 Finished candle/overloading/ml_checker                         2m41s   3GB
Feb 26 09:28:55 Starting candle/prover
Feb 26 09:37:17 Finished candle/prover                                         8m21s   3GB
Feb 26 09:37:18 Starting pancake
Feb 26 09:40:24 Finished pancake                                               3m06s   3GB
Feb 26 09:40:24 Starting pancake/ffi
Feb 26 09:40:25 Finished pancake/ffi                                              0s  31MB
Feb 26 09:40:25 Starting pancake/semantics
Feb 26 09:43:23 Finished pancake/semantics                                     2m58s   1GB
Feb 26 09:43:24 Starting pancake/proofs
Feb 26 09:57:49 Finished pancake/proofs                                       14m25s   5GB
Feb 26 09:57:49 Starting characteristic/examples
Feb 26 09:59:30 Finished characteristic/examples                               1m40s   2GB
Feb 26 09:59:30 Starting tutorial/solutions
Feb 26 10:18:21 Finished tutorial/solutions                                   18m49s  12GB
Feb 26 10:18:21 Starting translator/monadic/examples
Feb 26 10:23:21 Finished translator/monadic/examples                           4m59s   3GB
Feb 26 10:23:21 Starting examples
Feb 26 10:36:06 Finished examples                                             12m45s   3GB
Feb 26 10:36:07 Starting examples/compilation/x64
Feb 26 13:31:11 Finished examples/compilation/x64                           2h55m02s  19GB
Feb 26 13:31:11 Starting examples/compilation/x64/proofs
Feb 26 13:34:30 Finished examples/compilation/x64/proofs                       3m18s   3GB
Feb 26 13:34:30 Starting examples/compilation/ag32
Feb 26 14:15:45 Finished examples/compilation/ag32                            41m14s   9GB
Feb 26 14:15:45 Starting examples/compilation/ag32/proofs
Feb 26 14:17:01 Finished examples/compilation/ag32/proofs                      1m15s   3GB
Feb 26 14:17:01 Starting examples/cost
Feb 26 15:32:35 Finished examples/cost                                      1h15m32s   7GB
Feb 26 15:32:35 Starting examples/lpr_checker
Feb 26 15:33:44 Finished examples/lpr_checker                                  1m08s 992MB
Feb 26 15:33:44 Starting examples/lpr_checker/array
Feb 26 16:07:50 Finished examples/lpr_checker/array                           34m06s   4GB
Feb 26 16:07:51 Starting examples/lpr_checker/array/compilation
Feb 26 17:59:48 Finished examples/lpr_checker/array/compilation             1h51m54s  11GB
Feb 26 17:59:48 Starting examples/lpr_checker/array/compilation/proofs
Feb 26 18:02:15 Finished examples/lpr_checker/array/compilation/proofs         2m26s   3GB
Feb 26 18:02:15 Starting examples/opentheory
Feb 26 18:14:55 Finished examples/opentheory                                  12m40s   4GB
Feb 26 18:14:55 Starting examples/opentheory
Feb 26 18:14:57 Finished examples/opentheory                                      1s  24MB
Feb 26 18:14:57 Starting examples/opentheory/compilation
Feb 26 19:04:44 Finished examples/opentheory/compilation                      49m44s  18GB
Feb 26 19:04:44 Starting examples/opentheory/compilation/proofs
Feb 26 19:06:03 Finished examples/opentheory/compilation/proofs                1m18s   3GB
Feb 26 19:06:03 Starting examples/opentheory/compilation/ag32
Feb 26 19:57:17 Finished examples/opentheory/compilation/ag32                 51m13s   9GB
Feb 26 19:57:17 Starting examples/opentheory/compilation/ag32/proofs
Feb 26 19:59:14 Finished examples/opentheory/compilation/ag32/proofs           1m56s   6GB
Feb 26 19:59:14 Starting examples/sat_encodings
Feb 26 20:01:28 Finished examples/sat_encodings                                2m13s   1GB
Feb 26 20:01:28 Starting examples/sat_encodings/case_studies
Feb 26 20:03:26 Finished examples/sat_encodings/case_studies                   1m58s 874MB
Feb 26 20:03:26 Starting examples/sat_encodings/translation
Feb 26 20:10:35 Finished examples/sat_encodings/translation                    7m08s   3GB
Feb 26 20:10:35 Starting examples/sat_encodings/translation/compilation
Feb 26 21:19:41 Finished examples/sat_encodings/translation/compilation     1h09m05s   8GB
Feb 26 21:19:41 Starting translator/okasaki-examples
Feb 26 21:25:59 Finished translator/okasaki-examples                           6m17s   1GB
Feb 26 21:26:00 Starting translator/other-examples
Feb 26 21:28:41 Finished translator/other-examples                             2m40s   1GB
Feb 26 21:28:41 Starting compiler/parsing/tests
Feb 26 21:29:17 Finished compiler/parsing/tests                                  36s 575MB
Feb 26 21:29:18 Starting compiler/inference/tests
Feb 26 21:38:46 Finished compiler/inference/tests                              9m27s   3GB
Feb 26 21:38:46 Starting compiler/bootstrap/translation
Feb 27 00:54:09 Finished compiler/bootstrap/translation                     3h15m22s  12GB
Feb 27 00:54:09 Starting unverified/sexpr-bootstrap/x64/64
Feb 27 01:05:01 Finished unverified/sexpr-bootstrap/x64/64                    10m47s   8GB
Feb 27 01:05:01 Starting unverified/sexpr-bootstrap/x64/32
Feb 27 01:13:58 Finished unverified/sexpr-bootstrap/x64/32                     8m53s   8GB
Feb 27 01:13:58 Starting compiler/benchmarks
Feb 27 01:14:01 Finished compiler/benchmarks                                      2s  32MB
Feb 27 01:14:01 Starting compiler/bootstrap/compilation/x64/64
Feb 27 21:13:59 Finished compiler/bootstrap/compilation/x64/64             19h59m54s  34GB
Feb 27 21:13:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 27 21:18:29 Finished compiler/bootstrap/compilation/x64/64/proofs          4m29s  14GB
Feb 27 21:18:30 Starting compiler/bootstrap/compilation/x64/32
Feb 28 14:14:45 Finished compiler/bootstrap/compilation/x64/32             16h56m12s  28GB
Feb 28 14:14:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 28 14:18:55 Finished compiler/bootstrap/compilation/x64/32/proofs          4m09s  13GB
Feb 28 14:18:55 Starting compiler/bootstrap/compilation/ag32/32
Mar 01 08:07:22 Finished compiler/bootstrap/compilation/ag32/32            17h48m27s  30GB
Mar 01 08:07:23 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 01 08:35:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        28m31s  21GB
Mar 01 08:35:55 SUCCESS