Job 1430

CakeML:81170439e224ffe3e027792ffffc97de042a2ba1
  Tidy some sptree definitions/theorems [Jan 08 16:01:49]
#810 (master)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
  Fix breakage caused by change to sorted_map in HOL [Jan 05 15:57:59]
HOL:89e07c5a43c0637bc614b4396e6a8b3cb902cedb
  Get the Interaction-emacs manual built properly as part of release [Jan 06 05:48:29]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 10 23:23:59 Claimed job
Jan 10 23:24:02 Reusing HOL
Jan 10 23:24:10 Starting developers
Jan 10 23:24:10 Finished developers                                               0s  35MB
Jan 10 23:24:11 Starting developers/bin
Jan 10 23:24:17 Finished developers/bin                                           6s   1GB
Jan 10 23:24:17 Starting semantics/ffi
Jan 10 23:24:27 Finished semantics/ffi                                            9s 269MB
Jan 10 23:24:27 Starting semantics
Jan 10 23:25:51 Finished semantics                                             1m23s   1GB
Jan 10 23:25:51 Starting semantics/proofs
Jan 10 23:29:10 Finished semantics/proofs                                      3m19s   1GB
Jan 10 23:29:10 Starting semantics/alt_semantics
Jan 10 23:29:18 Finished semantics/alt_semantics                                  8s 392MB
Jan 10 23:29:19 Starting semantics/alt_semantics/proofs
Jan 10 23:31:26 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Jan 10 23:31:26 Starting basis/pure
Jan 10 23:32:18 Finished basis/pure                                              52s   1GB
Jan 10 23:32:19 Starting translator
Jan 10 23:34:56 Finished translator                                            2m37s   2GB
Jan 10 23:34:56 Starting compiler/parsing
Jan 10 23:36:04 Finished compiler/parsing                                      1m08s   4GB
Jan 10 23:36:05 Starting characteristic
Jan 10 23:42:03 Finished characteristic                                        5m57s   3GB
Jan 10 23:42:03 Starting translator/monadic
Jan 10 23:43:49 Finished translator/monadic                                    1m45s   3GB
Jan 10 23:43:49 Starting basis
Jan 11 00:17:07 Finished basis                                                33m16s  31GB
Jan 11 00:17:08 Starting compiler/inference
Jan 11 00:18:11 Finished compiler/inference                                    1m03s   1GB
Jan 11 00:18:12 Starting compiler/backend/reg_alloc
Jan 11 00:19:16 Finished compiler/backend/reg_alloc                            1m04s   1GB
Jan 11 00:19:16 Starting compiler/backend/gc
Jan 11 00:22:38 Finished compiler/backend/gc                                   3m21s   3GB
Jan 11 00:22:38 Starting compiler/backend
Jan 11 10:06:27 Resuming compiler/backend