Job 803

CakeML:3820e50e1c72e6b9c13a5b927d06ac16dc85fd4b
  Fix some now-broken definition-saves to regain "compute" attribute [Apr 17 00:04:02]
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/ [Apr 15 07:09:08]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 17 00:20:13 Claimed job
Apr 17 00:20:18 Reusing HOL
Apr 17 00:21:05 Starting developers
Apr 17 00:21:08 Finished developers                                               2s  21MB
Apr 17 00:21:08 Starting developers/bin
Apr 17 00:22:18 Finished developers/bin                                        1m09s 918MB
Apr 17 00:22:18 Starting semantics/ffi
Apr 17 00:22:29 Finished semantics/ffi                                           10s 227MB
Apr 17 00:22:29 Starting semantics
Apr 17 00:23:51 Finished semantics                                             1m21s   1GB
Apr 17 00:23:51 Starting semantics/proofs
Apr 17 00:26:47 Finished semantics/proofs                                      2m55s   1GB
Apr 17 00:26:47 Starting basis/pure
Apr 17 00:27:34 Finished basis/pure                                              46s 644MB
Apr 17 00:27:35 Starting translator
Apr 17 00:29:14 Finished translator                                            1m39s   1GB
Apr 17 00:29:14 Starting compiler/parsing
Apr 17 00:30:12 Finished compiler/parsing                                        57s   1GB
Apr 17 00:30:13 Starting characteristic
Apr 17 00:35:27 Finished characteristic                                        5m13s   1GB
Apr 17 00:35:27 Starting translator/monadic
Apr 17 00:36:57 Finished translator/monadic                                    1m29s   1GB
Apr 17 00:36:57 Starting basis
Apr 17 00:53:06 Finished basis                                                16m08s   3GB
Apr 17 00:53:06 Starting compiler/inference
Apr 17 00:54:39 Finished compiler/inference                                    1m33s   1GB
Apr 17 00:54:39 Starting compiler/backend/reg_alloc
Apr 17 00:55:33 Finished compiler/backend/reg_alloc                              53s   1GB
Apr 17 00:55:33 Starting compiler/backend/gc
Apr 17 01:03:32 Finished compiler/backend/gc                                   7m58s   2GB
Apr 17 01:03:32 Starting compiler/backend
Apr 17 01:03:34 Finished compiler/backend                                         2s  25MB
Apr 17 01:03:35 Starting compiler/encoders/asm
Apr 17 01:03:37 Finished compiler/encoders/asm                                    1s  22MB
Apr 17 01:03:37 Starting compiler/encoders/x64
Apr 17 01:04:01 Finished compiler/encoders/x64                                   24s 754MB
Apr 17 01:04:02 Starting compiler/encoders/arm6
Apr 17 01:04:47 Finished compiler/encoders/arm6                                  45s 736MB
Apr 17 01:04:47 Starting compiler/encoders/arm8
Apr 17 01:05:00 Finished compiler/encoders/arm8                                  13s 599MB
Apr 17 01:05:01 Starting compiler/encoders/mips
Apr 17 01:05:19 Finished compiler/encoders/mips                                  18s   1GB
Apr 17 01:05:20 Starting compiler/encoders/riscv
Apr 17 01:05:35 Finished compiler/encoders/riscv                                 14s 841MB
Apr 17 01:05:35 Starting compiler/encoders/ag32
Apr 17 01:05:52 Finished compiler/encoders/ag32                                  16s 572MB
Apr 17 01:05:52 Starting compiler/backend/x64
Apr 17 01:06:11 Finished compiler/backend/x64                                    18s   1GB
Apr 17 01:06:11 Starting compiler/backend/arm6
Apr 17 01:06:31 Finished compiler/backend/arm6                                   20s   1GB
Apr 17 01:06:32 Starting compiler/backend/arm8
Apr 17 01:06:51 Finished compiler/backend/arm8                                   18s   1GB
Apr 17 01:06:51 Starting compiler/backend/mips
Apr 17 01:07:10 Finished compiler/backend/mips                                   18s   1GB
Apr 17 01:07:10 Starting compiler/backend/riscv
Apr 17 01:07:30 Finished compiler/backend/riscv                                  18s   1GB
Apr 17 01:07:30 Starting compiler/backend/ag32
Apr 17 01:08:37 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 17 01:08:38 Starting compiler/parsing/proofs
Apr 17 01:14:07 Finished compiler/parsing/proofs                               5m29s   1GB
Apr 17 01:14:08 Starting compiler/inference/proofs
Apr 17 01:16:47 Finished compiler/inference/proofs                             2m39s   1GB
Apr 17 01:16:48 Starting compiler/backend/semantics
Apr 17 01:23:40 Finished compiler/backend/semantics                            6m52s   1GB
Apr 17 01:23:41 Starting compiler/backend/reg_alloc/proofs
Apr 17 01:26:20 Finished compiler/backend/reg_alloc/proofs                     2m38s   1GB
Apr 17 01:26:20 Starting compiler/backend/proofs
Apr 17 02:03:07 Finished compiler/backend/proofs                              36m47s   3GB
Apr 17 02:03:08 Starting compiler/encoders/x64/proofs
Apr 17 02:12:01 Finished compiler/encoders/x64/proofs                          8m53s   4GB
Apr 17 02:12:01 Starting compiler/encoders/arm6/proofs
Apr 17 02:24:13 Finished compiler/encoders/arm6/proofs                        12m11s   3GB
Apr 17 02:24:13 Starting compiler/encoders/arm8/proofs
Apr 17 02:29:36 Finished compiler/encoders/arm8/proofs                         5m23s   1GB
Apr 17 02:29:37 Starting compiler/encoders/mips/proofs
Apr 17 02:38:50 Finished compiler/encoders/mips/proofs                         9m13s   2GB
Apr 17 02:38:51 Starting compiler/encoders/riscv/proofs
Apr 17 02:46:58 Finished compiler/encoders/riscv/proofs                        8m07s   1GB
Apr 17 02:46:59 Starting compiler/encoders/ag32/proofs
Apr 17 02:49:26 Finished compiler/encoders/ag32/proofs                         2m27s 731MB
Apr 17 02:49:26 Starting compiler/backend/x64/proofs
Apr 17 02:49:47 Finished compiler/backend/x64/proofs                             20s 762MB
Apr 17 02:49:48 Starting compiler/backend/arm6/proofs
Apr 17 02:50:09 Finished compiler/backend/arm6/proofs                            21s 941MB
Apr 17 02:50:09 Starting compiler/backend/arm8/proofs
Apr 17 02:50:29 Finished compiler/backend/arm8/proofs                            19s 815MB
Apr 17 02:50:29 Starting compiler/backend/mips/proofs
Apr 17 02:50:49 Finished compiler/backend/mips/proofs                            19s 897MB
Apr 17 02:50:49 Starting compiler/backend/riscv/proofs
Apr 17 02:51:11 Finished compiler/backend/riscv/proofs                           21s   1GB
Apr 17 02:51:11 Starting compiler/backend/ag32/proofs
Apr 17 02:59:54 Finished compiler/backend/ag32/proofs                          8m42s   2GB
Apr 17 02:59:54 Starting compiler/proofs
Apr 17 03:01:13 Finished compiler/proofs                                       1m18s   3GB
Apr 17 03:01:13 Starting candle/set-theory
Apr 17 03:01:40 Finished candle/set-theory                                       26s 788MB
Apr 17 03:01:40 Starting candle/syntax-lib
Apr 17 03:01:51 Finished candle/syntax-lib                                       10s 645MB
Apr 17 03:01:51 Starting candle/standard/syntax
Apr 17 03:03:35 Finished candle/standard/syntax                                1m43s   1GB
Apr 17 03:03:35 Starting candle/standard/semantics
Apr 17 03:05:13 Finished candle/standard/semantics                             1m37s   1GB
Apr 17 03:05:14 Starting candle/standard/monadic
Apr 17 03:06:47 Finished candle/standard/monadic                               1m33s   1GB
Apr 17 03:06:47 Starting candle/standard/ml_kernel
Apr 17 03:10:40 Finished candle/standard/ml_kernel                             3m52s   3GB
Apr 17 03:10:40 Starting candle/standard/opentheory Apr 17 03:10:40 414s