Job 1475

CakeML:ea2e296a1d276fbc43647b0a1f9e80006a0dc4ee
  Updates after moving sptree closure/reachability theories to HOL [Feb 15 16:38:13]
#815 (master)
Merging into:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:3f7004dd05c08c5551cb3ab2dbfe6eccdb876a19
  Fix some problems in generation of REFERENCE manual [Feb 15 02:29:05]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 17 17:30:01 Claimed job
Feb 17 17:30:05 Building HOL
Feb 17 17:45:51 Starting developers
Feb 17 17:45:56 Finished developers                                               4s  94MB
Feb 17 17:45:56 Starting developers/bin
Feb 17 17:46:03 Finished developers/bin                                           6s   1GB
Feb 17 17:46:03 Starting semantics/ffi
Feb 17 17:46:15 Finished semantics/ffi                                           11s 239MB
Feb 17 17:46:15 Starting semantics
Feb 17 17:47:49 Finished semantics                                             1m34s   1GB
Feb 17 17:47:49 Starting semantics/proofs
Feb 17 17:51:26 Finished semantics/proofs                                      3m36s   1GB
Feb 17 17:51:27 Starting semantics/alt_semantics
Feb 17 17:51:36 Finished semantics/alt_semantics                                  8s 316MB
Feb 17 17:51:36 Starting semantics/alt_semantics/proofs
Feb 17 17:53:51 Finished semantics/alt_semantics/proofs                        2m14s 869MB
Feb 17 17:53:51 Starting basis/pure
Feb 17 17:56:54 Finished basis/pure                                            3m03s 926MB
Feb 17 17:56:55 Starting translator
Feb 17 17:59:40 Finished translator                                            2m45s   1GB
Feb 17 17:59:40 Starting compiler/parsing
Feb 17 18:00:55 Finished compiler/parsing                                      1m14s   2GB
Feb 17 18:00:55 Starting characteristic
Feb 17 18:07:02 Finished characteristic                                        6m06s   2GB
Feb 17 18:07:02 Starting translator/monadic
Feb 17 18:08:42 Finished translator/monadic                                    1m39s   1GB
Feb 17 18:08:43 Starting basis
Feb 17 18:55:13 Finished basis                                                46m30s  11GB
Feb 17 18:55:14 Starting compiler/inference
Feb 17 18:56:27 Finished compiler/inference                                    1m13s 942MB
Feb 17 18:56:27 Starting compiler/backend/reg_alloc
Feb 17 18:57:33 Finished compiler/backend/reg_alloc                            1m05s   1GB
Feb 17 18:57:34 Starting compiler/backend/gc
Feb 17 19:01:18 Finished compiler/backend/gc                                   3m44s   2GB
Feb 17 19:01:19 Starting compiler/backend
Feb 17 19:06:20 Finished compiler/backend                                      5m01s   4GB
Feb 17 19:06:20 Starting compiler/encoders/asm
Feb 17 19:06:43 Finished compiler/encoders/asm                                   22s 699MB
Feb 17 19:06:43 Starting compiler/encoders/x64
Feb 17 19:07:48 Finished compiler/encoders/x64                                 1m04s 745MB
Feb 17 19:07:48 Starting compiler/encoders/arm7
Feb 17 19:10:02 Finished compiler/encoders/arm7                                2m13s   1GB
Feb 17 19:10:02 Starting compiler/encoders/arm8
Feb 17 19:10:42 Finished compiler/encoders/arm8                                  39s 652MB
Feb 17 19:10:42 Starting compiler/encoders/mips
Feb 17 19:12:19 Finished compiler/encoders/mips                                1m36s   1GB
Feb 17 19:12:19 Starting compiler/encoders/riscv
Feb 17 19:14:10 Finished compiler/encoders/riscv                               1m50s   1GB
Feb 17 19:14:10 Starting compiler/encoders/ag32
Feb 17 19:14:29 Finished compiler/encoders/ag32                                  18s 822MB
Feb 17 19:14:29 Starting compiler/backend/x64
Feb 17 19:14:49 Finished compiler/backend/x64                                    19s   1GB
Feb 17 19:14:49 Starting compiler/backend/arm7
Feb 17 19:15:10 Finished compiler/backend/arm7                                   21s   1GB
Feb 17 19:15:10 Starting compiler/backend/arm8
Feb 17 19:15:30 Finished compiler/backend/arm8                                   19s   1GB
Feb 17 19:15:30 Starting compiler/backend/mips
Feb 17 19:15:51 Finished compiler/backend/mips                                   20s   1GB
Feb 17 19:15:51 Starting compiler/backend/riscv
Feb 17 19:16:12 Finished compiler/backend/riscv                                  20s   1GB
Feb 17 19:16:12 Starting compiler/backend/ag32
Feb 17 19:17:25 Finished compiler/backend/ag32                                 1m12s 966MB
Feb 17 19:17:25 Starting compiler/parsing/proofs
Feb 17 19:23:17 Finished compiler/parsing/proofs                               5m52s   1GB
Feb 17 19:23:18 Starting compiler/inference/proofs
Feb 17 19:25:56 Finished compiler/inference/proofs                             2m37s 961MB
Feb 17 19:25:56 Starting compiler/backend/semantics
Feb 17 19:58:45 Finished compiler/backend/semantics                           32m48s   2GB
Feb 17 19:58:45 Starting compiler/backend/reg_alloc/proofs
Feb 17 20:02:34 Finished compiler/backend/reg_alloc/proofs                     3m48s 830MB
Feb 17 20:02:34 Starting compiler/backend/proofs
Feb 17 21:01:07 Finished compiler/backend/proofs                              58m32s  16GB
Feb 17 21:01:07 Starting compiler/encoders/x64/proofs
Feb 17 21:11:38 Finished compiler/encoders/x64/proofs                         10m31s   4GB
Feb 17 21:11:38 Starting compiler/encoders/arm7/proofs
Feb 17 21:25:53 Finished compiler/encoders/arm7/proofs                        14m14s   6GB
Feb 17 21:25:53 Starting compiler/encoders/arm8/proofs
Feb 17 21:33:00 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Feb 17 21:33:00 Starting compiler/encoders/mips/proofs
Feb 17 21:44:05 Finished compiler/encoders/mips/proofs                        11m05s   2GB
Feb 17 21:44:05 Starting compiler/encoders/riscv/proofs
Feb 17 21:53:41 Finished compiler/encoders/riscv/proofs                        9m35s   1GB
Feb 17 21:53:41 Starting compiler/encoders/ag32/proofs
Feb 17 21:56:31 Finished compiler/encoders/ag32/proofs                         2m50s 773MB
Feb 17 21:56:31 Starting compiler/backend/x64/proofs
Feb 17 21:56:54 Finished compiler/backend/x64/proofs                             22s   1GB
Feb 17 21:56:55 Starting compiler/backend/arm7/proofs
Feb 17 21:57:18 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 17 21:57:18 Starting compiler/backend/arm8/proofs
Feb 17 21:57:40 Finished compiler/backend/arm8/proofs                            22s   1GB
Feb 17 21:57:40 Starting compiler/backend/mips/proofs
Feb 17 21:58:03 Finished compiler/backend/mips/proofs                            23s   1GB
Feb 17 21:58:04 Starting compiler/backend/riscv/proofs
Feb 17 21:58:27 Finished compiler/backend/riscv/proofs                           22s   1GB
Feb 17 21:58:27 Starting compiler/backend/ag32/proofs
Feb 17 22:11:59 Finished compiler/backend/ag32/proofs                         13m31s   2GB
Feb 17 22:11:59 Starting compiler/proofs
Feb 17 22:13:56 Finished compiler/proofs                                       1m56s   3GB
Feb 17 22:13:56 Starting candle/set-theory
Feb 17 22:14:25 Finished candle/set-theory                                       28s 717MB
Feb 17 22:14:25 Starting candle/syntax-lib
Feb 17 22:14:36 Finished candle/syntax-lib                                       10s 503MB
Feb 17 22:14:36 Starting candle/standard/syntax
Feb 17 22:16:31 Finished candle/standard/syntax                                1m54s 874MB
Feb 17 22:16:31 Starting candle/standard/semantics
Feb 17 22:18:19 Finished candle/standard/semantics                             1m47s   1GB
Feb 17 22:18:19 Starting candle/standard/monadic
Feb 17 22:20:08 Finished candle/standard/monadic                               1m48s   1GB
Feb 17 22:20:08 Starting candle/standard/ml_kernel
Feb 17 22:26:10 Finished candle/standard/ml_kernel                             6m01s   3GB
Feb 17 22:26:10 Starting candle/overloading/syntax
Feb 17 22:29:27 Finished candle/overloading/syntax                             3m16s   1GB
Feb 17 22:29:27 Starting candle/overloading/semantics
Feb 17 22:42:25 Finished candle/overloading/semantics                         12m57s   3GB
Feb 17 22:42:25 Starting characteristic/examples
Feb 17 22:43:47 Finished characteristic/examples                               1m21s   2GB
Feb 17 22:43:47 Starting tutorial/solutions Feb 17 22:43:47 1204s