Job 804

CakeML:fcc5a94f9d5425e6b678ee610a9226cab8fa20bf
  Fix bug in recursive post-processing of monadic translator [Apr 15 15:51:13]
#627 (monadic-trans-cleanup)
Merging into: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 17 11:43:49 Claimed job
Apr 17 11:43:55 Reusing HOL
Apr 17 11:43:59 Starting developers
Apr 17 11:44:00 Finished developers                                               0s  30MB
Apr 17 11:44:00 Starting developers/bin
Apr 17 11:44:33 Finished developers/bin                                          33s 205MB
Apr 17 11:44:34 Starting semantics/ffi
Apr 17 11:44:42 Finished semantics/ffi                                            7s 224MB
Apr 17 11:44:42 Starting semantics
Apr 17 11:46:01 Finished semantics                                             1m18s   1GB
Apr 17 11:46:02 Starting semantics/proofs
Apr 17 11:49:01 Finished semantics/proofs                                      2m58s   1GB
Apr 17 11:49:01 Starting basis/pure
Apr 17 11:49:46 Finished basis/pure                                              44s 812MB
Apr 17 11:49:46 Starting translator
Apr 17 11:51:25 Finished translator                                            1m38s   1GB
Apr 17 11:51:26 Starting compiler/parsing
Apr 17 11:52:25 Finished compiler/parsing                                        58s   2GB
Apr 17 11:52:25 Starting characteristic
Apr 17 11:57:38 Finished characteristic                                        5m12s   1GB
Apr 17 11:57:38 Starting translator/monadic
Apr 17 11:59:01 Finished translator/monadic                                    1m22s   1GB
Apr 17 11:59:02 Starting basis
Apr 17 12:15:31 Finished basis                                                16m28s   3GB
Apr 17 12:15:32 Starting compiler/inference
Apr 17 12:17:04 Finished compiler/inference                                    1m32s   1GB
Apr 17 12:17:05 Starting compiler/backend/reg_alloc
Apr 17 12:18:03 Finished compiler/backend/reg_alloc                              58s   1GB
Apr 17 12:18:04 Starting compiler/backend/gc
Apr 17 12:26:12 Finished compiler/backend/gc                                   8m07s   1GB
Apr 17 12:26:12 Starting compiler/backend
Apr 17 12:26:13 Finished compiler/backend                                         0s  42MB
Apr 17 12:26:14 Starting compiler/encoders/asm
Apr 17 12:26:14 Finished compiler/encoders/asm                                    0s  32MB
Apr 17 12:26:15 Starting compiler/encoders/x64
Apr 17 12:26:38 Finished compiler/encoders/x64                                   22s 956MB
Apr 17 12:26:38 Starting compiler/encoders/arm6
Apr 17 12:27:23 Finished compiler/encoders/arm6                                  44s 749MB
Apr 17 12:27:23 Starting compiler/encoders/arm8
Apr 17 12:27:35 Finished compiler/encoders/arm8                                  11s 637MB
Apr 17 12:27:35 Starting compiler/encoders/mips
Apr 17 12:27:52 Finished compiler/encoders/mips                                  16s 900MB
Apr 17 12:27:52 Starting compiler/encoders/riscv
Apr 17 12:28:06 Finished compiler/encoders/riscv                                 13s 797MB
Apr 17 12:28:06 Starting compiler/encoders/ag32
Apr 17 12:28:21 Finished compiler/encoders/ag32                                  14s 506MB
Apr 17 12:28:21 Starting compiler/backend/x64
Apr 17 12:28:36 Finished compiler/backend/x64                                    14s 812MB
Apr 17 12:28:37 Starting compiler/backend/arm6
Apr 17 12:28:54 Finished compiler/backend/arm6                                   16s   1GB
Apr 17 12:28:54 Starting compiler/backend/arm8
Apr 17 12:29:11 Finished compiler/backend/arm8                                   16s   1GB
Apr 17 12:29:11 Starting compiler/backend/mips
Apr 17 12:29:28 Finished compiler/backend/mips                                   16s   1GB
Apr 17 12:29:29 Starting compiler/backend/riscv
Apr 17 12:29:46 Finished compiler/backend/riscv                                  17s   1GB
Apr 17 12:29:46 Starting compiler/backend/ag32
Apr 17 12:30:57 Finished compiler/backend/ag32                                 1m09s   1GB
Apr 17 12:30:57 Starting compiler/parsing/proofs
Apr 17 12:36:33 Finished compiler/parsing/proofs                               5m35s 883MB
Apr 17 12:36:33 Starting compiler/inference/proofs
Apr 17 12:39:15 Finished compiler/inference/proofs                             2m40s   1GB
Apr 17 12:39:15 Starting compiler/backend/semantics
Apr 17 12:46:25 Finished compiler/backend/semantics                            7m09s   1GB
Apr 17 12:46:25 Starting compiler/backend/reg_alloc/proofs
Apr 17 12:49:44 Finished compiler/backend/reg_alloc/proofs                     3m18s 824MB
Apr 17 12:49:45 Starting compiler/backend/proofs
Apr 17 13:28:37 Finished compiler/backend/proofs                              38m51s   4GB
Apr 17 13:28:37 Starting compiler/encoders/x64/proofs
Apr 17 13:37:55 Finished compiler/encoders/x64/proofs                          9m17s   4GB
Apr 17 13:37:56 Starting compiler/encoders/arm6/proofs
Apr 17 13:50:39 Finished compiler/encoders/arm6/proofs                        12m42s   3GB
Apr 17 13:50:39 Starting compiler/encoders/arm8/proofs
Apr 17 13:56:12 Finished compiler/encoders/arm8/proofs                         5m32s   1GB
Apr 17 13:56:12 Starting compiler/encoders/mips/proofs
Apr 17 14:05:45 Finished compiler/encoders/mips/proofs                         9m32s   3GB
Apr 17 14:05:45 Starting compiler/encoders/riscv/proofs
Apr 17 14:14:11 Finished compiler/encoders/riscv/proofs                        8m25s   1GB
Apr 17 14:14:12 Starting compiler/encoders/ag32/proofs
Apr 17 14:16:42 Finished compiler/encoders/ag32/proofs                         2m29s 863MB
Apr 17 14:16:42 Starting compiler/backend/x64/proofs
Apr 17 14:16:59 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 17 14:16:59 Starting compiler/backend/arm6/proofs
Apr 17 14:17:18 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 17 14:17:18 Starting compiler/backend/arm8/proofs
Apr 17 14:17:35 Finished compiler/backend/arm8/proofs                            16s   1GB
Apr 17 14:17:36 Starting compiler/backend/mips/proofs
Apr 17 14:17:53 Finished compiler/backend/mips/proofs                            16s 912MB
Apr 17 14:17:53 Starting compiler/backend/riscv/proofs
Apr 17 14:18:11 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 17 14:18:11 Starting compiler/backend/ag32/proofs
Apr 17 14:27:23 Finished compiler/backend/ag32/proofs                          9m11s   2GB
Apr 17 14:27:23 Starting compiler/proofs
Apr 17 14:28:49 Finished compiler/proofs                                       1m25s   2GB
Apr 17 14:28:50 Starting candle/set-theory
Apr 17 14:29:15 Finished candle/set-theory                                       24s 827MB
Apr 17 14:29:15 Starting candle/syntax-lib
Apr 17 14:29:25 Finished candle/syntax-lib                                        8s 619MB
Apr 17 14:29:25 Starting candle/standard/syntax
Apr 17 14:31:08 Finished candle/standard/syntax                                1m41s   1GB
Apr 17 14:31:08 Starting candle/standard/semantics
Apr 17 14:32:44 Finished candle/standard/semantics                             1m35s   1GB
Apr 17 14:32:44 Starting candle/standard/monadic
Apr 17 14:34:19 Finished candle/standard/monadic                               1m34s   1GB
Apr 17 14:34:19 Starting candle/standard/ml_kernel
Apr 17 14:38:26 Finished candle/standard/ml_kernel                             4m06s   3GB
Apr 17 14:38:26 Starting candle/standard/opentheory Apr 17 14:38:26 414s