Job 1409

CakeML:64fa563af5add0fec73b7e0693abe8aec0e71efc
  Change a Q.prove to a Triviality .. Proof .. QED [Dec 03 20:09:19]
#808 (ord-chr-word8)
Merging into:3157c56dfe1eab23ef37b3cefb8fca2cced396c5
  Merge pull request #804 from CakeML/currheap [Nov 17 07:22:18]
HOL:77016ef7b01f987f1f684e825ac1d79feb8d454a
  emacs-mode: fix bug in previous caused by variable masking [Nov 27 05:03:03]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 03 20:10:53 Claimed job
Dec 03 20:10:59 Reusing HOL
Dec 03 20:11:06 Starting developers
Dec 03 20:11:08 Finished developers                                               2s 124MB
Dec 03 20:11:08 Starting developers/bin
Dec 03 20:11:15 Finished developers/bin                                           6s   1GB
Dec 03 20:11:15 Starting semantics/ffi
Dec 03 20:11:25 Finished semantics/ffi                                           10s 305MB
Dec 03 20:11:26 Starting semantics
Dec 03 20:12:55 Finished semantics                                             1m29s   1GB
Dec 03 20:12:56 Starting semantics/proofs
Dec 03 20:16:23 Finished semantics/proofs                                      3m27s   1GB
Dec 03 20:16:23 Starting semantics/alt_semantics
Dec 03 20:16:32 Finished semantics/alt_semantics                                  8s 348MB
Dec 03 20:16:32 Starting semantics/alt_semantics/proofs
Dec 03 20:18:43 Finished semantics/alt_semantics/proofs                        2m11s   1GB
Dec 03 20:18:43 Starting basis/pure
Dec 03 20:19:36 Finished basis/pure                                              52s   1GB
Dec 03 20:19:36 Starting translator
Dec 03 20:22:11 Finished translator                                            2m34s   2GB
Dec 03 20:22:11 Starting compiler/parsing
Dec 03 20:23:18 Finished compiler/parsing                                      1m07s   4GB
Dec 03 20:23:18 Starting characteristic
Dec 03 20:29:12 Finished characteristic                                        5m53s   3GB
Dec 03 20:29:12 Starting translator/monadic
Dec 03 20:30:55 Finished translator/monadic                                    1m42s   2GB
Dec 03 20:30:55 Starting basis
Dec 03 21:04:02 Finished basis                                                33m06s  24GB
Dec 03 21:04:02 Starting compiler/inference
Dec 03 21:05:04 Finished compiler/inference                                    1m02s   1GB
Dec 03 21:05:04 Starting compiler/backend/reg_alloc
Dec 03 21:06:07 Finished compiler/backend/reg_alloc                            1m02s   1GB
Dec 03 21:06:08 Starting compiler/backend/gc
Dec 03 21:09:28 Finished compiler/backend/gc                                   3m19s   2GB
Dec 03 21:09:28 Starting compiler/backend
Dec 03 21:14:25 Finished compiler/backend                                      4m57s   5GB
Dec 03 21:14:25 Starting compiler/encoders/asm
Dec 03 21:14:48 Finished compiler/encoders/asm                                   22s   1GB
Dec 03 21:14:48 Starting compiler/encoders/x64
Dec 03 21:15:15 Finished compiler/encoders/x64                                   26s   1GB
Dec 03 21:15:15 Starting compiler/encoders/arm7
Dec 03 21:16:07 Finished compiler/encoders/arm7                                  51s   1GB
Dec 03 21:16:07 Starting compiler/encoders/arm8
Dec 03 21:16:21 Finished compiler/encoders/arm8                                  13s   1GB
Dec 03 21:16:21 Starting compiler/encoders/mips
Dec 03 21:16:40 Finished compiler/encoders/mips                                  18s   1GB
Dec 03 21:16:40 Starting compiler/encoders/riscv
Dec 03 21:16:58 Finished compiler/encoders/riscv                                 17s   1GB
Dec 03 21:16:58 Starting compiler/encoders/ag32
Dec 03 21:17:17 Finished compiler/encoders/ag32                                  19s 908MB
Dec 03 21:17:17 Starting compiler/backend/x64
Dec 03 21:17:38 Finished compiler/backend/x64                                    20s   1GB
Dec 03 21:17:38 Starting compiler/backend/arm7
Dec 03 21:18:00 Finished compiler/backend/arm7                                   22s   1GB
Dec 03 21:18:00 Starting compiler/backend/arm8
Dec 03 21:18:22 Finished compiler/backend/arm8                                   21s   1GB
Dec 03 21:18:22 Starting compiler/backend/mips
Dec 03 21:18:42 Finished compiler/backend/mips                                   20s   1GB
Dec 03 21:18:42 Starting compiler/backend/riscv
Dec 03 21:19:03 Finished compiler/backend/riscv                                  19s   1GB
Dec 03 21:19:03 Starting compiler/backend/ag32
Dec 03 21:20:13 Finished compiler/backend/ag32                                 1m09s   1GB
Dec 03 21:20:13 Starting compiler/parsing/proofs
Dec 03 21:25:41 Finished compiler/parsing/proofs                               5m27s   2GB
Dec 03 21:25:41 Starting compiler/inference/proofs
Dec 03 21:28:13 Finished compiler/inference/proofs                             2m32s   2GB
Dec 03 21:28:14 Starting compiler/backend/semantics
Dec 03 21:55:06 Finished compiler/backend/semantics                           26m51s   4GB
Dec 03 21:55:06 Starting compiler/backend/reg_alloc/proofs
Dec 03 21:58:21 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Dec 03 21:58:21 Starting compiler/backend/proofs
Dec 03 22:51:56 Finished compiler/backend/proofs                              53m35s  21GB
Dec 03 22:51:56 Starting compiler/encoders/x64/proofs
Dec 03 23:01:22 Finished compiler/encoders/x64/proofs                          9m25s   4GB
Dec 03 23:01:22 Starting compiler/encoders/arm7/proofs
Dec 03 23:13:45 Finished compiler/encoders/arm7/proofs                        12m23s   6GB
Dec 03 23:13:45 Starting compiler/encoders/arm8/proofs
Dec 03 23:20:02 Finished compiler/encoders/arm8/proofs                         6m16s   4GB
Dec 03 23:20:02 Starting compiler/encoders/mips/proofs
Dec 03 23:29:53 Finished compiler/encoders/mips/proofs                         9m50s   6GB
Dec 03 23:29:53 Starting compiler/encoders/riscv/proofs
Dec 03 23:38:13 Finished compiler/encoders/riscv/proofs                        8m19s   3GB
Dec 03 23:38:13 Starting compiler/encoders/ag32/proofs
Dec 03 23:40:35 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Dec 03 23:40:35 Starting compiler/backend/x64/proofs
Dec 03 23:40:57 Finished compiler/backend/x64/proofs                             21s   1GB
Dec 03 23:40:57 Starting compiler/backend/arm7/proofs
Dec 03 23:41:21 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 03 23:41:21 Starting compiler/backend/arm8/proofs
Dec 03 23:41:41 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 03 23:41:41 Starting compiler/backend/mips/proofs
Dec 03 23:42:03 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 03 23:42:03 Starting compiler/backend/riscv/proofs
Dec 03 23:42:26 Finished compiler/backend/riscv/proofs                           22s   2GB
Dec 03 23:42:26 Starting compiler/backend/ag32/proofs
Dec 03 23:54:29 Finished compiler/backend/ag32/proofs                         12m03s   4GB
Dec 03 23:54:30 Starting compiler/proofs
Dec 03 23:56:11 Finished compiler/proofs                                       1m40s   6GB
Dec 03 23:56:11 Starting candle/set-theory
Dec 03 23:56:39 Finished candle/set-theory                                       28s 965MB
Dec 03 23:56:39 Starting candle/syntax-lib
Dec 03 23:56:50 Finished candle/syntax-lib                                       10s 788MB
Dec 03 23:56:50 Starting candle/standard/syntax
Dec 03 23:58:39 Finished candle/standard/syntax                                1m48s   1GB
Dec 03 23:58:39 Starting candle/standard/semantics
Dec 04 00:00:24 Finished candle/standard/semantics                             1m45s   2GB
Dec 04 00:00:25 Starting candle/standard/monadic
Dec 04 00:02:04 Finished candle/standard/monadic                               1m39s   1GB
Dec 04 00:02:04 Starting candle/standard/ml_kernel
Dec 04 00:07:18 Finished candle/standard/ml_kernel                             5m13s   6GB
Dec 04 00:07:18 Starting candle/overloading/syntax
Dec 04 00:10:29 Finished candle/overloading/syntax                             3m10s   1GB
Dec 04 00:10:29 Starting candle/overloading/semantics
Dec 04 00:22:29 Finished candle/overloading/semantics                         11m59s   8GB
Dec 04 00:22:29 Starting characteristic/examples
Dec 04 00:23:47 Finished characteristic/examples                               1m17s   4GB
Dec 04 00:23:48 Starting tutorial/solutions
Dec 04 00:38:56 Finished tutorial/solutions                                   15m08s  11GB
Dec 04 00:38:56 Starting translator/monadic/examples
Dec 04 00:42:15 Finished translator/monadic/examples                           3m18s   3GB
Dec 04 00:42:16 Starting examples
Dec 04 00:50:49 Finished examples                                              8m33s   6GB
Dec 04 00:50:49 Starting examples/compilation/x64
Dec 04 03:12:06 Finished examples/compilation/x64                           2h21m17s  20GB
Dec 04 03:12:06 Starting examples/compilation/x64/proofs
Dec 04 03:14:02 Finished examples/compilation/x64/proofs                       1m55s   3GB
Dec 04 03:14:02 Starting examples/compilation/ag32
Dec 04 03:46:49 Finished examples/compilation/ag32                            32m46s  14GB
Dec 04 03:46:49 Starting examples/compilation/ag32/proofs
Dec 04 03:47:42 Finished examples/compilation/ag32/proofs                        53s   4GB
Dec 04 03:47:43 Starting examples/cost
Dec 04 04:41:15 Finished examples/cost                                        53m32s  14GB
Dec 04 04:41:15 Starting examples/lpr_checker
Dec 04 04:44:59 Finished examples/lpr_checker                                  3m43s   3GB
Dec 04 04:44:59 Starting examples/lpr_checker/compilation
Dec 04 05:02:54 Finished examples/lpr_checker/compilation                     17m52s  19GB
Dec 04 05:02:54 Starting examples/lpr_checker/compilation/proofs
Dec 04 05:03:38 Finished examples/lpr_checker/compilation/proofs                 43s   3GB
Dec 04 05:03:38 Starting examples/lpr_checker/array
Dec 04 05:17:02 Finished examples/lpr_checker/array                           13m23s   5GB
Dec 04 05:17:02 Starting examples/lpr_checker/array/compilation
Dec 04 05:36:52 Finished examples/lpr_checker/array/compilation               19m49s  15GB
Dec 04 05:36:52 Starting examples/lpr_checker/array/compilation/proofs
Dec 04 05:37:42 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Dec 04 05:37:42 Starting examples/opentheory
Dec 04 05:47:18 Finished examples/opentheory                                   9m35s   6GB
Dec 04 05:47:18 Starting examples/opentheory
Dec 04 05:47:19 Finished examples/opentheory                                      0s 100MB
Dec 04 05:47:19 Starting examples/opentheory/compilation
Dec 04 06:24:54 Finished examples/opentheory/compilation                      37m35s  54GB
Dec 04 06:24:54 Starting examples/opentheory/compilation/proofs
Dec 04 06:25:54 Finished examples/opentheory/compilation/proofs                  59s   4GB
Dec 04 06:25:54 Starting examples/opentheory/compilation/ag32
Dec 04 07:10:48 Finished examples/opentheory/compilation/ag32                 44m53s  25GB
Dec 04 07:10:48 Starting examples/opentheory/compilation/ag32/proofs
Dec 04 07:12:23 Finished examples/opentheory/compilation/ag32/proofs           1m35s   5GB
Dec 04 07:12:23 Starting translator/okasaki-examples
Dec 04 07:17:01 Finished translator/okasaki-examples                           4m37s   2GB
Dec 04 07:17:01 Starting translator/other-examples
Dec 04 07:19:22 Finished translator/other-examples                             2m20s   1GB
Dec 04 07:19:22 Starting compiler/parsing/tests
Dec 04 07:19:47 Finished compiler/parsing/tests                                  24s 633MB
Dec 04 07:19:47 Starting compiler/inference/tests
Dec 04 07:27:11 Finished compiler/inference/tests                              7m23s   6GB
Dec 04 07:27:12 Starting compiler/bootstrap/translation
Dec 04 10:14:30 Finished compiler/bootstrap/translation                     2h47m18s  48GB
Dec 04 10:14:30 Starting unverified/sexpr-bootstrap/x64/64
Dec 04 10:26:34 Finished unverified/sexpr-bootstrap/x64/64                    12m03s   8GB
Dec 04 10:26:34 Starting unverified/sexpr-bootstrap/x64/32
Dec 04 10:36:56 Finished unverified/sexpr-bootstrap/x64/32                    10m21s   8GB
Dec 04 10:36:56 Starting compiler/benchmarks
Dec 04 11:14:39 Finished compiler/benchmarks                                  37m42s   2GB
Dec 04 11:14:39 Starting compiler/bootstrap/compilation/x64/64
Dec 05 05:59:44 Resuming compiler/bootstrap/compilation/x64/64