Job 2058

CakeML:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:cf37a2b2a4f27c3748bb4bb8738c08373abde4c3
  Update PropLogic example to use modern syntax [Nov 30 09:32:01]
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 04 13:07:41 Claimed job
Dec 04 13:07:50 Building HOL
Dec 04 13:30:50 Starting developers
Dec 04 13:30:59 Finished developers                                               8s  98MB
Dec 04 13:30:59 Starting developers/bin
Dec 04 13:31:12 Finished developers/bin                                          12s   1GB
Dec 04 13:31:12 Starting compiler/proofs
Dec 04 17:02:06 Finished compiler/proofs                                    3h30m53s  14GB
Dec 04 17:02:06 Starting compiler/bootstrap/translation
Dec 05 03:30:01 Finished compiler/bootstrap/translation                    10h27m54s  66GB
Dec 05 03:30:01 Starting semantics/ffi
Dec 05 03:30:08 Finished semantics/ffi                                            7s 228MB
Dec 05 03:30:09 Starting semantics
Dec 05 03:30:11 Finished semantics                                                2s  34MB
Dec 05 03:30:11 Starting semantics/proofs
Dec 05 03:31:31 Finished semantics/proofs                                      1m19s 992MB
Dec 05 03:31:31 Starting semantics/alt_semantics
Dec 05 03:32:31 Finished semantics/alt_semantics                                 59s 550MB
Dec 05 03:32:31 Starting semantics/alt_semantics/proofs
Dec 05 03:58:12 Finished semantics/alt_semantics/proofs                       25m40s   1GB
Dec 05 03:58:13 Starting basis/pure
Dec 05 03:58:15 Finished basis/pure                                               2s  33MB
Dec 05 03:58:15 Starting translator
Dec 05 04:01:58 Finished translator                                            3m42s   1GB
Dec 05 04:01:58 Starting compiler/parsing
Dec 05 04:02:00 Finished compiler/parsing                                         2s  17MB
Dec 05 04:02:01 Starting characteristic
Dec 05 04:02:04 Finished characteristic                                           3s  21MB
Dec 05 04:02:04 Starting translator/monadic
Dec 05 04:02:08 Finished translator/monadic                                       2s  25MB
Dec 05 04:02:08 Starting basis
Dec 05 04:09:34 Finished basis                                                 7m25s   2GB
Dec 05 04:09:34 Starting compiler/inference
Dec 05 04:09:37 Finished compiler/inference                                       2s  26MB
Dec 05 04:09:37 Starting compiler/backend/reg_alloc
Dec 05 04:09:39 Finished compiler/backend/reg_alloc                               2s  18MB
Dec 05 04:09:39 Starting compiler/backend/gc
Dec 05 04:09:43 Finished compiler/backend/gc                                      3s  32MB
Dec 05 04:09:44 Starting compiler/backend
Dec 05 04:10:07 Finished compiler/backend                                        23s 593MB
Dec 05 04:10:07 Starting compiler/encoders/asm
Dec 05 04:10:10 Finished compiler/encoders/asm                                    2s  29MB
Dec 05 04:10:10 Starting compiler/encoders/x64
Dec 05 04:10:13 Finished compiler/encoders/x64                                    2s  28MB
Dec 05 04:10:14 Starting compiler/encoders/arm7
Dec 05 04:10:17 Finished compiler/encoders/arm7                                   2s  32MB
Dec 05 04:10:17 Starting compiler/encoders/arm8
Dec 05 04:10:20 Finished compiler/encoders/arm8                                   2s  26MB
Dec 05 04:10:20 Starting compiler/encoders/arm8_asl
Dec 05 08:34:49 Finished compiler/encoders/arm8_asl                         4h24m28s  45GB
Dec 05 08:34:49 Starting compiler/encoders/mips
Dec 05 08:34:52 Finished compiler/encoders/mips                                   2s  28MB
Dec 05 08:34:52 Starting compiler/encoders/riscv
Dec 05 08:34:55 Finished compiler/encoders/riscv                                  2s  30MB
Dec 05 08:34:56 Starting compiler/encoders/ag32
Dec 05 08:34:58 Finished compiler/encoders/ag32                                   2s  23MB
Dec 05 08:34:59 Starting compiler/backend/x64
Dec 05 08:35:02 Finished compiler/backend/x64                                     3s  33MB
Dec 05 08:35:03 Starting compiler/backend/arm7
Dec 05 08:35:06 Finished compiler/backend/arm7                                    3s  38MB
Dec 05 08:35:06 Starting compiler/backend/arm8
Dec 05 08:35:10 Finished compiler/backend/arm8                                    3s  28MB
Dec 05 08:35:10 Starting compiler/backend/mips
Dec 05 08:35:14 Finished compiler/backend/mips                                    3s  32MB
Dec 05 08:35:14 Starting compiler/backend/riscv
Dec 05 08:35:18 Finished compiler/backend/riscv                                   3s  46MB
Dec 05 08:35:18 Starting compiler/backend/ag32
Dec 05 08:38:20 Finished compiler/backend/ag32                                 3m01s   1GB
Dec 05 08:38:20 Starting compiler/parsing/proofs
Dec 05 08:38:23 Finished compiler/parsing/proofs                                  2s  24MB
Dec 05 08:38:23 Starting compiler/inference/proofs
Dec 05 08:38:26 Finished compiler/inference/proofs                                2s  32MB
Dec 05 08:38:27 Starting compiler/backend/semantics
Dec 05 08:40:50 Finished compiler/backend/semantics                            2m23s   1GB
Dec 05 08:40:51 Starting compiler/backend/reg_alloc/proofs
Dec 05 08:40:54 Finished compiler/backend/reg_alloc/proofs                        3s  26MB
Dec 05 08:40:54 Starting compiler/backend/proofs
Dec 05 08:42:50 Finished compiler/backend/proofs                               1m55s   2GB
Dec 05 08:42:51 Starting compiler/backend/serialiser
Dec 05 08:42:56 Finished compiler/backend/serialiser                              5s  53MB
Dec 05 08:42:56 Starting compiler/encoders/x64/proofs
Dec 05 09:05:07 Finished compiler/encoders/x64/proofs                         22m10s   4GB
Dec 05 09:05:08 Starting compiler/encoders/arm7/proofs
Dec 05 09:35:36 Finished compiler/encoders/arm7/proofs                        30m26s   3GB
Dec 05 09:35:36 Starting compiler/encoders/arm8/proofs
Dec 05 09:51:36 Finished compiler/encoders/arm8/proofs                        16m00s   1GB
Dec 05 09:51:36 Starting compiler/encoders/arm8_asl/proofs
Dec 05 11:47:03 Finished compiler/encoders/arm8_asl/proofs                  1h55m26s   5GB
Dec 05 11:47:04 Starting compiler/encoders/mips/proofs
Dec 05 12:11:42 Finished compiler/encoders/mips/proofs                        24m38s   2GB
Dec 05 12:11:43 Starting compiler/encoders/riscv/proofs
Dec 05 12:31:59 Finished compiler/encoders/riscv/proofs                       20m15s   1GB
Dec 05 12:31:59 Starting compiler/encoders/ag32/proofs
Dec 05 12:37:54 Finished compiler/encoders/ag32/proofs                         5m54s 852MB
Dec 05 12:37:55 Starting compiler/backend/x64/proofs
Dec 05 12:38:49 Finished compiler/backend/x64/proofs                             54s   1GB
Dec 05 12:38:50 Starting compiler/backend/arm7/proofs
Dec 05 12:39:46 Finished compiler/backend/arm7/proofs                            55s   1GB
Dec 05 12:39:46 Starting compiler/backend/arm8/proofs
Dec 05 12:40:43 Finished compiler/backend/arm8/proofs                            56s   1GB
Dec 05 12:40:43 Starting compiler/backend/arm8_asl
Dec 05 12:41:27 Finished compiler/backend/arm8_asl                               43s   1GB
Dec 05 12:41:27 Starting compiler/backend/mips/proofs
Dec 05 12:42:24 Finished compiler/backend/mips/proofs                            56s   1GB
Dec 05 12:42:24 Starting compiler/backend/riscv/proofs
Dec 05 12:43:20 Finished compiler/backend/riscv/proofs                           55s   1GB
Dec 05 12:43:20 Starting compiler/backend/ag32/proofs
Dec 05 13:13:32 Finished compiler/backend/ag32/proofs                         30m11s   2GB
Dec 05 13:13:32 Starting candle/set-theory
Dec 05 13:14:41 Finished candle/set-theory                                     1m07s   1GB
Dec 05 13:14:41 Starting candle/syntax-lib
Dec 05 13:14:43 Finished candle/syntax-lib                                        2s  17MB
Dec 05 13:14:44 Starting candle/standard/syntax
Dec 05 13:15:03 Finished candle/standard/syntax                                  19s 559MB
Dec 05 13:15:03 Starting candle/standard/semantics
Dec 05 13:18:53 Finished candle/standard/semantics                             3m49s   1GB
Dec 05 13:18:53 Starting candle/standard/monadic
Dec 05 13:18:56 Finished candle/standard/monadic                                  3s  32MB
Dec 05 13:18:56 Starting candle/standard/ml_kernel
Dec 05 13:21:56 Finished candle/standard/ml_kernel                             2m59s   2GB
Dec 05 13:21:56 Starting candle/overloading/syntax
Dec 05 13:28:51 Finished candle/overloading/syntax                             6m54s 982MB
Dec 05 13:28:51 Starting candle/overloading/semantics
Dec 05 13:55:01 Finished candle/overloading/semantics                         26m09s   3GB
Dec 05 13:55:01 Starting candle/overloading/monadic
Dec 05 14:00:35 Finished candle/overloading/monadic                            5m34s   1GB
Dec 05 14:00:36 Starting candle/overloading/ml_kernel
Dec 05 14:15:56 Finished candle/overloading/ml_kernel                         15m19s   3GB
Dec 05 14:15:56 Starting candle/overloading/ml_checker
Dec 05 14:21:21 Finished candle/overloading/ml_checker                         5m25s   3GB
Dec 05 14:21:22 Starting candle/prover
Dec 05 14:43:24 Finished candle/prover                                        22m02s   2GB
Dec 05 14:43:25 Starting pancake
Dec 05 14:50:30 Finished pancake                                               7m04s   4GB
Dec 05 14:50:30 Starting pancake/ffi
Dec 05 14:50:31 Finished pancake/ffi                                              0s  12MB
Dec 05 14:50:31 Starting pancake/semantics
Dec 05 14:55:43 Finished pancake/semantics                                     5m12s   1GB
Dec 05 14:55:44 Starting pancake/proofs
Dec 05 15:02:02 Finished pancake/proofs                                        6m18s   1GB
Dec 05 15:02:03 Starting characteristic/examples
Dec 05 15:05:04 Finished characteristic/examples                               3m01s   3GB
Dec 05 15:05:05 Starting tutorial/solutions
Dec 05 15:37:50 Finished tutorial/solutions                                   32m45s   8GB
Dec 05 15:37:50 Starting translator/monadic/examples
Dec 05 15:44:25 Finished translator/monadic/examples                           6m34s   3GB
Dec 05 15:44:26 Starting examples
Dec 05 16:03:44 Finished examples                                             19m17s   3GB
Dec 05 16:03:44 Starting examples/compilation/x64
Dec 05 20:23:30 Finished examples/compilation/x64                           4h19m45s  19GB
Dec 05 20:23:30 Starting examples/compilation/x64/proofs
Dec 05 20:27:35 Finished examples/compilation/x64/proofs                       4m04s   3GB
Dec 05 20:27:35 Starting examples/compilation/ag32
Dec 05 21:33:35 Finished examples/compilation/ag32                          1h05m58s   8GB
Dec 05 21:33:35 Starting examples/compilation/ag32/proofs
Dec 05 21:35:13 Finished examples/compilation/ag32/proofs                      1m38s   3GB
Dec 05 21:35:13 Starting examples/compilation/to_word
Dec 05 21:42:02 Finished examples/compilation/to_word                          6m48s   6GB
Dec 05 21:42:02 Starting examples/lpr_checker
Dec 05 21:44:02 Finished examples/lpr_checker                                  1m59s   1GB
Dec 05 21:44:02 Starting examples/lpr_checker/array
Dec 05 23:03:58 Finished examples/lpr_checker/array                         1h19m55s   5GB
Dec 05 23:03:58 Starting examples/lpr_checker/array/compilation
Dec 06 00:24:04 Finished examples/lpr_checker/array/compilation             1h20m04s  39GB
Dec 06 00:24:04 Starting examples/lpr_checker/array/compilation/proofs
Dec 06 00:26:53 Finished examples/lpr_checker/array/compilation/proofs         2m49s   6GB
Dec 06 00:26:54 Starting examples/opentheory
Dec 06 00:49:15 Finished examples/opentheory                                  22m21s   5GB
Dec 06 00:49:15 Starting examples/opentheory
Dec 06 00:49:19 Finished examples/opentheory                                      3s  32MB
Dec 06 00:49:19 Starting examples/opentheory/compilation
Dec 06 02:10:03 Finished examples/opentheory/compilation                    1h20m43s  28GB
Dec 06 02:10:03 Starting examples/opentheory/compilation/proofs
Dec 06 02:11:38 Finished examples/opentheory/compilation/proofs                1m34s   3GB
Dec 06 02:11:38 Starting examples/opentheory/compilation/ag32
Dec 06 03:29:36 Finished examples/opentheory/compilation/ag32               1h17m57s  41GB
Dec 06 03:29:36 Starting examples/opentheory/compilation/ag32/proofs
Dec 06 03:33:09 Finished examples/opentheory/compilation/ag32/proofs           3m31s   6GB
Dec 06 03:33:09 Starting examples/sat_encodings
Dec 06 03:37:03 Finished examples/sat_encodings                                3m53s 701MB
Dec 06 03:37:03 Starting examples/sat_encodings/case_studies
Dec 06 03:40:28 Finished examples/sat_encodings/case_studies                   3m24s 945MB
Dec 06 03:40:28 Starting examples/sat_encodings/translation
Dec 06 03:52:16 Finished examples/sat_encodings/translation                   11m48s   5GB
Dec 06 03:52:16 Starting examples/sat_encodings/translation/compilation
Dec 06 05:13:00 Finished examples/sat_encodings/translation/compilation     1h20m42s  21GB
Dec 06 05:13:00 Starting examples/deflate
Dec 06 05:14:45 Finished examples/deflate                                      1m45s 831MB
Dec 06 05:14:45 Starting examples/deflate/translation
Dec 06 05:17:58 Finished examples/deflate/translation                          3m12s   3GB
Dec 06 05:17:58 Starting examples/deflate/translation/compilation
Dec 06 05:55:55 Finished examples/deflate/translation/compilation             37m56s  17GB
Dec 06 05:55:56 Starting translator/okasaki-examples
Dec 06 06:05:49 Finished translator/okasaki-examples                           9m52s   2GB
Dec 06 06:05:49 Starting translator/other-examples
Dec 06 06:10:37 Finished translator/other-examples                             4m47s   1GB
Dec 06 06:10:37 Starting compiler/parsing/tests
Dec 06 06:11:42 Finished compiler/parsing/tests                                1m05s 669MB
Dec 06 06:11:43 Starting compiler/inference/tests
Dec 06 06:28:15 Finished compiler/inference/tests                             16m31s   5GB
Dec 06 06:28:15 Starting compiler/printing/test
Dec 06 06:35:12 Finished compiler/printing/test                                6m56s   3GB
Dec 06 06:35:12 Starting icing/flover
Dec 06 08:07:05 Finished icing/flover                                       1h31m52s   1GB
Dec 06 08:07:05 Starting icing/
Dec 06 10:20:53 Finished icing/                                             2h13m47s   7GB
Dec 06 10:20:53 Starting icing/examples
Dec 06 10:24:02 Finished icing/examples                                        3m08s   3GB
Dec 06 10:24:02 Starting compiler/repl
Dec 06 10:42:22 Finished compiler/repl                                        18m19s   4GB
Dec 06 10:42:23 Starting unverified/sexpr-bootstrap/x64/64
Dec 06 11:05:45 Finished unverified/sexpr-bootstrap/x64/64                    23m21s  14GB
Dec 06 11:05:45 Starting unverified/sexpr-bootstrap/x64/32
Dec 06 11:24:32 Finished unverified/sexpr-bootstrap/x64/32                    18m45s  12GB
Dec 06 11:24:32 Starting compiler/benchmarks
Dec 06 11:24:39 Finished compiler/benchmarks                                      6s  38MB
Dec 06 11:24:39 Starting compiler/bootstrap/compilation/x64/64
Dec 07 13:18:23 Finished compiler/bootstrap/compilation/x64/64             25h53m43s 110GB
Dec 07 13:18:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 07 13:59:34 Finished compiler/bootstrap/compilation/x64/64/proofs         41m10s  23GB
Dec 07 13:59:35 Starting compiler/bootstrap/compilation/x64/32
Dec 08 04:08:51 Finished compiler/bootstrap/compilation/x64/32             14h09m15s  84GB
Dec 08 04:08:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 08 04:14:02 Finished compiler/bootstrap/compilation/x64/32/proofs          5m10s  15GB
Dec 08 04:14:02 Starting compiler/bootstrap/compilation/ag32/32
Dec 08 18:36:16 Finished compiler/bootstrap/compilation/ag32/32            14h22m13s 109GB
Dec 08 18:36:16 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 08 18:48:36 Finished compiler/bootstrap/compilation/ag32/32/proofs        12m20s  30GB
Dec 08 18:48:37 SUCCESS