Job 2073

CakeML:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:0cdd3535ed2f647e048a3741f226dd1bdbb3fcbd
  Tidy itreeTau changes (remove Unicode; fix over-long lines; reduce pr [Dec 11 22:45:07]
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 13 11:51:46 Claimed job
Dec 13 11:51:53 Building HOL
Dec 13 12:15:01 Starting developers
Dec 13 12:15:11 Finished developers                                               9s 109MB
Dec 13 12:15:11 Starting developers/bin
Dec 13 12:15:23 Finished developers/bin                                          12s   1GB
Dec 13 12:15:24 Starting compiler/proofs
Dec 13 15:46:04 Finished compiler/proofs                                    3h30m39s  17GB
Dec 13 15:46:04 Starting compiler/bootstrap/translation
Dec 14 02:04:25 Finished compiler/bootstrap/translation                    10h18m20s  36GB
Dec 14 02:04:26 Starting semantics/ffi
Dec 14 02:04:34 Finished semantics/ffi                                            8s 214MB
Dec 14 02:04:34 Starting semantics
Dec 14 02:04:37 Finished semantics                                                2s  21MB
Dec 14 02:04:37 Starting semantics/proofs
Dec 14 02:05:54 Finished semantics/proofs                                      1m16s 898MB
Dec 14 02:05:54 Starting semantics/alt_semantics
Dec 14 02:06:54 Finished semantics/alt_semantics                                 59s 538MB
Dec 14 02:06:54 Starting semantics/alt_semantics/proofs
Dec 14 02:32:20 Finished semantics/alt_semantics/proofs                       25m25s   1GB
Dec 14 02:32:20 Starting basis/pure
Dec 14 02:32:23 Finished basis/pure                                               2s  34MB
Dec 14 02:32:23 Starting translator
Dec 14 02:36:05 Finished translator                                            3m41s   1GB
Dec 14 02:36:05 Starting compiler/parsing
Dec 14 02:36:08 Finished compiler/parsing                                         2s  27MB
Dec 14 02:36:08 Starting characteristic
Dec 14 02:36:11 Finished characteristic                                           2s  33MB
Dec 14 02:36:11 Starting translator/monadic
Dec 14 02:36:14 Finished translator/monadic                                       2s  39MB
Dec 14 02:36:15 Starting basis
Dec 14 02:43:59 Finished basis                                                 7m44s   2GB
Dec 14 02:44:00 Starting compiler/inference
Dec 14 02:44:03 Finished compiler/inference                                       2s  29MB
Dec 14 02:44:03 Starting compiler/backend/reg_alloc
Dec 14 02:44:05 Finished compiler/backend/reg_alloc                               2s  18MB
Dec 14 02:44:05 Starting compiler/backend/gc
Dec 14 02:44:09 Finished compiler/backend/gc                                      3s  43MB
Dec 14 02:44:10 Starting compiler/backend
Dec 14 02:44:34 Finished compiler/backend                                        24s 463MB
Dec 14 02:44:35 Starting compiler/encoders/asm
Dec 14 02:44:37 Finished compiler/encoders/asm                                    2s  26MB
Dec 14 02:44:38 Starting compiler/encoders/x64
Dec 14 02:44:41 Finished compiler/encoders/x64                                    2s  31MB
Dec 14 02:44:41 Starting compiler/encoders/arm7
Dec 14 02:44:44 Finished compiler/encoders/arm7                                   2s  28MB
Dec 14 02:44:44 Starting compiler/encoders/arm8
Dec 14 02:44:47 Finished compiler/encoders/arm8                                   2s  23MB
Dec 14 02:44:47 Starting compiler/encoders/arm8_asl
Dec 14 07:08:29 Finished compiler/encoders/arm8_asl                         4h23m41s  41GB
Dec 14 07:08:29 Starting compiler/encoders/mips
Dec 14 07:08:32 Finished compiler/encoders/mips                                   2s  27MB
Dec 14 07:08:32 Starting compiler/encoders/riscv
Dec 14 07:08:35 Finished compiler/encoders/riscv                                  2s  31MB
Dec 14 07:08:35 Starting compiler/encoders/ag32
Dec 14 07:08:38 Finished compiler/encoders/ag32                                   2s  27MB
Dec 14 07:08:38 Starting compiler/backend/x64
Dec 14 07:08:42 Finished compiler/backend/x64                                     3s  32MB
Dec 14 07:08:42 Starting compiler/backend/arm7
Dec 14 07:08:46 Finished compiler/backend/arm7                                    3s  35MB
Dec 14 07:08:46 Starting compiler/backend/arm8
Dec 14 07:08:50 Finished compiler/backend/arm8                                    3s  26MB
Dec 14 07:08:50 Starting compiler/backend/mips
Dec 14 07:08:54 Finished compiler/backend/mips                                    2s  33MB
Dec 14 07:08:54 Starting compiler/backend/riscv
Dec 14 07:08:57 Finished compiler/backend/riscv                                   2s  30MB
Dec 14 07:08:57 Starting compiler/backend/ag32
Dec 14 07:11:55 Finished compiler/backend/ag32                                 2m58s   1GB
Dec 14 07:11:56 Starting compiler/parsing/proofs
Dec 14 07:11:58 Finished compiler/parsing/proofs                                  2s  24MB
Dec 14 07:11:59 Starting compiler/inference/proofs
Dec 14 07:12:02 Finished compiler/inference/proofs                                2s  33MB
Dec 14 07:12:02 Starting compiler/backend/semantics
Dec 14 07:14:23 Finished compiler/backend/semantics                            2m20s   1GB
Dec 14 07:14:23 Starting compiler/backend/reg_alloc/proofs
Dec 14 07:14:26 Finished compiler/backend/reg_alloc/proofs                        3s  26MB
Dec 14 07:14:27 Starting compiler/backend/proofs
Dec 14 07:16:27 Finished compiler/backend/proofs                               1m59s   3GB
Dec 14 07:16:27 Starting compiler/backend/serialiser
Dec 14 07:16:32 Finished compiler/backend/serialiser                              4s  49MB
Dec 14 07:16:32 Starting compiler/encoders/x64/proofs
Dec 14 07:38:44 Finished compiler/encoders/x64/proofs                         22m12s   5GB
Dec 14 07:38:45 Starting compiler/encoders/arm7/proofs
Dec 14 08:10:07 Finished compiler/encoders/arm7/proofs                        31m21s   3GB
Dec 14 08:10:07 Starting compiler/encoders/arm8/proofs
Dec 14 08:26:16 Finished compiler/encoders/arm8/proofs                        16m08s   1GB
Dec 14 08:26:16 Starting compiler/encoders/arm8_asl/proofs
Dec 14 10:22:19 Finished compiler/encoders/arm8_asl/proofs                  1h56m02s   5GB
Dec 14 10:22:20 Starting compiler/encoders/mips/proofs
Dec 14 10:46:30 Finished compiler/encoders/mips/proofs                        24m10s   2GB
Dec 14 10:46:30 Starting compiler/encoders/riscv/proofs
Dec 14 11:06:59 Finished compiler/encoders/riscv/proofs                       20m28s   1GB
Dec 14 11:06:59 Starting compiler/encoders/ag32/proofs
Dec 14 11:12:50 Finished compiler/encoders/ag32/proofs                         5m50s 904MB
Dec 14 11:12:50 Starting compiler/backend/x64/proofs
Dec 14 11:13:45 Finished compiler/backend/x64/proofs                             54s   1GB
Dec 14 11:13:46 Starting compiler/backend/arm7/proofs
Dec 14 11:14:44 Finished compiler/backend/arm7/proofs                            58s   1GB
Dec 14 11:14:45 Starting compiler/backend/arm8/proofs
Dec 14 11:15:39 Finished compiler/backend/arm8/proofs                            54s   1GB
Dec 14 11:15:39 Starting compiler/backend/arm8_asl
Dec 14 11:16:26 Finished compiler/backend/arm8_asl                               45s   1GB
Dec 14 11:16:26 Starting compiler/backend/mips/proofs
Dec 14 11:17:21 Finished compiler/backend/mips/proofs                            54s   1GB
Dec 14 11:17:21 Starting compiler/backend/riscv/proofs
Dec 14 11:18:13 Finished compiler/backend/riscv/proofs                           51s   1GB
Dec 14 11:18:13 Starting compiler/backend/ag32/proofs
Dec 14 11:48:28 Finished compiler/backend/ag32/proofs                         30m14s   2GB
Dec 14 11:48:28 Starting candle/set-theory
Dec 14 11:49:37 Finished candle/set-theory                                     1m08s   1GB
Dec 14 11:49:37 Starting candle/syntax-lib
Dec 14 11:49:39 Finished candle/syntax-lib                                        2s  16MB
Dec 14 11:49:40 Starting candle/standard/syntax
Dec 14 11:49:59 Finished candle/standard/syntax                                  19s 524MB
Dec 14 11:50:00 Starting candle/standard/semantics
Dec 14 11:53:47 Finished candle/standard/semantics                             3m47s   1GB
Dec 14 11:53:48 Starting candle/standard/monadic
Dec 14 11:53:51 Finished candle/standard/monadic                                  2s  33MB
Dec 14 11:53:51 Starting candle/standard/ml_kernel
Dec 14 11:56:47 Finished candle/standard/ml_kernel                             2m56s   2GB
Dec 14 11:56:47 Starting candle/overloading/syntax
Dec 14 12:03:43 Finished candle/overloading/syntax                             6m55s   1GB
Dec 14 12:03:43 Starting candle/overloading/semantics
Dec 14 12:29:55 Finished candle/overloading/semantics                         26m11s   2GB
Dec 14 12:29:55 Starting candle/overloading/monadic
Dec 14 12:35:26 Finished candle/overloading/monadic                            5m30s   1GB
Dec 14 12:35:26 Starting candle/overloading/ml_kernel
Dec 14 12:50:53 Finished candle/overloading/ml_kernel                         15m25s   3GB
Dec 14 12:50:53 Starting candle/overloading/ml_checker
Dec 14 12:56:21 Finished candle/overloading/ml_checker                         5m28s   2GB
Dec 14 12:56:21 Starting candle/prover
Dec 14 13:17:26 Finished candle/prover                                        21m04s   3GB
Dec 14 13:17:26 Starting pancake
Dec 14 13:23:42 Finished pancake                                               6m15s   4GB
Dec 14 13:23:42 Starting pancake/ffi
Dec 14 13:23:43 Finished pancake/ffi                                              0s  11MB
Dec 14 13:23:43 Starting pancake/semantics
Dec 14 13:28:47 Finished pancake/semantics                                     5m03s   1GB
Dec 14 13:28:47 Starting pancake/proofs
Dec 14 13:35:01 Finished pancake/proofs                                        6m13s   2GB
Dec 14 13:35:02 Starting characteristic/examples
Dec 14 13:38:00 Finished characteristic/examples                               2m58s   2GB
Dec 14 13:38:00 Starting tutorial/solutions
Dec 14 14:11:55 Finished tutorial/solutions                                   33m54s   9GB
Dec 14 14:11:56 Starting translator/monadic/examples
Dec 14 14:18:42 Finished translator/monadic/examples                           6m46s   2GB
Dec 14 14:18:42 Starting examples
Dec 14 14:38:11 Finished examples                                             19m27s   4GB
Dec 14 14:38:11 Starting examples/compilation/x64
Dec 14 18:56:27 Finished examples/compilation/x64                           4h18m15s  17GB
Dec 14 18:56:27 Starting examples/compilation/x64/proofs
Dec 14 19:00:40 Finished examples/compilation/x64/proofs                       4m12s   3GB
Dec 14 19:00:40 Starting examples/compilation/ag32
Dec 14 20:06:43 Finished examples/compilation/ag32                          1h06m01s   8GB
Dec 14 20:06:43 Starting examples/compilation/ag32/proofs
Dec 14 20:08:25 Finished examples/compilation/ag32/proofs                      1m42s   3GB
Dec 14 20:08:26 Starting examples/compilation/to_word
Dec 14 20:15:02 Finished examples/compilation/to_word                          6m36s   5GB
Dec 14 20:15:03 Starting examples/lpr_checker
Dec 14 20:17:01 Finished examples/lpr_checker                                  1m57s   1GB
Dec 14 20:17:01 Starting examples/lpr_checker/array
Dec 14 21:37:01 Finished examples/lpr_checker/array                         1h20m00s   6GB
Dec 14 21:37:02 Starting examples/lpr_checker/array/compilation
Dec 14 22:57:02 Finished examples/lpr_checker/array/compilation             1h19m59s  37GB
Dec 14 22:57:02 Starting examples/lpr_checker/array/compilation/proofs
Dec 14 22:59:40 Finished examples/lpr_checker/array/compilation/proofs         2m37s   6GB
Dec 14 22:59:41 Starting examples/opentheory
Dec 14 23:22:24 Finished examples/opentheory                                  22m42s   5GB
Dec 14 23:22:24 Starting examples/opentheory
Dec 14 23:22:28 Finished examples/opentheory                                      3s  33MB
Dec 14 23:22:28 Starting examples/opentheory/compilation
Dec 15 00:44:37 Finished examples/opentheory/compilation                    1h22m09s  33GB
Dec 15 00:44:37 Starting examples/opentheory/compilation/proofs
Dec 15 00:46:22 Finished examples/opentheory/compilation/proofs                1m43s   4GB
Dec 15 00:46:22 Starting examples/opentheory/compilation/ag32
Dec 15 02:02:43 Finished examples/opentheory/compilation/ag32               1h16m20s  41GB
Dec 15 02:02:44 Starting examples/opentheory/compilation/ag32/proofs
Dec 15 02:06:28 Finished examples/opentheory/compilation/ag32/proofs           3m43s   6GB
Dec 15 02:06:28 Starting examples/sat_encodings
Dec 15 02:10:13 Finished examples/sat_encodings                                3m45s 731MB
Dec 15 02:10:13 Starting examples/sat_encodings/case_studies
Dec 15 02:13:57 Finished examples/sat_encodings/case_studies                   3m43s   1GB
Dec 15 02:13:57 Starting examples/sat_encodings/translation
Dec 15 02:25:31 Finished examples/sat_encodings/translation                   11m33s   3GB
Dec 15 02:25:31 Starting examples/sat_encodings/translation/compilation
Dec 15 03:44:54 Finished examples/sat_encodings/translation/compilation     1h19m22s  21GB
Dec 15 03:44:54 Starting examples/deflate
Dec 15 03:46:40 Finished examples/deflate                                      1m45s 930MB
Dec 15 03:46:40 Starting examples/deflate/translation
Dec 15 03:49:35 Finished examples/deflate/translation                          2m54s   3GB
Dec 15 03:49:35 Starting examples/deflate/translation/compilation
Dec 15 04:26:20 Finished examples/deflate/translation/compilation             36m44s  17GB
Dec 15 04:26:20 Starting translator/okasaki-examples
Dec 15 04:36:10 Finished translator/okasaki-examples                           9m49s   2GB
Dec 15 04:36:10 Starting translator/other-examples
Dec 15 04:41:00 Finished translator/other-examples                             4m49s   1GB
Dec 15 04:41:01 Starting compiler/parsing/tests
Dec 15 04:42:07 Finished compiler/parsing/tests                                1m06s 772MB
Dec 15 04:42:07 Starting compiler/inference/tests
Dec 15 04:59:22 Finished compiler/inference/tests                             17m14s   3GB
Dec 15 04:59:22 Starting compiler/printing/test
Dec 15 05:06:19 Finished compiler/printing/test                                6m57s   3GB
Dec 15 05:06:20 Starting icing/flover
Dec 15 06:36:59 Finished icing/flover                                       1h30m38s   1GB
Dec 15 06:36:59 Starting icing/
Dec 15 08:50:26 Finished icing/                                             2h13m26s   7GB
Dec 15 08:50:27 Starting icing/examples
Dec 15 08:53:53 Finished icing/examples                                        3m25s   5GB
Dec 15 08:53:53 Starting compiler/repl
Dec 15 09:12:32 Finished compiler/repl                                        18m38s   4GB
Dec 15 09:12:32 Starting unverified/sexpr-bootstrap/x64/64
Dec 15 09:35:59 Finished unverified/sexpr-bootstrap/x64/64                    23m26s  12GB
Dec 15 09:35:59 Starting unverified/sexpr-bootstrap/x64/32
Dec 15 09:54:57 Finished unverified/sexpr-bootstrap/x64/32                    18m56s  13GB
Dec 15 09:54:57 Starting compiler/benchmarks
Dec 15 09:55:03 Finished compiler/benchmarks                                      6s  38MB
Dec 15 09:55:04 Starting compiler/bootstrap/compilation/x64/64
Dec 16 11:26:17 Finished compiler/bootstrap/compilation/x64/64             25h31m11s 111GB
Dec 16 11:26:17 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 16 12:09:23 Finished compiler/bootstrap/compilation/x64/64/proofs         43m05s  30GB
Dec 16 12:09:23 Starting compiler/bootstrap/compilation/x64/32
Dec 17 01:52:10 Finished compiler/bootstrap/compilation/x64/32             13h42m45s  99GB
Dec 17 01:52:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 17 01:57:46 Finished compiler/bootstrap/compilation/x64/32/proofs          5m35s  14GB
Dec 17 01:57:46 Starting compiler/bootstrap/compilation/ag32/32
Dec 17 15:48:34 Finished compiler/bootstrap/compilation/ag32/32            13h50m47s 109GB
Dec 17 15:48:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 17 16:04:26 Finished compiler/bootstrap/compilation/ag32/32/proofs        15m49s  16GB
Dec 17 16:04:26 SUCCESS