Job 1231

CakeML:e4c7de82bb84f991e4532da8a9cfe557930d1bb4
  Fix a few proof failures due to changes in HOL [May 18 20:17:13]
HOL:d0b4f135f9d0ca34127c775ce90771ace76482e8
  Fix a MULRELNORM instance: 2 * x = inv 2 * y should canonicalise [May 15 07:11:51]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

May 18 20:35:05 Claimed job
May 18 20:35:07 Reusing HOL
May 18 20:36:00 Starting developers
May 18 20:36:04 Finished developers                                               4s 104MB
May 18 20:36:04 Starting developers/bin
May 18 20:36:12 Finished developers/bin                                           7s   1GB
May 18 20:36:12 Starting semantics/ffi
May 18 20:36:23 Finished semantics/ffi                                           10s 225MB
May 18 20:36:23 Starting semantics
May 18 20:37:44 Finished semantics                                             1m21s   1GB
May 18 20:37:45 Starting semantics/proofs
May 18 20:41:16 Finished semantics/proofs                                      3m31s 970MB
May 18 20:41:16 Starting semantics/alt_semantics
May 18 20:41:25 Finished semantics/alt_semantics                                  8s 298MB
May 18 20:41:25 Starting semantics/alt_semantics/proofs
May 18 20:43:37 Finished semantics/alt_semantics/proofs                        2m11s 844MB
May 18 20:43:37 Starting basis/pure
May 18 20:44:26 Finished basis/pure                                              49s 752MB
May 18 20:44:26 Starting translator
May 18 20:47:08 Finished translator                                            2m41s   1GB
May 18 20:47:08 Starting compiler/parsing
May 18 20:48:21 Finished compiler/parsing                                      1m12s   2GB
May 18 20:48:21 Starting characteristic
May 18 20:54:24 Finished characteristic                                        6m03s   2GB
May 18 20:54:24 Starting translator/monadic
May 18 20:56:00 Finished translator/monadic                                    1m35s   1GB
May 18 20:56:01 Starting basis
May 18 21:29:45 Finished basis                                                33m44s  11GB
May 18 21:29:45 Starting compiler/inference
May 18 21:30:47 Finished compiler/inference                                    1m02s   1GB
May 18 21:30:48 Starting compiler/backend/reg_alloc
May 18 21:31:50 Finished compiler/backend/reg_alloc                            1m02s   1GB
May 18 21:31:50 Starting compiler/backend/gc
May 18 21:35:11 Finished compiler/backend/gc                                   3m20s   2GB
May 18 21:35:11 Starting compiler/backend
May 18 21:39:50 Finished compiler/backend                                      4m38s   3GB
May 18 21:39:50 Starting compiler/encoders/asm
May 18 21:40:12 Finished compiler/encoders/asm                                   22s 729MB
May 18 21:40:13 Starting compiler/encoders/x64
May 18 21:40:38 Finished compiler/encoders/x64                                   25s   1GB
May 18 21:40:39 Starting compiler/encoders/arm7
May 18 21:41:31 Finished compiler/encoders/arm7                                  52s   1GB
May 18 21:41:31 Starting compiler/encoders/arm8
May 18 21:41:45 Finished compiler/encoders/arm8                                  13s 899MB
May 18 21:41:45 Starting compiler/encoders/mips
May 18 21:42:02 Finished compiler/encoders/mips                                  17s   1GB
May 18 21:42:03 Starting compiler/encoders/riscv
May 18 21:42:18 Finished compiler/encoders/riscv                                 14s 874MB
May 18 21:42:18 Starting compiler/encoders/ag32
May 18 21:42:35 Finished compiler/encoders/ag32                                  17s 822MB
May 18 21:42:36 Starting compiler/backend/x64
May 18 21:42:53 Finished compiler/backend/x64                                    17s 927MB
May 18 21:42:53 Starting compiler/backend/arm7
May 18 21:43:14 Finished compiler/backend/arm7                                   20s   1GB
May 18 21:43:14 Starting compiler/backend/arm8
May 18 21:43:32 Finished compiler/backend/arm8                                   18s   1GB
May 18 21:43:33 Starting compiler/backend/mips
May 18 21:43:53 Finished compiler/backend/mips                                   19s   1GB
May 18 21:43:53 Starting compiler/backend/riscv
May 18 21:44:12 Finished compiler/backend/riscv                                  18s   1GB
May 18 21:44:12 Starting compiler/backend/ag32
May 18 21:45:24 Finished compiler/backend/ag32                                 1m11s   1GB
May 18 21:45:24 Starting compiler/parsing/proofs
May 18 21:51:11 Finished compiler/parsing/proofs                               5m47s 962MB
May 18 21:51:11 Starting compiler/inference/proofs
May 18 21:53:46 Finished compiler/inference/proofs                             2m34s 898MB
May 18 21:53:46 Starting compiler/backend/semantics
May 18 22:25:13 Finished compiler/backend/semantics                           31m25s   2GB
May 18 22:25:13 Starting compiler/backend/reg_alloc/proofs
May 18 22:28:54 Finished compiler/backend/reg_alloc/proofs                     3m40s 937MB
May 18 22:28:54 Starting compiler/backend/proofs
May 18 23:36:47 Finished compiler/backend/proofs                            1h07m52s  12GB
May 18 23:36:47 Starting compiler/encoders/x64/proofs
May 18 23:46:49 Finished compiler/encoders/x64/proofs                         10m01s   4GB
May 18 23:46:49 Starting compiler/encoders/arm7/proofs
May 19 00:00:15 Finished compiler/encoders/arm7/proofs                        13m25s   4GB
May 19 00:00:15 Starting compiler/encoders/arm8/proofs
May 19 00:07:07 Finished compiler/encoders/arm8/proofs                         6m51s   1GB
May 19 00:07:07 Starting compiler/encoders/mips/proofs
May 19 00:17:35 Finished compiler/encoders/mips/proofs                        10m27s   2GB
May 19 00:17:35 Starting compiler/encoders/riscv/proofs
May 19 00:26:44 Finished compiler/encoders/riscv/proofs                        9m08s 965MB
May 19 00:26:44 Starting compiler/encoders/ag32/proofs
May 19 00:29:30 Finished compiler/encoders/ag32/proofs                         2m43s 689MB
May 19 00:29:30 Starting compiler/backend/x64/proofs
May 19 00:29:51 Finished compiler/backend/x64/proofs                             20s   1GB
May 19 00:29:51 Starting compiler/backend/arm7/proofs
May 19 00:30:14 Finished compiler/backend/arm7/proofs                            22s   1GB
May 19 00:30:14 Starting compiler/backend/arm8/proofs
May 19 00:30:34 Finished compiler/backend/arm8/proofs                            20s   1GB
May 19 00:30:34 Starting compiler/backend/mips/proofs
May 19 00:30:56 Finished compiler/backend/mips/proofs                            21s   1GB
May 19 00:30:56 Starting compiler/backend/riscv/proofs
May 19 00:31:17 Finished compiler/backend/riscv/proofs                           21s   1GB
May 19 00:31:17 Starting compiler/backend/ag32/proofs
May 19 00:44:54 Finished compiler/backend/ag32/proofs                         13m36s   2GB
May 19 00:44:54 Starting compiler/proofs
May 19 00:46:24 Finished compiler/proofs                                       1m30s   2GB
May 19 00:46:25 Starting candle/set-theory
May 19 00:46:54 Finished candle/set-theory                                       28s   1GB
May 19 00:46:54 Starting candle/syntax-lib
May 19 00:47:05 Finished candle/syntax-lib                                       10s 684MB
May 19 00:47:05 Starting candle/standard/syntax
May 19 00:48:57 Finished candle/standard/syntax                                1m52s 927MB
May 19 00:48:58 Starting candle/standard/semantics
May 19 00:50:43 Finished candle/standard/semantics                             1m44s   1GB
May 19 00:50:43 Starting candle/standard/monadic
May 19 00:52:28 Finished candle/standard/monadic                               1m45s   1GB
May 19 00:52:28 Starting candle/standard/ml_kernel
May 19 00:58:08 Finished candle/standard/ml_kernel                             5m39s   3GB
May 19 00:58:08 Starting candle/standard/opentheory
May 19 01:07:35 Finished candle/standard/opentheory                            9m27s   5GB
May 19 01:07:36 Starting candle/standard/opentheory/compilation
May 19 01:38:59 Finished candle/standard/opentheory/compilation               31m23s  12GB
May 19 01:39:00 Starting candle/standard/opentheory/compilation/proofs
May 19 01:39:37 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
May 19 01:39:38 Starting candle/overloading/syntax
May 19 01:42:49 Finished candle/overloading/syntax                             3m11s   1GB
May 19 01:42:49 Starting candle/overloading/semantics
May 19 01:50:05 Finished candle/overloading/semantics                          7m16s   2GB
May 19 01:50:05 Starting characteristic/examples
May 19 01:51:23 Finished characteristic/examples                               1m17s   2GB
May 19 01:51:23 Starting tutorial/solutions
May 19 02:06:05 Finished tutorial/solutions                                   14m41s   7GB
May 19 02:06:05 Starting translator/monadic/examples
May 19 02:09:11 Finished translator/monadic/examples                           3m06s   2GB
May 19 02:09:11 Starting examples
May 19 02:17:40 Finished examples                                              8m29s   3GB
May 19 02:17:40 Starting examples/compilation/x64
May 19 04:33:34 Finished examples/compilation/x64                           2h15m53s  12GB
May 19 04:33:34 Starting examples/compilation/x64/proofs
May 19 04:35:04 Finished examples/compilation/x64/proofs                       1m29s   3GB
May 19 04:35:04 Starting examples/compilation/ag32
May 19 05:06:13 Finished examples/compilation/ag32                            31m07s   6GB
May 19 05:06:13 Starting examples/compilation/ag32/proofs
May 19 05:07:02 Finished examples/compilation/ag32/proofs                        48s   3GB
May 19 05:07:02 Starting examples/cost
May 19 05:50:30 Finished examples/cost                                        43m27s   6GB
May 19 05:50:30 Starting examples/lpr_checker
May 19 05:54:23 Finished examples/lpr_checker                                  3m52s   3GB
May 19 05:54:23 Starting examples/lpr_checker/compilation
May 19 06:11:39 Finished examples/lpr_checker/compilation                     17m15s   8GB
May 19 06:11:39 Starting examples/lpr_checker/compilation/proofs
May 19 06:12:17 Finished examples/lpr_checker/compilation/proofs                 37s   3GB
May 19 06:12:17 Starting examples/lpr_checker/array
May 19 06:22:53 Finished examples/lpr_checker/array                           10m36s   2GB
May 19 06:22:54 Starting examples/lpr_checker/array/compilation
May 19 06:41:09 Finished examples/lpr_checker/array/compilation               18m14s  10GB
May 19 06:41:09 Starting examples/lpr_checker/array/compilation/proofs
May 19 06:41:58 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
May 19 06:41:58 Starting translator/okasaki-examples
May 19 06:46:23 Finished translator/okasaki-examples                           4m24s   1GB
May 19 06:46:23 Starting translator/other-examples
May 19 06:48:22 Finished translator/other-examples                             1m59s   1GB
May 19 06:48:23 Starting compiler/parsing/tests
May 19 06:48:48 Finished compiler/parsing/tests                                  25s 570MB
May 19 06:48:48 Starting compiler/inference/tests
May 19 06:53:22 Finished compiler/inference/tests                              4m33s   2GB
May 19 06:53:22 Starting compiler/bootstrap/translation
May 19 09:39:47 Finished compiler/bootstrap/translation                     2h46m24s  38GB
May 19 09:39:47 Starting unverified/sexpr-bootstrap/x64/64
May 19 09:53:43 Finished unverified/sexpr-bootstrap/x64/64                    13m55s   4GB
May 19 09:53:43 Starting unverified/sexpr-bootstrap/x64/32
May 19 10:03:46 Finished unverified/sexpr-bootstrap/x64/32                    10m02s   7GB
May 19 10:03:46 Starting compiler/benchmarks
May 19 10:03:48 Finished compiler/benchmarks                                      1s  37MB
May 19 10:03:48 Starting compiler/bootstrap/compilation/x64/64
May 20 01:22:23 Finished compiler/bootstrap/compilation/x64/64             15h18m34s  64GB
May 20 01:22:24 Starting compiler/bootstrap/compilation/x64/64/proofs
May 20 01:25:38 Finished compiler/bootstrap/compilation/x64/64/proofs          3m14s  14GB
May 20 01:25:38 Starting compiler/bootstrap/compilation/x64/32
May 20 14:30:26 Finished compiler/bootstrap/compilation/x64/32             13h04m47s  64GB
May 20 14:30:26 Starting compiler/bootstrap/compilation/x64/32/proofs
May 20 14:33:27 Finished compiler/bootstrap/compilation/x64/32/proofs          3m01s  12GB
May 20 14:33:28 Starting compiler/bootstrap/compilation/ag32/32
May 21 05:27:59 Finished compiler/bootstrap/compilation/ag32/32            14h54m31s  64GB
May 21 05:27:59 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 21 05:47:20 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m20s  31GB
May 21 05:47:20 SUCCESS