Job 1397

CakeML:ac5c74531f672da189747a095e1b6664f3b9ce21
  Replace a Q.prove with Theorem ... QED [Nov 15 20:20:31]
#804 (currheap)
Merging into:e76d28c8e72843dfda88ff470e38d5fdfa8acda4
  Merge pull request #802 from CakeML/data-cost [Nov 14 14:20:36]
HOL:ea22210a5c1604df84c66d847322f752e263354d
  Fiddle with file in attempt to get otknl build progressing further [Nov 10 07:57:06]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 15 21:08:17 Claimed job
Nov 15 21:08:20 Building HOL
Nov 15 21:22:12 Starting developers
Nov 15 21:22:14 Finished developers                                               2s 123MB
Nov 15 21:22:14 Starting developers/bin
Nov 15 21:22:20 Finished developers/bin                                           5s   1GB
Nov 15 21:22:20 Starting semantics/ffi
Nov 15 21:22:30 Finished semantics/ffi                                            9s 293MB
Nov 15 21:22:31 Starting semantics
Nov 15 21:24:04 Finished semantics                                             1m32s   1GB
Nov 15 21:24:04 Starting semantics/proofs
Nov 15 21:27:21 Finished semantics/proofs                                      3m16s   1GB
Nov 15 21:27:21 Starting semantics/alt_semantics
Nov 15 21:27:29 Finished semantics/alt_semantics                                  7s 408MB
Nov 15 21:27:29 Starting semantics/alt_semantics/proofs
Nov 15 21:29:35 Finished semantics/alt_semantics/proofs                        2m05s   1GB
Nov 15 21:29:35 Starting basis/pure
Nov 15 21:32:19 Finished basis/pure                                            2m43s   1GB
Nov 15 21:32:19 Starting translator
Nov 15 21:34:54 Finished translator                                            2m35s   2GB
Nov 15 21:34:55 Starting compiler/parsing
Nov 15 21:36:04 Finished compiler/parsing                                      1m09s   4GB
Nov 15 21:36:04 Starting characteristic
Nov 15 21:41:58 Finished characteristic                                        5m53s   4GB
Nov 15 21:41:58 Starting translator/monadic
Nov 15 21:43:42 Finished translator/monadic                                    1m44s   2GB
Nov 15 21:43:42 Starting basis
Nov 15 22:16:50 Finished basis                                                33m08s  37GB
Nov 15 22:16:51 Starting compiler/inference
Nov 15 22:17:59 Finished compiler/inference                                    1m07s   1GB
Nov 15 22:17:59 Starting compiler/backend/reg_alloc
Nov 15 22:19:01 Finished compiler/backend/reg_alloc                            1m01s   1GB
Nov 15 22:19:01 Starting compiler/backend/gc
Nov 15 22:22:35 Finished compiler/backend/gc                                   3m33s   3GB
Nov 15 22:22:35 Starting compiler/backend
Nov 15 22:27:26 Finished compiler/backend                                      4m50s   4GB
Nov 15 22:27:26 Starting compiler/encoders/asm
Nov 15 22:27:49 Finished compiler/encoders/asm                                   22s   1GB
Nov 15 22:27:49 Starting compiler/encoders/x64
Nov 15 22:28:51 Finished compiler/encoders/x64                                 1m01s   1GB
Nov 15 22:28:51 Starting compiler/encoders/arm7
Nov 15 22:30:52 Finished compiler/encoders/arm7                                2m00s   1GB
Nov 15 22:30:52 Starting compiler/encoders/arm8
Nov 15 22:31:31 Finished compiler/encoders/arm8                                  38s   1GB
Nov 15 22:31:31 Starting compiler/encoders/mips
Nov 15 22:32:55 Finished compiler/encoders/mips                                1m24s   1GB
Nov 15 22:32:55 Starting compiler/encoders/riscv
Nov 15 22:34:31 Finished compiler/encoders/riscv                               1m35s   1GB
Nov 15 22:34:31 Starting compiler/encoders/ag32
Nov 15 22:34:50 Finished compiler/encoders/ag32                                  18s 919MB
Nov 15 22:34:50 Starting compiler/backend/x64
Nov 15 22:35:08 Finished compiler/backend/x64                                    17s   1GB
Nov 15 22:35:08 Starting compiler/backend/arm7
Nov 15 22:35:30 Finished compiler/backend/arm7                                   21s   1GB
Nov 15 22:35:30 Starting compiler/backend/arm8
Nov 15 22:35:51 Finished compiler/backend/arm8                                   20s   1GB
Nov 15 22:35:51 Starting compiler/backend/mips
Nov 15 22:36:11 Finished compiler/backend/mips                                   20s   1GB
Nov 15 22:36:12 Starting compiler/backend/riscv
Nov 15 22:36:32 Finished compiler/backend/riscv                                  20s   1GB
Nov 15 22:36:33 Starting compiler/backend/ag32
Nov 15 22:37:44 Finished compiler/backend/ag32                                 1m10s   2GB
Nov 15 22:37:44 Starting compiler/parsing/proofs
Nov 15 22:43:11 Finished compiler/parsing/proofs                               5m26s   1GB
Nov 15 22:43:11 Starting compiler/inference/proofs
Nov 15 22:45:44 Finished compiler/inference/proofs                             2m33s   2GB
Nov 15 22:45:44 Starting compiler/backend/semantics
Nov 15 23:12:01 Finished compiler/backend/semantics                           26m17s   5GB
Nov 15 23:12:02 Starting compiler/backend/reg_alloc/proofs
Nov 15 23:15:17 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Nov 15 23:15:17 Starting compiler/backend/proofs
Nov 16 00:09:00 Finished compiler/backend/proofs                              53m42s  17GB
Nov 16 00:09:01 Starting compiler/encoders/x64/proofs
Nov 16 00:18:19 Finished compiler/encoders/x64/proofs                          9m18s   4GB
Nov 16 00:18:20 Starting compiler/encoders/arm7/proofs
Nov 16 00:30:47 Finished compiler/encoders/arm7/proofs                        12m27s   6GB
Nov 16 00:30:47 Starting compiler/encoders/arm8/proofs
Nov 16 00:37:20 Finished compiler/encoders/arm8/proofs                         6m32s   4GB
Nov 16 00:37:20 Starting compiler/encoders/mips/proofs
Nov 16 00:47:13 Finished compiler/encoders/mips/proofs                         9m52s   8GB
Nov 16 00:47:13 Starting compiler/encoders/riscv/proofs
Nov 16 00:55:39 Finished compiler/encoders/riscv/proofs                        8m25s   3GB
Nov 16 00:55:39 Starting compiler/encoders/ag32/proofs
Nov 16 00:58:00 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Nov 16 00:58:00 Starting compiler/backend/x64/proofs
Nov 16 00:58:21 Finished compiler/backend/x64/proofs                             20s   1GB
Nov 16 00:58:21 Starting compiler/backend/arm7/proofs
Nov 16 00:58:44 Finished compiler/backend/arm7/proofs                            23s   1GB
Nov 16 00:58:45 Starting compiler/backend/arm8/proofs
Nov 16 00:59:06 Finished compiler/backend/arm8/proofs                            21s   1GB
Nov 16 00:59:06 Starting compiler/backend/mips/proofs
Nov 16 00:59:27 Finished compiler/backend/mips/proofs                            21s   1GB
Nov 16 00:59:28 Starting compiler/backend/riscv/proofs
Nov 16 00:59:50 Finished compiler/backend/riscv/proofs                           22s   2GB
Nov 16 00:59:50 Starting compiler/backend/ag32/proofs
Nov 16 01:11:56 Finished compiler/backend/ag32/proofs                         12m05s   5GB
Nov 16 01:11:56 Starting compiler/proofs
Nov 16 01:13:51 Finished compiler/proofs                                       1m54s   6GB
Nov 16 01:13:51 Starting candle/set-theory
Nov 16 01:14:20 Finished candle/set-theory                                       28s 990MB
Nov 16 01:14:20 Starting candle/syntax-lib
Nov 16 01:14:31 Finished candle/syntax-lib                                       10s 788MB
Nov 16 01:14:31 Starting candle/standard/syntax
Nov 16 01:16:23 Finished candle/standard/syntax                                1m51s   1GB
Nov 16 01:16:23 Starting candle/standard/semantics
Nov 16 01:18:10 Finished candle/standard/semantics                             1m46s   2GB
Nov 16 01:18:10 Starting candle/standard/monadic
Nov 16 01:19:49 Finished candle/standard/monadic                               1m38s   1GB
Nov 16 01:19:49 Starting candle/standard/ml_kernel
Nov 16 01:25:03 Finished candle/standard/ml_kernel                             5m13s   6GB
Nov 16 01:25:03 Starting candle/overloading/syntax
Nov 16 01:28:14 Finished candle/overloading/syntax                             3m10s   1GB
Nov 16 01:28:14 Starting candle/overloading/semantics
Nov 16 01:40:21 Finished candle/overloading/semantics                         12m07s   8GB
Nov 16 01:40:21 Starting characteristic/examples
Nov 16 01:41:39 Finished characteristic/examples                               1m17s   4GB
Nov 16 01:41:39 Starting tutorial/solutions
Nov 16 01:55:36 Finished tutorial/solutions                                   13m56s  15GB
Nov 16 01:55:36 Starting translator/monadic/examples
Nov 16 01:58:54 Finished translator/monadic/examples                           3m17s   4GB
Nov 16 01:58:55 Starting examples
Nov 16 02:07:26 Finished examples                                              8m30s   7GB
Nov 16 02:07:26 Starting examples/compilation/x64
Nov 16 04:15:38 Finished examples/compilation/x64                           2h08m11s  20GB
Nov 16 04:15:38 Starting examples/compilation/x64/proofs
Nov 16 04:17:33 Finished examples/compilation/x64/proofs                       1m54s   3GB
Nov 16 04:17:33 Starting examples/compilation/ag32
Nov 16 04:47:41 Finished examples/compilation/ag32                            30m07s  10GB
Nov 16 04:47:41 Starting examples/compilation/ag32/proofs
Nov 16 04:48:35 Finished examples/compilation/ag32/proofs                        53s   4GB
Nov 16 04:48:35 Starting examples/cost
Nov 16 05:42:45 Finished examples/cost                                        54m09s  15GB
Nov 16 05:42:45 Starting examples/lpr_checker
Nov 16 05:46:27 Finished examples/lpr_checker                                  3m42s   3GB
Nov 16 05:46:27 Starting examples/lpr_checker/compilation
Nov 16 06:03:09 Finished examples/lpr_checker/compilation                     16m42s  15GB
Nov 16 06:03:10 Starting examples/lpr_checker/compilation/proofs
Nov 16 06:03:52 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Nov 16 06:03:52 Starting examples/lpr_checker/array
Nov 16 06:17:12 Finished examples/lpr_checker/array                           13m20s   6GB
Nov 16 06:17:12 Starting examples/lpr_checker/array/compilation
Nov 16 06:34:51 Finished examples/lpr_checker/array/compilation               17m38s  18GB
Nov 16 06:34:52 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 06:35:39 Finished examples/lpr_checker/array/compilation/proofs           47s   4GB
Nov 16 06:35:40 Starting examples/opentheory
Nov 16 06:44:41 Finished examples/opentheory                                   9m01s   6GB
Nov 16 06:44:41 Starting examples/opentheory
Nov 16 06:44:42 Finished examples/opentheory                                      0s 100MB
Nov 16 06:44:42 Starting examples/opentheory/compilation
Nov 16 07:14:26 Finished examples/opentheory/compilation                      29m43s  16GB
Nov 16 07:14:26 Starting examples/opentheory/compilation/proofs
Nov 16 07:15:08 Finished examples/opentheory/compilation/proofs                  41s   4GB
Nov 16 07:15:08 Starting examples/opentheory/compilation/ag32
Nov 16 07:48:45 Finished examples/opentheory/compilation/ag32                 33m36s  24GB
Nov 16 07:48:45 Starting examples/opentheory/compilation/ag32/proofs
Nov 16 07:50:19 Finished examples/opentheory/compilation/ag32/proofs           1m34s   9GB
Nov 16 07:50:19 Starting translator/okasaki-examples
Nov 16 07:54:28 Finished translator/okasaki-examples                           4m07s   2GB
Nov 16 07:54:28 Starting translator/other-examples
Nov 16 07:56:30 Finished translator/other-examples                             2m01s   2GB
Nov 16 07:56:30 Starting compiler/parsing/tests
Nov 16 07:56:54 Finished compiler/parsing/tests                                  23s 639MB
Nov 16 07:56:54 Starting compiler/inference/tests
Nov 16 08:01:17 Finished compiler/inference/tests                              4m23s   3GB
Nov 16 08:01:17 Starting compiler/bootstrap/translation
Nov 16 11:07:02 Finished compiler/bootstrap/translation                     3h05m44s  48GB
Nov 16 11:07:02 Starting unverified/sexpr-bootstrap/x64/64
Nov 16 11:16:33 Finished unverified/sexpr-bootstrap/x64/64                     9m30s   8GB
Nov 16 11:16:33 Starting unverified/sexpr-bootstrap/x64/32
Nov 16 11:24:28 Finished unverified/sexpr-bootstrap/x64/32                     7m54s   8GB
Nov 16 11:24:28 Starting compiler/benchmarks
Nov 16 12:02:58 Finished compiler/benchmarks                                  38m30s   2GB
Nov 16 12:02:59 Starting compiler/bootstrap/compilation/x64/64
Nov 17 04:38:28 Finished compiler/bootstrap/compilation/x64/64             16h35m29s  64GB
Nov 17 04:38:29 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 17 04:40:44 Finished compiler/bootstrap/compilation/x64/64/proofs          2m14s  15GB
Nov 17 04:40:44 Starting compiler/bootstrap/compilation/x64/32
Nov 17 19:50:46 Finished compiler/bootstrap/compilation/x64/32             15h10m02s  64GB
Nov 17 19:50:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 17 19:53:03 Finished compiler/bootstrap/compilation/x64/32/proofs          2m16s  16GB
Nov 17 19:53:03 Starting compiler/bootstrap/compilation/ag32/32
Nov 18 10:24:05 Finished compiler/bootstrap/compilation/ag32/32            14h31m01s  62GB
Nov 18 10:24:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 18 10:33:16 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m10s  56GB
Nov 18 10:33:16 SUCCESS