Job 1673

CakeML:804fcaa356c30094a81e8319eefbb4cfbec0dc94
  Fix for deletion of terminationTheory [Dec 03 18:13:47]
#849 (delete_terminationTheory)
Merging into:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
  Merge pull request #847 from CakeML/clos-smart-op [Nov 30 09:57:02]
HOL:6dcb52a09341deda5c5068c06f92c6eaa2af36b6
  emacs-mode: display *Holmake* buffer better when it does its thing [Nov 26 04:28:46]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 03 19:59:20 Claimed job
Dec 03 19:59:29 Reusing HOL
Dec 03 20:00:09 Starting developers
Dec 03 20:00:14 Finished developers                                               4s  87MB
Dec 03 20:00:15 Starting developers/bin
Dec 03 20:00:22 Finished developers/bin                                           6s   1GB
Dec 03 20:00:22 Starting semantics/ffi
Dec 03 20:00:31 Finished semantics/ffi                                            8s 205MB
Dec 03 20:00:31 Starting semantics
Dec 03 20:01:58 Finished semantics                                             1m26s   1GB
Dec 03 20:01:58 Starting semantics/proofs
Dec 03 20:05:47 Finished semantics/proofs                                      3m49s   1GB
Dec 03 20:05:47 Starting semantics/alt_semantics
Dec 03 20:06:00 Finished semantics/alt_semantics                                 12s 340MB
Dec 03 20:06:00 Starting semantics/alt_semantics/proofs
Dec 03 20:08:36 Finished semantics/alt_semantics/proofs                        2m36s 800MB
Dec 03 20:08:37 Starting basis/pure
Dec 03 20:09:29 Finished basis/pure                                              52s 855MB
Dec 03 20:09:29 Starting translator
Dec 03 20:12:31 Finished translator                                            3m01s   1GB
Dec 03 20:12:31 Starting compiler/parsing
Dec 03 20:13:49 Finished compiler/parsing                                      1m18s   2GB
Dec 03 20:13:49 Starting characteristic
Dec 03 20:19:47 Finished characteristic                                        5m57s   1GB
Dec 03 20:19:48 Starting translator/monadic
Dec 03 20:21:32 Finished translator/monadic                                    1m43s   1GB
Dec 03 20:21:32 Starting basis
Dec 03 21:10:13 Finished basis                                                48m41s  11GB
Dec 03 21:10:14 Starting compiler/inference
Dec 03 21:11:23 Finished compiler/inference                                    1m09s   1GB
Dec 03 21:11:23 Starting compiler/backend/reg_alloc
Dec 03 21:12:34 Finished compiler/backend/reg_alloc                            1m10s   1GB
Dec 03 21:12:35 Starting compiler/backend/gc
Dec 03 21:16:10 Finished compiler/backend/gc                                   3m34s   1GB
Dec 03 21:16:10 Starting compiler/backend
Dec 03 21:21:00 Finished compiler/backend                                      4m49s   2GB
Dec 03 21:21:00 Starting compiler/encoders/asm
Dec 03 21:21:25 Finished compiler/encoders/asm                                   24s 751MB
Dec 03 21:21:25 Starting compiler/encoders/x64
Dec 03 21:21:52 Finished compiler/encoders/x64                                   27s   1GB
Dec 03 21:21:53 Starting compiler/encoders/arm7
Dec 03 21:22:46 Finished compiler/encoders/arm7                                  52s 732MB
Dec 03 21:22:46 Starting compiler/encoders/arm8
Dec 03 21:23:00 Finished compiler/encoders/arm8                                  14s 601MB
Dec 03 21:23:00 Starting compiler/encoders/mips
Dec 03 21:23:19 Finished compiler/encoders/mips                                  18s   1GB
Dec 03 21:23:19 Starting compiler/encoders/riscv
Dec 03 21:23:37 Finished compiler/encoders/riscv                                 17s 797MB
Dec 03 21:23:37 Starting compiler/encoders/ag32
Dec 03 21:23:56 Finished compiler/encoders/ag32                                  19s 611MB
Dec 03 21:23:57 Starting compiler/backend/x64
Dec 03 21:24:16 Finished compiler/backend/x64                                    19s   1GB
Dec 03 21:24:16 Starting compiler/backend/arm7
Dec 03 21:24:39 Finished compiler/backend/arm7                                   21s   1GB
Dec 03 21:24:39 Starting compiler/backend/arm8
Dec 03 21:24:59 Finished compiler/backend/arm8                                   19s   1GB
Dec 03 21:25:00 Starting compiler/backend/mips
Dec 03 21:25:20 Finished compiler/backend/mips                                   20s   1GB
Dec 03 21:25:20 Starting compiler/backend/riscv
Dec 03 21:25:41 Finished compiler/backend/riscv                                  20s   1GB
Dec 03 21:25:42 Starting compiler/backend/ag32
Dec 03 21:26:54 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 03 21:26:55 Starting compiler/parsing/proofs
Dec 03 21:30:54 Finished compiler/parsing/proofs                               3m59s   1GB
Dec 03 21:30:55 Starting compiler/inference/proofs
Dec 03 21:33:28 Finished compiler/inference/proofs                             2m33s   1GB
Dec 03 21:33:28 Starting compiler/backend/semantics
Dec 03 22:06:38 Finished compiler/backend/semantics                           33m09s   2GB
Dec 03 22:06:38 Starting compiler/backend/reg_alloc/proofs
Dec 03 22:10:26 Finished compiler/backend/reg_alloc/proofs                     3m47s 814MB
Dec 03 22:10:26 Starting compiler/backend/proofs
Dec 03 23:08:01 Finished compiler/backend/proofs                              57m33s  18GB
Dec 03 23:08:01 Starting compiler/backend/serialiser
Dec 03 23:09:15 Finished compiler/backend/serialiser                           1m14s   1GB
Dec 03 23:09:15 Starting compiler/encoders/x64/proofs
Dec 03 23:19:37 Finished compiler/encoders/x64/proofs                         10m21s   4GB
Dec 03 23:19:38 Starting compiler/encoders/arm7/proofs
Dec 03 23:33:38 Finished compiler/encoders/arm7/proofs                        14m00s   3GB
Dec 03 23:33:38 Starting compiler/encoders/arm8/proofs
Dec 03 23:40:45 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Dec 03 23:40:45 Starting compiler/encoders/mips/proofs
Dec 03 23:51:21 Finished compiler/encoders/mips/proofs                        10m35s   2GB
Dec 03 23:51:21 Starting compiler/encoders/riscv/proofs
Dec 04 00:00:53 Finished compiler/encoders/riscv/proofs                        9m31s   1GB
Dec 04 00:00:54 Starting compiler/encoders/ag32/proofs
Dec 04 00:03:41 Finished compiler/encoders/ag32/proofs                         2m46s 645MB
Dec 04 00:03:41 Starting compiler/backend/x64/proofs
Dec 04 00:04:05 Finished compiler/backend/x64/proofs                             23s   1GB
Dec 04 00:04:05 Starting compiler/backend/arm7/proofs
Dec 04 00:04:30 Finished compiler/backend/arm7/proofs                            24s   1GB
Dec 04 00:04:30 Starting compiler/backend/arm8/proofs
Dec 04 00:04:54 Finished compiler/backend/arm8/proofs                            23s   1GB
Dec 04 00:04:54 Starting compiler/backend/mips/proofs
Dec 04 00:05:18 Finished compiler/backend/mips/proofs                            23s   1GB
Dec 04 00:05:18 Starting compiler/backend/riscv/proofs
Dec 04 00:05:43 Finished compiler/backend/riscv/proofs                           24s   1GB
Dec 04 00:05:43 Starting compiler/backend/ag32/proofs
Dec 04 00:19:14 Finished compiler/backend/ag32/proofs                         13m30s   2GB
Dec 04 00:19:14 Starting compiler/proofs
Dec 04 00:21:02 Finished compiler/proofs                                       1m48s   4GB
Dec 04 00:21:03 Starting candle/set-theory
Dec 04 00:21:32 Finished candle/set-theory                                       29s 947MB
Dec 04 00:21:33 Starting candle/syntax-lib
Dec 04 00:21:44 Finished candle/syntax-lib                                       11s 701MB
Dec 04 00:21:45 Starting candle/standard/syntax
Dec 04 00:23:38 Finished candle/standard/syntax                                1m53s   1GB
Dec 04 00:23:38 Starting candle/standard/semantics
Dec 04 00:25:26 Finished candle/standard/semantics                             1m47s   1GB
Dec 04 00:25:26 Starting candle/standard/monadic
Dec 04 00:27:15 Finished candle/standard/monadic                               1m49s   1GB
Dec 04 00:27:15 Starting candle/standard/ml_kernel
Dec 04 00:33:16 Finished candle/standard/ml_kernel                             6m00s   3GB
Dec 04 00:33:16 Starting candle/overloading/syntax
Dec 04 00:36:32 Finished candle/overloading/syntax                             3m15s   1GB
Dec 04 00:36:32 Starting candle/overloading/semantics
Dec 04 00:48:46 Finished candle/overloading/semantics                         12m13s   2GB
Dec 04 00:48:46 Starting pancake
Dec 04 00:50:47 Finished pancake                                               2m00s   2GB
Dec 04 00:50:47 Starting pancake/ffi
Dec 04 00:50:48 Finished pancake/ffi                                              0s   4MB
Dec 04 00:50:48 Starting pancake/semantics
Dec 04 00:53:14 Finished pancake/semantics                                     2m26s   1GB
Dec 04 00:53:14 Starting pancake/proofs
Dec 04 01:06:01 Finished pancake/proofs                                       12m46s   6GB
Dec 04 01:06:01 Starting characteristic/examples
Dec 04 01:07:27 Finished characteristic/examples                               1m25s   3GB
Dec 04 01:07:27 Starting tutorial/solutions
Dec 04 01:24:33 Finished tutorial/solutions                                   17m04s   9GB
Dec 04 01:24:33 Starting translator/monadic/examples
Dec 04 01:28:06 Finished translator/monadic/examples                           3m32s   2GB
Dec 04 01:28:06 Starting examples
Dec 04 01:38:02 Finished examples                                              9m55s   4GB
Dec 04 01:38:03 Starting examples/compilation/x64
Dec 04 04:12:30 Finished examples/compilation/x64                           2h34m26s  19GB
Dec 04 04:12:30 Starting examples/compilation/x64/proofs
Dec 04 04:14:40 Finished examples/compilation/x64/proofs                       2m09s   3GB
Dec 04 04:14:40 Starting examples/compilation/ag32
Dec 04 04:50:33 Finished examples/compilation/ag32                            35m52s   9GB
Dec 04 04:50:33 Starting examples/compilation/ag32/proofs
Dec 04 04:51:23 Finished examples/compilation/ag32/proofs                        50s   3GB
Dec 04 04:51:23 Starting examples/cost
Dec 04 05:51:56 Finished examples/cost                                      1h00m32s   7GB
Dec 04 05:51:56 Starting examples/lpr_checker
Dec 04 05:52:46 Finished examples/lpr_checker                                    49s 838MB
Dec 04 05:52:46 Starting examples/lpr_checker/array
Dec 04 06:23:23 Finished examples/lpr_checker/array                           30m36s   5GB
Dec 04 06:23:23 Starting examples/lpr_checker/array/compilation
Dec 04 07:51:48 Finished examples/lpr_checker/array/compilation             1h28m24s  35GB
Dec 04 07:51:48 Starting examples/lpr_checker/array/compilation/proofs
Dec 04 07:53:43 Finished examples/lpr_checker/array/compilation/proofs         1m54s   4GB
Dec 04 07:53:43 Starting examples/opentheory
Dec 04 08:03:45 Finished examples/opentheory                                  10m02s   3GB
Dec 04 08:03:46 Starting examples/opentheory
Dec 04 08:03:47 Finished examples/opentheory                                      1s  26MB
Dec 04 08:03:47 Starting examples/opentheory/compilation
Dec 04 08:40:08 Finished examples/opentheory/compilation                      36m20s  28GB
Dec 04 08:40:09 Starting examples/opentheory/compilation/proofs
Dec 04 08:40:51 Finished examples/opentheory/compilation/proofs                  42s   3GB
Dec 04 08:40:51 Starting examples/opentheory/compilation/ag32
Dec 04 09:21:18 Finished examples/opentheory/compilation/ag32                 40m25s  35GB
Dec 04 09:21:18 Starting examples/opentheory/compilation/ag32/proofs
Dec 04 09:23:26 Finished examples/opentheory/compilation/ag32/proofs           2m07s   6GB
Dec 04 09:23:26 Starting examples/sat_encodings
Dec 04 09:25:18 Finished examples/sat_encodings                                1m51s 800MB
Dec 04 09:25:18 Starting examples/sat_encodings/case_studies
Dec 04 09:27:01 Finished examples/sat_encodings/case_studies                   1m42s 713MB
Dec 04 09:27:01 Starting examples/sat_encodings/translation
Dec 04 09:32:55 Finished examples/sat_encodings/translation                    5m54s   3GB
Dec 04 09:32:56 Starting examples/sat_encodings/translation/compilation
Dec 04 10:27:06 Finished examples/sat_encodings/translation/compilation       54m09s  19GB
Dec 04 10:27:06 Starting translator/okasaki-examples
Dec 04 10:31:57 Finished translator/okasaki-examples                           4m50s   1GB
Dec 04 10:31:57 Starting translator/other-examples
Dec 04 10:32:44 Finished translator/other-examples                               46s   1GB
Dec 04 10:32:44 Starting compiler/parsing/tests
Dec 04 10:33:15 Finished compiler/parsing/tests                                  30s 531MB
Dec 04 10:33:15 Starting compiler/inference/tests
Dec 04 10:41:34 Finished compiler/inference/tests                              8m18s   5GB
Dec 04 10:41:34 Starting compiler/bootstrap/translation Dec 04 10:41:34 32412s