Job 1127

CakeML:9309fef75cc5ec28ddc92b105a48bd83fbe03672
  Remove a cheat and add check_thm (also add README.md) [Dec 13 00:18:34]
HOL:7838e4b6252b9d50d23ed31f3c68f01b3bca6d1a
  Fix finite_set once more [Dec 12 21:26:45]
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

Dec 16 06:26:59 Claimed job
Dec 16 06:27:03 Building HOL
Dec 16 06:38:21 Starting developers
Dec 16 06:38:25 Finished developers                                               4s  84MB
Dec 16 06:38:25 Starting developers/bin
Dec 16 06:38:32 Finished developers/bin                                           6s 960MB
Dec 16 06:38:32 Starting semantics/ffi
Dec 16 06:38:43 Finished semantics/ffi                                            9s 235MB
Dec 16 06:38:43 Starting semantics
Dec 16 06:40:13 Finished semantics                                             1m29s 820MB
Dec 16 06:40:13 Starting semantics/proofs
Dec 16 06:43:35 Finished semantics/proofs                                      3m21s 801MB
Dec 16 06:43:35 Starting semantics/alt_semantics
Dec 16 06:43:43 Finished semantics/alt_semantics                                  7s 268MB
Dec 16 06:43:43 Starting semantics/alt_semantics/proofs
Dec 16 06:45:49 Finished semantics/alt_semantics/proofs                        2m05s 779MB
Dec 16 06:45:49 Starting basis/pure
Dec 16 06:48:50 Finished basis/pure                                            3m00s 888MB
Dec 16 06:48:50 Starting translator
Dec 16 06:51:22 Finished translator                                            2m32s   1GB
Dec 16 06:51:22 Starting compiler/parsing
Dec 16 06:52:32 Finished compiler/parsing                                      1m09s   1GB
Dec 16 06:52:32 Starting characteristic
Dec 16 06:58:21 Finished characteristic                                        5m48s   1GB
Dec 16 06:58:22 Starting translator/monadic
Dec 16 06:59:56 Finished translator/monadic                                    1m34s   1GB
Dec 16 06:59:56 Starting basis
Dec 16 07:35:00 Finished basis                                                35m02s  21GB
Dec 16 07:35:00 Starting compiler/inference
Dec 16 07:36:55 Finished compiler/inference                                    1m54s   2GB
Dec 16 07:36:55 Starting compiler/backend/reg_alloc
Dec 16 07:37:58 Finished compiler/backend/reg_alloc                            1m02s   1GB
Dec 16 07:37:58 Starting compiler/backend/gc
Dec 16 07:41:25 Finished compiler/backend/gc                                   3m27s   1GB
Dec 16 07:41:25 Starting compiler/backend
Dec 16 07:45:21 Finished compiler/backend                                      3m55s   2GB
Dec 16 07:45:21 Starting compiler/encoders/asm
Dec 16 07:45:43 Finished compiler/encoders/asm                                   22s 563MB
Dec 16 07:45:43 Starting compiler/encoders/x64
Dec 16 07:46:41 Finished compiler/encoders/x64                                   57s 652MB
Dec 16 07:46:41 Starting compiler/encoders/arm7
Dec 16 07:48:29 Finished compiler/encoders/arm7                                1m48s   1GB
Dec 16 07:48:30 Starting compiler/encoders/arm8
Dec 16 07:49:04 Finished compiler/encoders/arm8                                  33s 548MB
Dec 16 07:49:04 Starting compiler/encoders/mips
Dec 16 07:50:16 Finished compiler/encoders/mips                                1m11s   1GB
Dec 16 07:50:16 Starting compiler/encoders/riscv
Dec 16 07:51:41 Finished compiler/encoders/riscv                               1m24s   1GB
Dec 16 07:51:41 Starting compiler/encoders/ag32
Dec 16 07:51:59 Finished compiler/encoders/ag32                                  17s 749MB
Dec 16 07:51:59 Starting compiler/backend/x64
Dec 16 07:52:17 Finished compiler/backend/x64                                    17s   1GB
Dec 16 07:52:17 Starting compiler/backend/arm7
Dec 16 07:52:37 Finished compiler/backend/arm7                                   19s   1GB
Dec 16 07:52:37 Starting compiler/backend/arm8
Dec 16 07:52:55 Finished compiler/backend/arm8                                   17s   1GB
Dec 16 07:52:55 Starting compiler/backend/mips
Dec 16 07:53:12 Finished compiler/backend/mips                                   16s 904MB
Dec 16 07:53:12 Starting compiler/backend/riscv
Dec 16 07:53:31 Finished compiler/backend/riscv                                  18s   1GB
Dec 16 07:53:31 Starting compiler/backend/ag32
Dec 16 07:54:42 Finished compiler/backend/ag32                                 1m11s 912MB
Dec 16 07:54:42 Starting compiler/parsing/proofs
Dec 16 08:00:30 Finished compiler/parsing/proofs                               5m47s   1GB
Dec 16 08:00:30 Starting compiler/inference/proofs
Dec 16 08:03:30 Finished compiler/inference/proofs                             2m59s   1GB
Dec 16 08:03:30 Starting compiler/backend/semantics
Dec 16 08:34:00 Finished compiler/backend/semantics                           30m30s   2GB
Dec 16 08:34:01 Starting compiler/backend/reg_alloc/proofs
Dec 16 08:37:41 Finished compiler/backend/reg_alloc/proofs                     3m39s   1GB
Dec 16 08:37:41 Starting compiler/backend/proofs
Dec 16 09:42:59 Finished compiler/backend/proofs                            1h05m16s  15GB
Dec 16 09:42:59 Starting compiler/encoders/x64/proofs
Dec 16 09:52:47 Finished compiler/encoders/x64/proofs                          9m48s   5GB
Dec 16 09:52:47 Starting compiler/encoders/arm7/proofs
Dec 16 10:06:01 Finished compiler/encoders/arm7/proofs                        13m13s   3GB
Dec 16 10:06:02 Starting compiler/encoders/arm8/proofs
Dec 16 10:12:43 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Dec 16 10:12:44 Starting compiler/encoders/mips/proofs
Dec 16 10:22:47 Finished compiler/encoders/mips/proofs                        10m03s   2GB
Dec 16 10:22:47 Starting compiler/encoders/riscv/proofs
Dec 16 10:31:50 Finished compiler/encoders/riscv/proofs                        9m02s   1GB
Dec 16 10:31:50 Starting compiler/encoders/ag32/proofs
Dec 16 10:34:31 Finished compiler/encoders/ag32/proofs                         2m40s 603MB
Dec 16 10:34:31 Starting compiler/backend/x64/proofs
Dec 16 10:34:50 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 16 10:34:50 Starting compiler/backend/arm7/proofs
Dec 16 10:35:09 Finished compiler/backend/arm7/proofs                            19s   1GB
Dec 16 10:35:09 Starting compiler/backend/arm8/proofs
Dec 16 10:35:28 Finished compiler/backend/arm8/proofs                            17s   1GB
Dec 16 10:35:28 Starting compiler/backend/mips/proofs
Dec 16 10:35:47 Finished compiler/backend/mips/proofs                            19s 844MB
Dec 16 10:35:47 Starting compiler/backend/riscv/proofs
Dec 16 10:36:07 Finished compiler/backend/riscv/proofs                           19s   1GB
Dec 16 10:36:07 Starting compiler/backend/ag32/proofs
Dec 16 10:45:48 Finished compiler/backend/ag32/proofs                          9m40s   2GB
Dec 16 10:45:48 Starting compiler/proofs
Dec 16 10:47:50 Finished compiler/proofs                                       2m01s   2GB
Dec 16 10:47:50 Starting candle/set-theory
Dec 16 10:48:18 Finished candle/set-theory                                       27s 676MB
Dec 16 10:48:19 Starting candle/syntax-lib
Dec 16 10:48:29 Finished candle/syntax-lib                                       10s 614MB
Dec 16 10:48:29 Starting candle/standard/syntax
Dec 16 10:50:19 Finished candle/standard/syntax                                1m49s 945MB
Dec 16 10:50:19 Starting candle/standard/semantics
Dec 16 10:52:02 Finished candle/standard/semantics                             1m42s   1GB
Dec 16 10:52:02 Starting candle/standard/monadic
Dec 16 10:53:43 Finished candle/standard/monadic                               1m41s   1GB
Dec 16 10:53:44 Starting candle/standard/ml_kernel
Dec 16 10:59:04 Finished candle/standard/ml_kernel                             5m19s   4GB
Dec 16 10:59:04 Starting candle/standard/opentheory
Dec 16 11:08:57 Finished candle/standard/opentheory                            9m52s   4GB
Dec 16 11:08:57 Starting candle/standard/opentheory/compilation
Dec 16 11:39:51 Finished candle/standard/opentheory/compilation               30m53s  16GB
Dec 16 11:39:51 Starting candle/standard/opentheory/compilation/proofs
Dec 16 11:40:56 Finished candle/standard/opentheory/compilation/proofs         1m05s   3GB
Dec 16 11:40:57 Starting characteristic/examples
Dec 16 11:42:29 Finished characteristic/examples                               1m31s   2GB
Dec 16 11:42:29 Starting tutorial/solutions
Dec 16 11:56:18 Finished tutorial/solutions                                   13m48s   7GB
Dec 16 11:56:18 Starting translator/monadic/examples
Dec 16 11:59:18 Finished translator/monadic/examples                           3m00s   2GB
Dec 16 11:59:18 Starting examples
Dec 16 12:08:57 Finished examples                                              9m38s   3GB
Dec 16 12:08:57 Starting examples/compilation/x64
Dec 16 14:15:51 Finished examples/compilation/x64                           2h06m53s  14GB
Dec 16 14:15:51 Starting examples/compilation/x64/proofs
Dec 16 14:17:49 Finished examples/compilation/x64/proofs                       1m57s   2GB
Dec 16 14:17:49 Starting examples/compilation/ag32
Dec 16 14:47:17 Finished examples/compilation/ag32                            29m28s   6GB
Dec 16 14:47:18 Starting examples/compilation/ag32/proofs
Dec 16 14:48:10 Finished examples/compilation/ag32/proofs                        51s   3GB
Dec 16 14:48:10 Starting examples/cost
Dec 16 15:16:48 Finished examples/cost                                        28m36s   6GB
Dec 16 15:16:48 Starting examples/lrat_checker
Dec 16 15:20:20 Finished examples/lrat_checker                                 3m31s   3GB
Dec 16 15:20:20 Starting examples/lrat_checker/compilation
Dec 16 15:36:03 Finished examples/lrat_checker/compilation                    15m42s   8GB
Dec 16 15:36:03 Starting examples/lrat_checker/compilation/proofs
Dec 16 15:36:41 Finished examples/lrat_checker/compilation/proofs                37s   3GB
Dec 16 15:36:41 Starting examples/lrat_checker/array
Dec 16 15:43:25 Finished examples/lrat_checker/array                           6m44s   2GB
Dec 16 15:43:25 Starting examples/lrat_checker/array/compilation
Dec 16 15:57:34 Finished examples/lrat_checker/array/compilation              14m08s   9GB
Dec 16 15:57:34 Starting examples/lrat_checker/array/compilation/proofs
Dec 16 15:58:22 Finished examples/lrat_checker/array/compilation/proofs          47s   2GB
Dec 16 15:58:22 Starting translator/okasaki-examples
Dec 16 16:02:41 Finished translator/okasaki-examples                           4m18s   1GB
Dec 16 16:02:42 Starting translator/other-examples
Dec 16 16:04:35 Finished translator/other-examples                             1m53s   1GB
Dec 16 16:04:35 Starting compiler/parsing/tests
Dec 16 16:05:01 Finished compiler/parsing/tests                                  25s 552MB
Dec 16 16:05:01 Starting compiler/inference/tests
Dec 16 16:09:36 Finished compiler/inference/tests                              4m34s   5GB
Dec 16 16:09:36 Starting compiler/bootstrap/translation
Dec 16 19:49:06 Finished compiler/bootstrap/translation                     3h39m27s  46GB
Dec 16 19:49:06 Starting unverified/sexpr-bootstrap/x64/64
Dec 16 20:02:53 Finished unverified/sexpr-bootstrap/x64/64                    13m46s   3GB
Dec 16 20:02:53 Starting unverified/sexpr-bootstrap/x64/32
Dec 16 20:13:01 Finished unverified/sexpr-bootstrap/x64/32                    10m06s   6GB
Dec 16 20:13:01 Starting compiler/benchmarks
Dec 16 20:13:03 Finished compiler/benchmarks                                      2s  27MB
Dec 16 20:13:03 Starting compiler/bootstrap/compilation/x64/64
Dec 17 09:27:32 Finished compiler/bootstrap/compilation/x64/64             13h14m27s  64GB
Dec 17 09:27:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 17 09:31:12 Finished compiler/bootstrap/compilation/x64/64/proofs          3m39s   5GB
Dec 17 09:31:12 Starting compiler/bootstrap/compilation/x64/32
Dec 17 21:54:23 Finished compiler/bootstrap/compilation/x64/32             12h23m09s  64GB
Dec 17 21:54:23 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 17 21:58:04 Finished compiler/bootstrap/compilation/x64/32/proofs          3m41s   4GB
Dec 17 21:58:05 Starting compiler/bootstrap/compilation/ag32/32
Dec 18 11:04:32 Finished compiler/bootstrap/compilation/ag32/32            13h06m26s  64GB
Dec 18 11:04:32 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 18 11:35:03 Finished compiler/bootstrap/compilation/ag32/32/proofs        30m30s  18GB
Dec 18 11:35:03 SUCCESS