Job 2077

CakeML:64cd17eb616d68a37179855402bb3ff8806d661b
  Fix/avoid some breakage [Dec 17 21:46:43]
HOL:9fe7958228a051e013f9a9842a7fbea4485a772c
  Fix a bug in `qrefinel` [Dec 15 00:59:10]
Machine:oven3
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Dec 22 17:39:39 Claimed job
Dec 22 17:39:48 Building HOL
Dec 22 18:03:11 Starting developers
Dec 22 18:03:20 Finished developers                                               8s 141MB
Dec 22 18:03:20 Starting developers/bin
Dec 22 18:03:33 Finished developers/bin                                          12s   1GB
Dec 22 18:03:33 Starting compiler/proofs
Dec 22 21:34:06 Finished compiler/proofs                                    3h30m32s  20GB
Dec 22 21:34:06 Starting compiler/bootstrap/translation
Dec 23 07:53:03 Finished compiler/bootstrap/translation                    10h18m56s  43GB
Dec 23 07:53:04 Starting semantics/ffi
Dec 23 07:53:12 Finished semantics/ffi                                            7s 203MB
Dec 23 07:53:12 Starting semantics
Dec 23 07:53:14 Finished semantics                                                2s  17MB
Dec 23 07:53:15 Starting semantics/proofs
Dec 23 07:54:34 Finished semantics/proofs                                      1m19s 802MB
Dec 23 07:54:34 Starting semantics/alt_semantics
Dec 23 07:55:30 Finished semantics/alt_semantics                                 55s 686MB
Dec 23 07:55:30 Starting semantics/alt_semantics/proofs
Dec 23 08:21:06 Finished semantics/alt_semantics/proofs                       25m35s   1GB
Dec 23 08:21:06 Starting basis/pure
Dec 23 08:21:09 Finished basis/pure                                               2s  32MB
Dec 23 08:21:09 Starting translator
Dec 23 08:24:53 Finished translator                                            3m44s   1GB
Dec 23 08:24:54 Starting compiler/parsing
Dec 23 08:24:56 Finished compiler/parsing                                         2s  18MB
Dec 23 08:24:56 Starting characteristic
Dec 23 08:25:00 Finished characteristic                                           3s  33MB
Dec 23 08:25:00 Starting translator/monadic
Dec 23 08:25:03 Finished translator/monadic                                       2s  41MB
Dec 23 08:25:03 Starting basis
Dec 23 08:32:41 Finished basis                                                 7m37s   2GB
Dec 23 08:32:42 Starting compiler/inference
Dec 23 08:32:44 Finished compiler/inference                                       2s  29MB
Dec 23 08:32:45 Starting compiler/backend/reg_alloc
Dec 23 08:32:47 Finished compiler/backend/reg_alloc                               2s  27MB
Dec 23 08:32:47 Starting compiler/backend/gc
Dec 23 08:32:51 Finished compiler/backend/gc                                      3s  31MB
Dec 23 08:32:52 Starting compiler/backend
Dec 23 08:33:14 Finished compiler/backend                                        22s 633MB
Dec 23 08:33:14 Starting compiler/encoders/asm
Dec 23 08:33:17 Finished compiler/encoders/asm                                    2s  27MB
Dec 23 08:33:17 Starting compiler/encoders/x64
Dec 23 08:33:20 Finished compiler/encoders/x64                                    2s  33MB
Dec 23 08:33:21 Starting compiler/encoders/arm7
Dec 23 08:33:24 Finished compiler/encoders/arm7                                   2s  24MB
Dec 23 08:33:24 Starting compiler/encoders/arm8
Dec 23 08:33:27 Finished compiler/encoders/arm8                                   2s  29MB
Dec 23 08:33:27 Starting compiler/encoders/arm8_asl
Dec 23 12:50:18 Finished compiler/encoders/arm8_asl                         4h16m51s  30GB
Dec 23 12:50:19 Starting compiler/encoders/mips
Dec 23 12:50:22 Finished compiler/encoders/mips                                   2s  27MB
Dec 23 12:50:22 Starting compiler/encoders/riscv
Dec 23 12:50:26 Finished compiler/encoders/riscv                                  4s  35MB
Dec 23 12:50:26 Starting compiler/encoders/ag32
Dec 23 12:50:29 Finished compiler/encoders/ag32                                   2s  31MB
Dec 23 12:50:29 Starting compiler/backend/x64
Dec 23 12:50:33 Finished compiler/backend/x64                                     3s  33MB
Dec 23 12:50:33 Starting compiler/backend/arm7
Dec 23 12:50:37 Finished compiler/backend/arm7                                    3s  33MB
Dec 23 12:50:37 Starting compiler/backend/arm8
Dec 23 12:50:41 Finished compiler/backend/arm8                                    3s  44MB
Dec 23 12:50:41 Starting compiler/backend/mips
Dec 23 12:50:45 Finished compiler/backend/mips                                    3s  34MB
Dec 23 12:50:45 Starting compiler/backend/riscv
Dec 23 12:50:49 Finished compiler/backend/riscv                                   3s  33MB
Dec 23 12:50:49 Starting compiler/backend/ag32
Dec 23 12:53:47 Finished compiler/backend/ag32                                 2m57s   1GB
Dec 23 12:53:47 Starting compiler/parsing/proofs
Dec 23 12:53:50 Finished compiler/parsing/proofs                                  2s  28MB
Dec 23 12:53:50 Starting compiler/inference/proofs
Dec 23 12:53:53 Finished compiler/inference/proofs                                2s  27MB
Dec 23 12:53:54 Starting compiler/backend/semantics
Dec 23 12:56:11 Finished compiler/backend/semantics                            2m17s   1GB
Dec 23 12:56:11 Starting compiler/backend/reg_alloc/proofs
Dec 23 12:56:14 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Dec 23 12:56:15 Starting compiler/backend/proofs
Dec 23 12:58:16 Finished compiler/backend/proofs                               2m00s   3GB
Dec 23 12:58:16 Starting compiler/backend/serialiser
Dec 23 12:58:21 Finished compiler/backend/serialiser                              5s  47MB
Dec 23 12:58:21 Starting compiler/encoders/x64/proofs
Dec 23 13:20:09 Finished compiler/encoders/x64/proofs                         21m47s   5GB
Dec 23 13:20:09 Starting compiler/encoders/arm7/proofs
Dec 23 13:51:07 Finished compiler/encoders/arm7/proofs                        30m56s   3GB
Dec 23 13:51:07 Starting compiler/encoders/arm8/proofs
Dec 23 14:07:01 Finished compiler/encoders/arm8/proofs                        15m53s   1GB
Dec 23 14:07:01 Starting compiler/encoders/arm8_asl/proofs
Dec 23 16:04:01 Finished compiler/encoders/arm8_asl/proofs                  1h56m59s   6GB
Dec 23 16:04:01 Starting compiler/encoders/mips/proofs
Dec 23 16:27:39 Finished compiler/encoders/mips/proofs                        23m37s   2GB
Dec 23 16:27:39 Starting compiler/encoders/riscv/proofs
Dec 23 16:48:14 Finished compiler/encoders/riscv/proofs                       20m35s   1GB
Dec 23 16:48:14 Starting compiler/encoders/ag32/proofs
Dec 23 16:54:08 Finished compiler/encoders/ag32/proofs                         5m53s 884MB
Dec 23 16:54:08 Starting compiler/backend/x64/proofs
Dec 23 16:55:03 Finished compiler/backend/x64/proofs                             54s   1GB
Dec 23 16:55:03 Starting compiler/backend/arm7/proofs
Dec 23 16:55:58 Finished compiler/backend/arm7/proofs                            55s   1GB
Dec 23 16:55:59 Starting compiler/backend/arm8/proofs
Dec 23 16:56:56 Finished compiler/backend/arm8/proofs                            57s   1GB
Dec 23 16:56:56 Starting compiler/backend/arm8_asl
Dec 23 16:57:39 Finished compiler/backend/arm8_asl                               42s   1GB
Dec 23 16:57:39 Starting compiler/backend/mips/proofs
Dec 23 16:58:34 Finished compiler/backend/mips/proofs                            54s   1GB
Dec 23 16:58:34 Starting compiler/backend/riscv/proofs
Dec 23 16:59:44 Finished compiler/backend/riscv/proofs                         1m10s   1GB
Dec 23 16:59:44 Starting compiler/backend/ag32/proofs
Dec 23 17:30:16 Finished compiler/backend/ag32/proofs                         30m31s   2GB
Dec 23 17:30:16 Starting candle/set-theory
Dec 23 17:31:27 Finished candle/set-theory                                     1m10s 995MB
Dec 23 17:31:27 Starting candle/syntax-lib
Dec 23 17:31:30 Finished candle/syntax-lib                                        2s  16MB
Dec 23 17:31:30 Starting candle/standard/syntax
Dec 23 17:31:49 Finished candle/standard/syntax                                  19s 553MB
Dec 23 17:31:50 Starting candle/standard/semantics
Dec 23 17:35:46 Finished candle/standard/semantics                             3m55s   1GB
Dec 23 17:35:46 Starting candle/standard/monadic
Dec 23 17:35:49 Finished candle/standard/monadic                                  2s  33MB
Dec 23 17:35:49 Starting candle/standard/ml_kernel
Dec 23 17:38:51 Finished candle/standard/ml_kernel                             3m01s   2GB
Dec 23 17:38:51 Starting candle/overloading/syntax
Dec 23 17:45:51 Finished candle/overloading/syntax                             7m00s   1GB
Dec 23 17:45:51 Starting candle/overloading/semantics
Dec 23 18:12:18 Finished candle/overloading/semantics                         26m26s   2GB
Dec 23 18:12:18 Starting candle/overloading/monadic
Dec 23 18:17:57 Finished candle/overloading/monadic                            5m38s   1GB
Dec 23 18:17:57 Starting candle/overloading/ml_kernel
Dec 23 18:33:19 Finished candle/overloading/ml_kernel                         15m21s   3GB
Dec 23 18:33:19 Starting candle/overloading/ml_checker
Dec 23 18:38:42 Finished candle/overloading/ml_checker                         5m23s   2GB
Dec 23 18:38:43 Starting candle/prover
Dec 23 19:00:22 Finished candle/prover                                        21m39s   3GB
Dec 23 19:00:23 Starting pancake
Dec 23 19:06:49 Finished pancake                                               6m25s   4GB
Dec 23 19:06:49 Starting pancake/ffi
Dec 23 19:06:50 Finished pancake/ffi                                              0s  11MB
Dec 23 19:06:50 Starting pancake/semantics
Dec 23 19:11:54 Finished pancake/semantics                                     5m03s   1GB
Dec 23 19:11:54 Starting pancake/proofs
Dec 23 19:18:04 Finished pancake/proofs                                        6m10s   2GB
Dec 23 19:18:05 Starting characteristic/examples
Dec 23 19:21:05 Finished characteristic/examples                               3m00s   2GB
Dec 23 19:21:05 Starting tutorial/solutions
Dec 23 19:54:42 Finished tutorial/solutions                                   33m36s   7GB
Dec 23 19:54:42 Starting translator/monadic/examples
Dec 23 20:01:22 Finished translator/monadic/examples                           6m39s   2GB
Dec 23 20:01:22 Starting examples
Dec 23 20:20:47 Finished examples                                             19m24s   3GB
Dec 23 20:20:47 Starting examples/compilation/x64
Dec 24 00:38:48 Finished examples/compilation/x64                           4h18m00s  17GB
Dec 24 00:38:48 Starting examples/compilation/x64/proofs
Dec 24 00:42:50 Finished examples/compilation/x64/proofs                       4m01s   3GB
Dec 24 00:42:50 Starting examples/compilation/ag32
Dec 24 01:49:26 Finished examples/compilation/ag32                          1h06m35s  10GB
Dec 24 01:49:26 Starting examples/compilation/ag32/proofs
Dec 24 01:51:08 Finished examples/compilation/ag32/proofs                      1m41s   3GB
Dec 24 01:51:08 Starting examples/compilation/to_word
Dec 24 01:57:44 Finished examples/compilation/to_word                          6m35s   5GB
Dec 24 01:57:45 Starting examples/lpr_checker
Dec 24 01:59:42 Finished examples/lpr_checker                                  1m56s   1GB
Dec 24 01:59:42 Starting examples/lpr_checker/array
Dec 24 03:21:04 Finished examples/lpr_checker/array                         1h21m21s   4GB
Dec 24 03:21:04 Starting examples/lpr_checker/array/compilation
Dec 24 04:38:24 Finished examples/lpr_checker/array/compilation             1h17m19s  28GB
Dec 24 04:38:24 Starting examples/lpr_checker/array/compilation/proofs
Dec 24 04:41:04 Finished examples/lpr_checker/array/compilation/proofs         2m39s   5GB
Dec 24 04:41:04 Starting examples/opentheory
Dec 24 05:03:25 Finished examples/opentheory                                  22m19s   6GB
Dec 24 05:03:25 Starting examples/opentheory
Dec 24 05:03:28 Finished examples/opentheory                                      3s  32MB
Dec 24 05:03:28 Starting examples/opentheory/compilation
Dec 24 06:28:07 Finished examples/opentheory/compilation                    1h24m38s  40GB
Dec 24 06:28:07 Starting examples/opentheory/compilation/proofs
Dec 24 06:29:49 Finished examples/opentheory/compilation/proofs                1m41s   4GB
Dec 24 06:29:49 Starting examples/opentheory/compilation/ag32
Dec 24 07:47:51 Finished examples/opentheory/compilation/ag32               1h18m01s  47GB
Dec 24 07:47:51 Starting examples/opentheory/compilation/ag32/proofs
Dec 24 07:51:31 Finished examples/opentheory/compilation/ag32/proofs           3m39s   6GB
Dec 24 07:51:32 Starting examples/sat_encodings
Dec 24 07:55:17 Finished examples/sat_encodings                                3m45s   1GB
Dec 24 07:55:17 Starting examples/sat_encodings/case_studies
Dec 24 07:58:56 Finished examples/sat_encodings/case_studies                   3m38s   1GB
Dec 24 07:58:56 Starting examples/sat_encodings/translation
Dec 24 08:10:26 Finished examples/sat_encodings/translation                   11m29s   3GB
Dec 24 08:10:26 Starting examples/sat_encodings/translation/compilation
Dec 24 09:31:28 Finished examples/sat_encodings/translation/compilation     1h21m01s  24GB
Dec 24 09:31:28 Starting examples/deflate
Dec 24 09:33:18 Finished examples/deflate                                      1m50s 792MB
Dec 24 09:33:19 Starting examples/deflate/translation
Dec 24 09:36:20 Finished examples/deflate/translation                          3m01s   2GB
Dec 24 09:36:21 Starting examples/deflate/translation/compilation
Dec 24 10:12:42 Finished examples/deflate/translation/compilation             36m20s  14GB
Dec 24 10:12:42 Starting translator/okasaki-examples
Dec 24 10:22:38 Finished translator/okasaki-examples                           9m55s   1GB
Dec 24 10:22:38 Starting translator/other-examples
Dec 24 10:27:40 Finished translator/other-examples                             5m01s   1GB
Dec 24 10:27:40 Starting compiler/parsing/tests
Dec 24 10:28:47 Finished compiler/parsing/tests                                1m06s 617MB
Dec 24 10:28:48 Starting compiler/inference/tests
Dec 24 10:45:39 Finished compiler/inference/tests                             16m50s   3GB
Dec 24 10:45:39 Starting compiler/printing/test
Dec 24 10:52:46 Finished compiler/printing/test                                7m07s   3GB
Dec 24 10:52:47 Starting icing/flover
Dec 24 12:27:40 Finished icing/flover                                       1h34m53s   1GB
Dec 24 12:27:40 Starting icing/
Dec 24 14:41:36 Finished icing/                                             2h13m54s   7GB
Dec 24 14:41:36 Starting icing/examples
Dec 24 14:44:44 Finished icing/examples                                        3m07s   3GB
Dec 24 14:44:44 Starting compiler/repl
Dec 24 15:03:08 Finished compiler/repl                                        18m23s   5GB
Dec 24 15:03:08 Starting unverified/sexpr-bootstrap/x64/64
Dec 24 15:26:16 Finished unverified/sexpr-bootstrap/x64/64                    23m07s  13GB
Dec 24 15:26:16 Starting unverified/sexpr-bootstrap/x64/32
Dec 24 15:45:06 Finished unverified/sexpr-bootstrap/x64/32                    18m49s  12GB
Dec 24 15:45:06 Starting compiler/benchmarks
Dec 24 15:45:13 Finished compiler/benchmarks                                      6s  44MB
Dec 24 15:45:13 Starting compiler/bootstrap/compilation/x64/64
Dec 25 18:06:32 Finished compiler/bootstrap/compilation/x64/64             26h21m18s 123GB
Dec 25 18:06:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 25 18:50:00 Finished compiler/bootstrap/compilation/x64/64/proofs         43m27s  35GB
Dec 25 18:50:00 Starting compiler/bootstrap/compilation/x64/32
Dec 26 08:38:39 Finished compiler/bootstrap/compilation/x64/32             13h48m37s 109GB
Dec 26 08:38:39 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 26 08:43:45 Finished compiler/bootstrap/compilation/x64/32/proofs          5m05s  16GB
Dec 26 08:43:45 Starting compiler/bootstrap/compilation/ag32/32
Dec 26 22:51:56 Finished compiler/bootstrap/compilation/ag32/32            14h08m10s 107GB
Dec 26 22:51:56 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 26 23:04:43 Finished compiler/bootstrap/compilation/ag32/32/proofs        12m46s  35GB
Dec 26 23:04:43 SUCCESS