Job 1555

CakeML:76ed0b05089a77059dee72d197fc56c3dae661e8
  Merge pull request #829 from CakeML/help [Jun 18 08:39:57]
HOL:ce49c6542adf54f809665caba71e33707dcddda8
  Prove little lemma about being a subset of a singleton [Jul 21 04:25:15]
Machine:oven3 4.19.67.1.amd64-smp
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jul 23 16:01:18 Claimed job
Jul 23 16:01:30 Building HOL
Jul 23 16:34:03 Starting developers
Jul 23 16:34:11 Finished developers                                               7s 139MB
Jul 23 16:34:11 Starting developers/bin
Jul 23 16:34:23 Finished developers/bin                                          12s   1GB
Jul 23 16:34:23 Starting semantics/ffi
Jul 23 16:34:49 Finished semantics/ffi                                           25s 280MB
Jul 23 16:34:49 Starting semantics
Jul 23 16:37:59 Finished semantics                                             3m09s   1GB
Jul 23 16:37:59 Starting semantics/proofs
Jul 23 16:45:43 Finished semantics/proofs                                      7m43s   1GB
Jul 23 16:45:43 Starting semantics/alt_semantics
Jul 23 16:46:05 Finished semantics/alt_semantics                                 22s 343MB
Jul 23 16:46:06 Starting semantics/alt_semantics/proofs
Jul 23 16:50:58 Finished semantics/alt_semantics/proofs                        4m52s 935MB
Jul 23 16:50:58 Starting basis/pure
Jul 23 16:57:13 Finished basis/pure                                            6m14s 828MB
Jul 23 16:57:13 Starting translator
Jul 23 17:04:06 Finished translator                                            6m52s   1GB
Jul 23 17:04:06 Starting compiler/parsing
Jul 23 17:06:38 Finished compiler/parsing                                      2m31s   2GB
Jul 23 17:06:38 Starting characteristic
Jul 23 17:18:47 Finished characteristic                                       12m08s   2GB
Jul 23 17:18:47 Starting translator/monadic
Jul 23 17:22:09 Finished translator/monadic                                    3m21s   1GB
Jul 23 17:22:10 Starting basis
Jul 23 18:59:27 Finished basis                                              1h37m17s  21GB
Jul 23 18:59:28 Starting compiler/inference
Jul 23 19:02:10 Finished compiler/inference                                    2m42s   1GB
Jul 23 19:02:10 Starting compiler/backend/reg_alloc
Jul 23 19:04:19 Finished compiler/backend/reg_alloc                            2m08s   1GB
Jul 23 19:04:19 Starting compiler/backend/gc
Jul 23 19:11:18 Finished compiler/backend/gc                                   6m58s   2GB
Jul 23 19:11:18 Starting compiler/backend
Jul 23 19:20:57 Finished compiler/backend                                      9m39s   3GB
Jul 23 19:20:57 Starting compiler/encoders/asm
Jul 23 19:21:46 Finished compiler/encoders/asm                                   48s 837MB
Jul 23 19:21:46 Starting compiler/encoders/x64
Jul 23 19:24:03 Finished compiler/encoders/x64                                 2m16s 805MB
Jul 23 19:24:03 Starting compiler/encoders/arm7
Jul 23 19:28:27 Finished compiler/encoders/arm7                                4m23s   1GB
Jul 23 19:28:27 Starting compiler/encoders/arm8
Jul 23 19:29:51 Finished compiler/encoders/arm8                                1m23s 979MB
Jul 23 19:29:51 Starting compiler/encoders/mips
Jul 23 19:33:10 Finished compiler/encoders/mips                                3m18s   1GB
Jul 23 19:33:10 Starting compiler/encoders/riscv
Jul 23 19:37:01 Finished compiler/encoders/riscv                               3m51s 873MB
Jul 23 19:37:02 Starting compiler/encoders/ag32
Jul 23 19:37:43 Finished compiler/encoders/ag32                                  41s 685MB
Jul 23 19:37:44 Starting compiler/backend/x64
Jul 23 19:38:25 Finished compiler/backend/x64                                    41s   1GB
Jul 23 19:38:25 Starting compiler/backend/arm7
Jul 23 19:39:11 Finished compiler/backend/arm7                                   45s   1GB
Jul 23 19:39:11 Starting compiler/backend/arm8
Jul 23 19:39:52 Finished compiler/backend/arm8                                   40s   1GB
Jul 23 19:39:52 Starting compiler/backend/mips
Jul 23 19:40:35 Finished compiler/backend/mips                                   42s   1GB
Jul 23 19:40:35 Starting compiler/backend/riscv
Jul 23 19:41:17 Finished compiler/backend/riscv                                  41s   1GB
Jul 23 19:41:17 Starting compiler/backend/ag32
Jul 23 19:43:48 Finished compiler/backend/ag32                                 2m30s   1GB
Jul 23 19:43:48 Starting compiler/parsing/proofs
Jul 23 19:56:54 Finished compiler/parsing/proofs                              13m05s 904MB
Jul 23 19:56:55 Starting compiler/inference/proofs
Jul 23 20:02:20 Finished compiler/inference/proofs                             5m24s   1GB
Jul 23 20:02:20 Starting compiler/backend/semantics
Jul 23 21:03:26 Finished compiler/backend/semantics                         1h01m05s   2GB
Jul 23 21:03:26 Starting compiler/backend/reg_alloc/proofs
Jul 23 21:11:08 Finished compiler/backend/reg_alloc/proofs                     7m41s 962MB
Jul 23 21:11:09 Starting compiler/backend/proofs
Jul 23 22:53:23 Finished compiler/backend/proofs                            1h42m14s  15GB
Jul 23 22:53:24 Starting compiler/encoders/x64/proofs
Jul 23 23:14:56 Finished compiler/encoders/x64/proofs                         21m31s   4GB
Jul 23 23:14:56 Starting compiler/encoders/arm7/proofs
Jul 23 23:44:44 Finished compiler/encoders/arm7/proofs                        29m48s   3GB
Jul 23 23:44:45 Starting compiler/encoders/arm8/proofs
Jul 24 00:00:15 Finished compiler/encoders/arm8/proofs                        15m29s   1GB
Jul 24 00:00:15 Starting compiler/encoders/mips/proofs
Jul 24 00:23:01 Finished compiler/encoders/mips/proofs                        22m45s   2GB
Jul 24 00:23:01 Starting compiler/encoders/riscv/proofs
Jul 24 00:43:05 Finished compiler/encoders/riscv/proofs                       20m03s   1GB
Jul 24 00:43:05 Starting compiler/encoders/ag32/proofs
Jul 24 00:48:51 Finished compiler/encoders/ag32/proofs                         5m45s 844MB
Jul 24 00:48:51 Starting compiler/backend/x64/proofs
Jul 24 00:49:40 Finished compiler/backend/x64/proofs                             48s   1GB
Jul 24 00:49:40 Starting compiler/backend/arm7/proofs
Jul 24 00:50:28 Finished compiler/backend/arm7/proofs                            48s   1GB
Jul 24 00:50:29 Starting compiler/backend/arm8/proofs
Jul 24 00:51:17 Finished compiler/backend/arm8/proofs                            47s   1GB
Jul 24 00:51:17 Starting compiler/backend/mips/proofs
Jul 24 00:52:05 Finished compiler/backend/mips/proofs                            47s   1GB
Jul 24 00:52:05 Starting compiler/backend/riscv/proofs
Jul 24 00:52:53 Finished compiler/backend/riscv/proofs                           48s   1GB
Jul 24 00:52:54 Starting compiler/backend/ag32/proofs
Jul 24 01:20:10 Finished compiler/backend/ag32/proofs                         27m15s   3GB
Jul 24 01:20:10 Starting compiler/proofs
Jul 24 01:24:23 Finished compiler/proofs                                       4m12s   5GB
Jul 24 01:24:23 Starting candle/set-theory
Jul 24 01:25:21 Finished candle/set-theory                                       57s   1GB
Jul 24 01:25:21 Starting candle/syntax-lib
Jul 24 01:25:45 Finished candle/syntax-lib                                       23s 525MB
Jul 24 01:25:45 Starting candle/standard/syntax
Jul 24 01:29:40 Finished candle/standard/syntax                                3m54s 955MB
Jul 24 01:29:40 Starting candle/standard/semantics
Jul 24 01:33:35 Finished candle/standard/semantics                             3m53s   1GB
Jul 24 01:33:35 Starting candle/standard/monadic
Jul 24 01:37:15 Finished candle/standard/monadic                               3m39s   1GB
Jul 24 01:37:15 Starting candle/standard/ml_kernel
Jul 24 01:49:20 Finished candle/standard/ml_kernel                            12m04s   3GB
Jul 24 01:49:20 Starting candle/overloading/syntax
Jul 24 01:56:11 Finished candle/overloading/syntax                             6m50s   1GB
Jul 24 01:56:11 Starting candle/overloading/semantics
Jul 24 02:22:18 Finished candle/overloading/semantics                         26m05s   4GB
Jul 24 02:22:18 Starting characteristic/examples
Jul 24 02:25:23 Finished characteristic/examples                               3m04s   2GB
Jul 24 02:25:23 Starting tutorial/solutions
Jul 24 02:59:15 Finished tutorial/solutions                                   33m51s   9GB
Jul 24 02:59:15 Starting translator/monadic/examples
Jul 24 03:05:03 Finished translator/monadic/examples                           5m47s   3GB
Jul 24 03:05:03 Starting examples
Jul 24 03:21:50 Finished examples                                             16m47s   4GB
Jul 24 03:21:51 Starting examples/compilation/x64
Jul 24 08:42:29 Finished examples/compilation/x64                           5h20m38s  19GB
Jul 24 08:42:30 Starting examples/compilation/x64/proofs
Jul 24 08:46:05 Finished examples/compilation/x64/proofs                       3m34s   3GB
Jul 24 08:46:05 Starting examples/compilation/ag32
Jul 24 10:01:23 Finished examples/compilation/ag32                          1h15m18s   8GB
Jul 24 10:01:24 Starting examples/compilation/ag32/proofs
Jul 24 10:03:01 Finished examples/compilation/ag32/proofs                      1m36s   3GB
Jul 24 10:03:01 Starting examples/cost
Jul 24 11:57:52 Finished examples/cost                                      1h54m50s   7GB
Jul 24 11:57:53 Starting examples/lpr_checker
Jul 24 12:06:12 Finished examples/lpr_checker                                  8m19s   3GB
Jul 24 12:06:12 Starting examples/lpr_checker/compilation
Jul 24 12:42:22 Finished examples/lpr_checker/compilation                     36m09s  10GB
Jul 24 12:42:22 Starting examples/lpr_checker/compilation/proofs
Jul 24 12:43:54 Finished examples/lpr_checker/compilation/proofs               1m31s   2GB
Jul 24 12:43:54 Starting examples/lpr_checker/array
Jul 24 13:15:51 Finished examples/lpr_checker/array                           31m56s   4GB
Jul 24 13:15:51 Starting examples/lpr_checker/array/compilation
Jul 24 13:58:14 Finished examples/lpr_checker/array/compilation               42m22s  12GB
Jul 24 13:58:14 Starting examples/lpr_checker/array/compilation/proofs
Jul 24 14:00:02 Finished examples/lpr_checker/array/compilation/proofs         1m47s   4GB
Jul 24 14:00:02 Starting examples/opentheory
Jul 24 14:21:48 Finished examples/opentheory                                  21m45s   5GB
Jul 24 14:21:49 Starting examples/opentheory
Jul 24 14:21:51 Finished examples/opentheory                                      2s  33MB
Jul 24 14:21:51 Starting examples/opentheory/compilation
Jul 24 15:29:55 Finished examples/opentheory/compilation                    1h08m03s  18GB
Jul 24 15:29:55 Starting examples/opentheory/compilation/proofs
Jul 24 15:31:25 Finished examples/opentheory/compilation/proofs                1m29s   3GB
Jul 24 15:31:25 Starting examples/opentheory/compilation/ag32
Jul 24 16:44:33 Finished examples/opentheory/compilation/ag32               1h13m07s  20GB
Jul 24 16:44:33 Starting examples/opentheory/compilation/ag32/proofs
Jul 24 16:47:52 Finished examples/opentheory/compilation/ag32/proofs           3m19s   5GB
Jul 24 16:47:53 Starting examples/sat_encodings
Jul 24 16:51:46 Finished examples/sat_encodings                                3m53s 883MB
Jul 24 16:51:46 Starting examples/sat_encodings/case_studies
Jul 24 16:55:12 Finished examples/sat_encodings/case_studies                   3m25s   1GB
Jul 24 16:55:13 Starting examples/sat_encodings/translation
Jul 24 17:06:35 Finished examples/sat_encodings/translation                   11m21s   5GB
Jul 24 17:06:35 Starting examples/sat_encodings/translation/compilation
Jul 24 18:25:23 Finished examples/sat_encodings/translation/compilation     1h18m47s  11GB
Jul 24 18:25:23 Starting translator/okasaki-examples
Jul 24 18:34:29 Finished translator/okasaki-examples                           9m06s   1GB
Jul 24 18:34:30 Starting translator/other-examples
Jul 24 18:38:24 Finished translator/other-examples                             3m54s   1GB
Jul 24 18:38:25 Starting compiler/parsing/tests
Jul 24 18:39:24 Finished compiler/parsing/tests                                  59s 596MB
Jul 24 18:39:25 Starting compiler/inference/tests
Jul 24 18:54:53 Finished compiler/inference/tests                             15m28s   6GB
Jul 24 18:54:54 Starting compiler/bootstrap/translation
Jul 25 00:24:58 Finished compiler/bootstrap/translation                     5h30m02s  34GB
Jul 25 00:24:58 Starting unverified/sexpr-bootstrap/x64/64
Jul 25 00:49:02 Finished unverified/sexpr-bootstrap/x64/64                    23m59s   8GB
Jul 25 00:49:02 Starting unverified/sexpr-bootstrap/x64/32
Jul 25 01:09:39 Finished unverified/sexpr-bootstrap/x64/32                    20m33s   8GB
Jul 25 01:09:40 Starting compiler/benchmarks
Jul 25 01:09:43 Finished compiler/benchmarks                                      3s  32MB
Jul 25 01:09:43 Starting compiler/bootstrap/compilation/x64/64
Jul 26 02:36:55 Finished compiler/bootstrap/compilation/x64/64             25h27m08s  78GB
Jul 26 02:36:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 26 02:41:38 Finished compiler/bootstrap/compilation/x64/64/proofs          4m43s  16GB
Jul 26 02:41:39 Starting compiler/bootstrap/compilation/x64/32
Jul 27 04:25:23 Finished compiler/bootstrap/compilation/x64/32             25h43m41s 110GB
Jul 27 04:25:24 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 27 04:29:44 Finished compiler/bootstrap/compilation/x64/32/proofs          4m19s  19GB
Jul 27 04:29:44 Starting compiler/bootstrap/compilation/ag32/32
Jul 28 06:35:57 Finished compiler/bootstrap/compilation/ag32/32            26h06m11s  92GB
Jul 28 06:35:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 28 07:07:23 Finished compiler/bootstrap/compilation/ag32/32/proofs        31m26s  19GB
Jul 28 07:07:24 SUCCESS