Job 1177

CakeML:bc31859d41b156f0209a253ab1cee3f334e9b742
  Fix type error caused by HOL change to ThmSetData API [Feb 10 03:15:23]
HOL:1ada1617c02bd7b9335a433e842dc2590e539c6b
  Revert "Eta-expand GEN_REWRITE_CONV so that bounded rewrites work bet [Feb 08 01:35:04]
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

Feb 10 03:16:10 Claimed job
Feb 10 03:16:20 Building HOL
Feb 10 03:39:16 Starting developers
Feb 10 03:39:22 Finished developers                                               6s 124MB
Feb 10 03:39:23 Starting developers/bin
Feb 10 03:39:38 Finished developers/bin                                          15s   1GB
Feb 10 03:39:38 Starting semantics/ffi
Feb 10 03:40:02 Finished semantics/ffi                                           23s 240MB
Feb 10 03:40:02 Starting semantics
Feb 10 03:43:05 Finished semantics                                             3m02s   1GB
Feb 10 03:43:05 Starting semantics/proofs
Feb 10 03:49:58 Finished semantics/proofs                                      6m53s   1GB
Feb 10 03:49:58 Starting semantics/alt_semantics
Feb 10 03:50:17 Finished semantics/alt_semantics                                 18s 321MB
Feb 10 03:50:18 Starting semantics/alt_semantics/proofs
Feb 10 03:54:40 Finished semantics/alt_semantics/proofs                        4m22s   1GB
Feb 10 03:54:40 Starting basis/pure
Feb 10 04:00:32 Finished basis/pure                                            5m51s 905MB
Feb 10 04:00:32 Starting translator
Feb 10 04:05:40 Finished translator                                            5m07s   1GB
Feb 10 04:05:40 Starting compiler/parsing
Feb 10 04:07:59 Finished compiler/parsing                                      2m18s   1GB
Feb 10 04:07:59 Starting characteristic
Feb 10 04:20:04 Finished characteristic                                       12m05s   1GB
Feb 10 04:20:04 Starting translator/monadic
Feb 10 04:23:23 Finished translator/monadic                                    3m18s   1GB
Feb 10 04:23:24 Starting basis
Feb 10 05:32:07 Finished basis                                              1h08m42s  20GB
Feb 10 05:32:07 Starting compiler/inference
Feb 10 05:36:51 Finished compiler/inference                                    4m44s   2GB
Feb 10 05:36:51 Starting compiler/backend/reg_alloc
Feb 10 05:38:45 Finished compiler/backend/reg_alloc                            1m53s   1GB
Feb 10 05:38:45 Starting compiler/backend/gc
Feb 10 05:45:07 Finished compiler/backend/gc                                   6m21s   2GB
Feb 10 05:45:07 Starting compiler/backend
Feb 10 05:53:18 Finished compiler/backend                                      8m09s   4GB
Feb 10 05:53:18 Starting compiler/encoders/asm
Feb 10 05:54:05 Finished compiler/encoders/asm                                   46s 825MB
Feb 10 05:54:05 Starting compiler/encoders/x64
Feb 10 05:56:07 Finished compiler/encoders/x64                                 2m01s 754MB
Feb 10 05:56:08 Starting compiler/encoders/arm7
Feb 10 06:00:00 Finished compiler/encoders/arm7                                3m51s   1GB
Feb 10 06:00:00 Starting compiler/encoders/arm8
Feb 10 06:01:11 Finished compiler/encoders/arm8                                1m11s 816MB
Feb 10 06:01:11 Starting compiler/encoders/mips
Feb 10 06:03:39 Finished compiler/encoders/mips                                2m27s   1GB
Feb 10 06:03:39 Starting compiler/encoders/riscv
Feb 10 06:06:35 Finished compiler/encoders/riscv                               2m55s   1GB
Feb 10 06:06:35 Starting compiler/encoders/ag32
Feb 10 06:07:11 Finished compiler/encoders/ag32                                  36s 826MB
Feb 10 06:07:11 Starting compiler/backend/x64
Feb 10 06:07:49 Finished compiler/backend/x64                                    37s   1GB
Feb 10 06:07:49 Starting compiler/backend/arm7
Feb 10 06:08:32 Finished compiler/backend/arm7                                   42s   1GB
Feb 10 06:08:32 Starting compiler/backend/arm8
Feb 10 06:09:09 Finished compiler/backend/arm8                                   37s   1GB
Feb 10 06:09:09 Starting compiler/backend/mips
Feb 10 06:09:49 Finished compiler/backend/mips                                   39s   1GB
Feb 10 06:09:49 Starting compiler/backend/riscv
Feb 10 06:10:28 Finished compiler/backend/riscv                                  39s   1GB
Feb 10 06:10:29 Starting compiler/backend/ag32
Feb 10 06:12:52 Finished compiler/backend/ag32                                 2m23s   1GB
Feb 10 06:12:52 Starting compiler/parsing/proofs
Feb 10 06:25:06 Finished compiler/parsing/proofs                              12m13s   1GB
Feb 10 06:25:06 Starting compiler/inference/proofs
Feb 10 06:31:33 Finished compiler/inference/proofs                             6m26s   1GB
Feb 10 06:31:33 Starting compiler/backend/semantics
Feb 10 07:27:54 Finished compiler/backend/semantics                           56m20s   2GB
Feb 10 07:27:55 Starting compiler/backend/reg_alloc/proofs
Feb 10 07:35:21 Finished compiler/backend/reg_alloc/proofs                     7m26s   1GB
Feb 10 07:35:21 Starting compiler/backend/proofs
Feb 10 09:37:10 Finished compiler/backend/proofs                            2h01m48s  23GB
Feb 10 09:37:10 Starting compiler/encoders/x64/proofs
Feb 10 09:57:12 Finished compiler/encoders/x64/proofs                         20m02s   4GB
Feb 10 09:57:13 Starting compiler/encoders/arm7/proofs
Feb 10 10:24:43 Finished compiler/encoders/arm7/proofs                        27m30s   3GB
Feb 10 10:24:43 Starting compiler/encoders/arm8/proofs
Feb 10 10:38:36 Finished compiler/encoders/arm8/proofs                        13m52s   1GB
Feb 10 10:38:36 Starting compiler/encoders/mips/proofs
Feb 10 11:00:07 Finished compiler/encoders/mips/proofs                        21m30s   2GB
Feb 10 11:00:07 Starting compiler/encoders/riscv/proofs
Feb 10 11:18:55 Finished compiler/encoders/riscv/proofs                       18m47s   1GB
Feb 10 11:18:56 Starting compiler/encoders/ag32/proofs
Feb 10 11:24:14 Finished compiler/encoders/ag32/proofs                         5m18s 791MB
Feb 10 11:24:14 Starting compiler/backend/x64/proofs
Feb 10 11:24:58 Finished compiler/backend/x64/proofs                             43s   1GB
Feb 10 11:24:58 Starting compiler/backend/arm7/proofs
Feb 10 11:25:41 Finished compiler/backend/arm7/proofs                            42s   1GB
Feb 10 11:25:41 Starting compiler/backend/arm8/proofs
Feb 10 11:26:23 Finished compiler/backend/arm8/proofs                            41s 834MB
Feb 10 11:26:23 Starting compiler/backend/mips/proofs
Feb 10 11:27:06 Finished compiler/backend/mips/proofs                            43s   1GB
Feb 10 11:27:07 Starting compiler/backend/riscv/proofs
Feb 10 11:27:49 Finished compiler/backend/riscv/proofs                           42s   1GB
Feb 10 11:27:49 Starting compiler/backend/ag32/proofs
Feb 10 11:55:23 Finished compiler/backend/ag32/proofs                         27m33s   2GB
Feb 10 11:55:23 Starting compiler/proofs
Feb 10 11:59:08 Finished compiler/proofs                                       3m44s   3GB
Feb 10 11:59:08 Starting candle/set-theory
Feb 10 12:00:03 Finished candle/set-theory                                       54s 784MB
Feb 10 12:00:03 Starting candle/syntax-lib
Feb 10 12:00:25 Finished candle/syntax-lib                                       21s 471MB
Feb 10 12:00:25 Starting candle/standard/syntax
Feb 10 12:04:06 Finished candle/standard/syntax                                3m40s 906MB
Feb 10 12:04:06 Starting candle/standard/semantics
Feb 10 12:07:40 Finished candle/standard/semantics                             3m34s   1GB
Feb 10 12:07:40 Starting candle/standard/monadic
Feb 10 12:11:09 Finished candle/standard/monadic                               3m28s   1GB
Feb 10 12:11:09 Starting candle/standard/ml_kernel
Feb 10 12:21:39 Finished candle/standard/ml_kernel                            10m28s   4GB
Feb 10 12:21:39 Starting candle/standard/opentheory
Feb 10 12:41:11 Finished candle/standard/opentheory                           19m32s   4GB
Feb 10 12:41:12 Starting candle/standard/opentheory/compilation
Feb 10 13:44:52 Finished candle/standard/opentheory/compilation             1h03m40s  15GB
Feb 10 13:44:53 Starting candle/standard/opentheory/compilation/proofs
Feb 10 13:46:07 Finished candle/standard/opentheory/compilation/proofs         1m14s   2GB
Feb 10 13:46:07 Starting characteristic/examples
Feb 10 13:49:12 Finished characteristic/examples                               3m04s   2GB
Feb 10 13:49:12 Starting tutorial/solutions
Feb 10 14:19:47 Finished tutorial/solutions                                   30m35s   6GB
Feb 10 14:19:48 Starting translator/monadic/examples
Feb 10 14:24:51 Finished translator/monadic/examples                           5m03s   2GB
Feb 10 14:24:51 Starting examples
Feb 10 14:40:44 Finished examples                                             15m52s   3GB
Feb 10 14:40:44 Starting examples/compilation/x64
Feb 10 19:27:15 Finished examples/compilation/x64                           4h46m30s  15GB
Feb 10 19:27:15 Starting examples/compilation/x64/proofs
Feb 10 19:30:22 Finished examples/compilation/x64/proofs                       3m07s   3GB
Feb 10 19:30:23 Starting examples/compilation/ag32
Feb 10 20:37:37 Finished examples/compilation/ag32                          1h07m13s   6GB
Feb 10 20:37:37 Starting examples/compilation/ag32/proofs
Feb 10 20:39:03 Finished examples/compilation/ag32/proofs                      1m26s   3GB
Feb 10 20:39:03 Starting examples/cost
Feb 10 22:06:58 Finished examples/cost                                      1h27m54s   7GB
Feb 10 22:06:58 Starting examples/lpr_checker
Feb 10 22:14:53 Finished examples/lpr_checker                                  7m54s   3GB
Feb 10 22:14:53 Starting examples/lpr_checker/compilation
Feb 10 22:47:00 Finished examples/lpr_checker/compilation                     32m06s   8GB
Feb 10 22:47:00 Starting examples/lpr_checker/compilation/proofs
Feb 10 22:48:18 Finished examples/lpr_checker/compilation/proofs               1m17s   3GB
Feb 10 22:48:18 Starting examples/lpr_checker/array
Feb 10 23:08:22 Finished examples/lpr_checker/array                           20m03s   2GB
Feb 10 23:08:23 Starting examples/lpr_checker/array/compilation
Feb 10 23:40:32 Finished examples/lpr_checker/array/compilation               32m09s   7GB
Feb 10 23:40:32 Starting examples/lpr_checker/array/compilation/proofs
Feb 10 23:42:00 Finished examples/lpr_checker/array/compilation/proofs         1m27s   3GB
Feb 10 23:42:00 Starting translator/okasaki-examples
Feb 10 23:50:32 Finished translator/okasaki-examples                           8m31s   1GB
Feb 10 23:50:32 Starting translator/other-examples
Feb 10 23:54:18 Finished translator/other-examples                             3m46s   2GB
Feb 10 23:54:18 Starting compiler/parsing/tests
Feb 10 23:55:13 Finished compiler/parsing/tests                                  53s 544MB
Feb 10 23:55:13 Starting compiler/inference/tests
Feb 11 00:03:50 Finished compiler/inference/tests                              8m37s   3GB
Feb 11 00:03:50 Starting compiler/bootstrap/translation
Feb 11 07:34:45 Finished compiler/bootstrap/translation                     7h30m54s  56GB
Feb 11 07:34:45 Starting unverified/sexpr-bootstrap/x64/64
Feb 11 08:02:10 Finished unverified/sexpr-bootstrap/x64/64                    27m23s  11GB
Feb 11 08:02:10 Starting unverified/sexpr-bootstrap/x64/32
Feb 11 08:22:41 Finished unverified/sexpr-bootstrap/x64/32                    20m30s   9GB
Feb 11 08:22:41 Starting compiler/benchmarks
Feb 11 08:22:45 Finished compiler/benchmarks                                      3s  32MB
Feb 11 08:22:45 Starting compiler/bootstrap/compilation/x64/64
Feb 12 12:55:26 Finished compiler/bootstrap/compilation/x64/64             28h32m38s  90GB
Feb 12 12:55:26 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 12 13:01:11 Finished compiler/bootstrap/compilation/x64/64/proofs          5m44s  25GB
Feb 12 13:01:11 Starting compiler/bootstrap/compilation/x64/32
Feb 13 16:56:17 Finished compiler/bootstrap/compilation/x64/32             27h55m04s 110GB
Feb 13 16:56:17 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 13 17:01:27 Finished compiler/bootstrap/compilation/x64/32/proofs          5m09s  23GB
Feb 13 17:01:27 Starting compiler/bootstrap/compilation/ag32/32
Feb 14 21:38:20 Finished compiler/bootstrap/compilation/ag32/32            28h36m52s 127GB
Feb 14 21:38:20 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 14 22:07:18 Finished compiler/bootstrap/compilation/ag32/32/proofs        28m57s  46GB
Feb 14 22:07:18 SUCCESS