Job 1230

CakeML:126109fde48f06518350d201ec6e93771b1adecc
  Add tight bounds for data_safe_lcgLoop [May 16 13:08:53]
#736 (data-cost)
Merging into: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 18 20:17:29 Claimed job
May 18 20:17:31 Reusing HOL
May 18 20:17:41 Starting developers
May 18 20:17:42 Finished developers                                               0s  30MB
May 18 20:17:42 Starting developers/bin
May 18 20:17:48 Finished developers/bin                                           6s   1GB
May 18 20:17:48 Starting semantics/ffi
May 18 20:17:57 Finished semantics/ffi                                            8s 231MB
May 18 20:17:57 Starting semantics
May 18 20:19:14 Finished semantics                                             1m17s   1GB
May 18 20:19:15 Starting semantics/proofs
May 18 20:22:24 Finished semantics/proofs                                      3m09s 904MB
May 18 20:22:24 Starting semantics/alt_semantics
May 18 20:22:31 Finished semantics/alt_semantics                                  6s 346MB
May 18 20:22:31 Starting semantics/alt_semantics/proofs
May 18 20:24:35 Finished semantics/alt_semantics/proofs                        2m02s 836MB
May 18 20:24:35 Starting basis/pure
May 18 20:25:22 Finished basis/pure                                              47s 676MB
May 18 20:25:23 Starting translator
May 18 20:27:56 Finished translator                                            2m33s   1GB
May 18 20:27:56 Starting compiler/parsing
May 18 20:29:03 Finished compiler/parsing                                      1m06s   3GB
May 18 20:29:03 Starting characteristic
May 18 20:34:45 Finished characteristic                                        5m41s   1GB
May 18 20:34:45 Starting translator/monadic
May 18 20:36:17 Finished translator/monadic                                    1m31s   1GB
May 18 20:36:17 Starting basis
May 18 21:06:53 Finished basis                                                30m35s  18GB
May 18 21:06:53 Starting compiler/inference
May 18 21:07:52 Finished compiler/inference                                      58s   1GB
May 18 21:07:52 Starting compiler/backend/reg_alloc
May 18 21:08:53 Finished compiler/backend/reg_alloc                            1m00s   1GB
May 18 21:08:53 Starting compiler/backend/gc
May 18 21:11:58 Finished compiler/backend/gc                                   3m05s   2GB
May 18 21:11:59 Starting compiler/backend
May 18 21:16:25 Finished compiler/backend                                      4m26s   3GB
May 18 21:16:26 Starting compiler/encoders/asm
May 18 21:16:46 Finished compiler/encoders/asm                                   20s 856MB
May 18 21:16:47 Starting compiler/encoders/x64
May 18 21:17:11 Finished compiler/encoders/x64                                   23s 885MB
May 18 21:17:11 Starting compiler/encoders/arm7
May 18 21:18:05 Finished compiler/encoders/arm7                                  54s 894MB
May 18 21:18:05 Starting compiler/encoders/arm8
May 18 21:18:17 Finished compiler/encoders/arm8                                  11s 917MB
May 18 21:18:18 Starting compiler/encoders/mips
May 18 21:18:34 Finished compiler/encoders/mips                                  15s   1GB
May 18 21:18:34 Starting compiler/encoders/riscv
May 18 21:18:49 Finished compiler/encoders/riscv                                 15s 969MB
May 18 21:18:49 Starting compiler/encoders/ag32
May 18 21:19:05 Finished compiler/encoders/ag32                                  16s 752MB
May 18 21:19:06 Starting compiler/backend/x64
May 18 21:19:23 Finished compiler/backend/x64                                    17s   1GB
May 18 21:19:23 Starting compiler/backend/arm7
May 18 21:19:41 Finished compiler/backend/arm7                                   18s   1GB
May 18 21:19:41 Starting compiler/backend/arm8
May 18 21:20:00 Finished compiler/backend/arm8                                   17s   1GB
May 18 21:20:00 Starting compiler/backend/mips
May 18 21:20:18 Finished compiler/backend/mips                                   18s   1GB
May 18 21:20:18 Starting compiler/backend/riscv
May 18 21:20:37 Finished compiler/backend/riscv                                  18s   1GB
May 18 21:20:37 Starting compiler/backend/ag32
May 18 21:21:45 Finished compiler/backend/ag32                                 1m08s 923MB
May 18 21:21:46 Starting compiler/parsing/proofs
May 18 21:27:29 Finished compiler/parsing/proofs                               5m43s   1GB
May 18 21:27:29 Starting compiler/inference/proofs
May 18 21:29:52 Finished compiler/inference/proofs                             2m22s 921MB
May 18 21:29:52 Starting compiler/backend/semantics
May 18 21:57:16 Finished compiler/backend/semantics                           27m23s   1GB
May 18 21:57:16 Starting compiler/backend/reg_alloc/proofs
May 18 22:00:38 Finished compiler/backend/reg_alloc/proofs                     3m21s 815MB
May 18 22:00:38 Starting compiler/backend/proofs
May 18 23:01:15 Finished compiler/backend/proofs                            1h00m36s  22GB
May 18 23:01:15 Starting compiler/encoders/x64/proofs
May 18 23:10:31 Finished compiler/encoders/x64/proofs                          9m15s   4GB
May 18 23:10:31 Starting compiler/encoders/arm7/proofs
May 18 23:22:52 Finished compiler/encoders/arm7/proofs                        12m21s   3GB
May 18 23:22:52 Starting compiler/encoders/arm8/proofs
May 18 23:29:09 Finished compiler/encoders/arm8/proofs                         6m15s   1GB
May 18 23:29:09 Starting compiler/encoders/mips/proofs
May 18 23:38:54 Finished compiler/encoders/mips/proofs                         9m44s   2GB
May 18 23:38:54 Starting compiler/encoders/riscv/proofs
May 18 23:47:19 Finished compiler/encoders/riscv/proofs                        8m24s   1GB
May 18 23:47:19 Starting compiler/encoders/ag32/proofs
May 18 23:49:46 Finished compiler/encoders/ag32/proofs                         2m27s 831MB
May 18 23:49:46 Starting compiler/backend/x64/proofs
May 18 23:50:06 Finished compiler/backend/x64/proofs                             19s   1GB
May 18 23:50:06 Starting compiler/backend/arm7/proofs
May 18 23:50:27 Finished compiler/backend/arm7/proofs                            20s   1GB
May 18 23:50:27 Starting compiler/backend/arm8/proofs
May 18 23:50:48 Finished compiler/backend/arm8/proofs                            20s 812MB
May 18 23:50:48 Starting compiler/backend/mips/proofs
May 18 23:51:08 Finished compiler/backend/mips/proofs                            20s   1GB
May 18 23:51:08 Starting compiler/backend/riscv/proofs
May 18 23:51:28 Finished compiler/backend/riscv/proofs                           19s   1GB
May 18 23:51:28 Starting compiler/backend/ag32/proofs
May 19 00:03:44 Finished compiler/backend/ag32/proofs                         12m15s   2GB
May 19 00:03:44 Starting compiler/proofs
May 19 00:05:10 Finished compiler/proofs                                       1m25s   3GB
May 19 00:05:10 Starting candle/set-theory
May 19 00:05:37 Finished candle/set-theory                                       26s 770MB
May 19 00:05:37 Starting candle/syntax-lib
May 19 00:05:46 Finished candle/syntax-lib                                        9s 477MB
May 19 00:05:46 Starting candle/standard/syntax
May 19 00:07:31 Finished candle/standard/syntax                                1m44s   1GB
May 19 00:07:32 Starting candle/standard/semantics
May 19 00:09:11 Finished candle/standard/semantics                             1m39s   1GB
May 19 00:09:12 Starting candle/standard/monadic
May 19 00:10:49 Finished candle/standard/monadic                               1m37s   1GB
May 19 00:10:49 Starting candle/standard/ml_kernel
May 19 00:15:58 Finished candle/standard/ml_kernel                             5m08s   3GB
May 19 00:15:58 Starting candle/standard/opentheory
May 19 00:24:45 Finished candle/standard/opentheory                            8m46s   4GB
May 19 00:24:45 Starting candle/standard/opentheory/compilation
May 19 00:56:01 Finished candle/standard/opentheory/compilation               31m16s  17GB
May 19 00:56:02 Starting candle/standard/opentheory/compilation/proofs
May 19 00:56:37 Finished candle/standard/opentheory/compilation/proofs           35s   3GB
May 19 00:56:38 Starting candle/overloading/syntax
May 19 00:59:36 Finished candle/overloading/syntax                             2m58s   1GB
May 19 00:59:36 Starting candle/overloading/semantics
May 19 01:06:24 Finished candle/overloading/semantics                          6m47s   3GB
May 19 01:06:24 Starting characteristic/examples
May 19 01:07:36 Finished characteristic/examples                               1m11s   3GB
May 19 01:07:36 Starting tutorial/solutions
May 19 01:21:22 Finished tutorial/solutions                                   13m46s   5GB
May 19 01:21:22 Starting translator/monadic/examples
May 19 01:24:23 Finished translator/monadic/examples                           3m01s   2GB
May 19 01:24:23 Starting examples
May 19 01:32:37 Finished examples                                              8m12s   5GB
May 19 01:32:37 Starting examples/compilation/x64
May 19 03:46:10 Finished examples/compilation/x64                           2h13m32s  13GB
May 19 03:46:10 Starting examples/compilation/x64/proofs
May 19 03:47:44 Finished examples/compilation/x64/proofs                       1m33s   2GB
May 19 03:47:44 Starting examples/compilation/ag32
May 19 04:18:02 Finished examples/compilation/ag32                            30m17s   7GB
May 19 04:18:02 Starting examples/compilation/ag32/proofs
May 19 04:18:44 Finished examples/compilation/ag32/proofs                        41s   2GB
May 19 04:18:44 Starting examples/cost
May 19 05:05:24 Finished examples/cost                                        46m39s   8GB
May 19 05:05:24 Starting examples/lpr_checker
May 19 05:09:01 Finished examples/lpr_checker                                  3m37s   2GB
May 19 05:09:01 Starting examples/lpr_checker/compilation
May 19 05:25:56 Finished examples/lpr_checker/compilation                     16m54s  14GB
May 19 05:25:56 Starting examples/lpr_checker/compilation/proofs
May 19 05:26:34 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
May 19 05:26:34 Starting examples/lpr_checker/array
May 19 05:36:06 Finished examples/lpr_checker/array                            9m31s   2GB
May 19 05:36:06 Starting examples/lpr_checker/array/compilation
May 19 05:53:39 Finished examples/lpr_checker/array/compilation               17m32s  12GB
May 19 05:53:39 Starting examples/lpr_checker/array/compilation/proofs
May 19 05:54:26 Finished examples/lpr_checker/array/compilation/proofs           46s   4GB
May 19 05:54:26 Starting translator/okasaki-examples
May 19 05:58:37 Finished translator/okasaki-examples                           4m11s   1GB
May 19 05:58:37 Starting translator/other-examples
May 19 06:00:27 Finished translator/other-examples                             1m49s   1GB
May 19 06:00:27 Starting compiler/parsing/tests
May 19 06:00:51 Finished compiler/parsing/tests                                  23s 589MB
May 19 06:00:51 Starting compiler/inference/tests
May 19 06:05:16 Finished compiler/inference/tests                              4m24s   4GB
May 19 06:05:16 Starting compiler/bootstrap/translation
May 19 08:35:54 Finished compiler/bootstrap/translation                     2h30m37s  37GB
May 19 08:35:54 Starting unverified/sexpr-bootstrap/x64/64
May 19 08:50:45 Finished unverified/sexpr-bootstrap/x64/64                    14m50s   5GB
May 19 08:50:45 Starting unverified/sexpr-bootstrap/x64/32
May 19 09:01:18 Finished unverified/sexpr-bootstrap/x64/32                    10m33s   8GB
May 19 09:01:18 Starting compiler/benchmarks
May 19 09:40:10 Finished compiler/benchmarks                                  38m51s   2GB
May 19 09:40:10 Starting compiler/bootstrap/compilation/x64/64
May 20 00:20:50 Finished compiler/bootstrap/compilation/x64/64             14h40m39s  64GB
May 20 00:20:51 Starting compiler/bootstrap/compilation/x64/64/proofs
May 20 00:24:06 Finished compiler/bootstrap/compilation/x64/64/proofs          3m15s  13GB
May 20 00:24:06 Starting compiler/bootstrap/compilation/x64/32
May 20 14:05:12 Finished compiler/bootstrap/compilation/x64/32             13h41m05s  64GB
May 20 14:05:12 Starting compiler/bootstrap/compilation/x64/32/proofs
May 20 14:08:15 Finished compiler/bootstrap/compilation/x64/32/proofs          3m02s  12GB
May 20 14:08:15 Starting compiler/bootstrap/compilation/ag32/32
May 21 05:06:09 Finished compiler/bootstrap/compilation/ag32/32            14h57m53s  64GB
May 21 05:06:09 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 21 05:20:34 Finished compiler/bootstrap/compilation/ag32/32/proofs        14m24s  32GB
May 21 05:20:34 SUCCESS