Job 1185

CakeML:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
  Merge pull request #714 from CakeML/nopacklib [Feb 16 18:25:28]
HOL:bbc6f9a1dc624543ead89ce3c72e7a8d773e37db
  Added BOREL_INDUCT (was: Induct_on_Borel_functions) [Feb 09 23:16:11]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Feb 16 18:29:19 Claimed job
Feb 16 18:29:24 Building HOL
Feb 16 18:40:43 Starting developers
Feb 16 18:40:47 Finished developers                                               4s 119MB
Feb 16 18:40:47 Starting developers/bin
Feb 16 18:40:54 Finished developers/bin                                           6s   1GB
Feb 16 18:40:54 Starting semantics/ffi
Feb 16 18:41:04 Finished semantics/ffi                                           10s 254MB
Feb 16 18:41:04 Starting semantics
Feb 16 18:42:30 Finished semantics                                             1m26s   1GB
Feb 16 18:42:30 Starting semantics/proofs
Feb 16 18:45:35 Finished semantics/proofs                                      3m04s 971MB
Feb 16 18:45:35 Starting semantics/alt_semantics
Feb 16 18:45:43 Finished semantics/alt_semantics                                  7s 317MB
Feb 16 18:45:43 Starting semantics/alt_semantics/proofs
Feb 16 18:47:41 Finished semantics/alt_semantics/proofs                        1m57s 850MB
Feb 16 18:47:41 Starting basis/pure
Feb 16 18:50:28 Finished basis/pure                                            2m46s 896MB
Feb 16 18:50:28 Starting translator
Feb 16 18:52:55 Finished translator                                            2m27s   1GB
Feb 16 18:52:55 Starting compiler/parsing
Feb 16 18:53:59 Finished compiler/parsing                                      1m03s   3GB
Feb 16 18:53:59 Starting characteristic
Feb 16 18:59:33 Finished characteristic                                        5m33s   2GB
Feb 16 18:59:33 Starting translator/monadic
Feb 16 19:01:03 Finished translator/monadic                                    1m30s   1GB
Feb 16 19:01:03 Starting basis
Feb 16 19:31:06 Finished basis                                                30m01s  19GB
Feb 16 19:31:06 Starting compiler/inference
Feb 16 19:33:14 Finished compiler/inference                                    2m07s   2GB
Feb 16 19:33:14 Starting compiler/backend/reg_alloc
Feb 16 19:34:14 Finished compiler/backend/reg_alloc                              59s   1GB
Feb 16 19:34:14 Starting compiler/backend/gc
Feb 16 19:37:23 Finished compiler/backend/gc                                   3m08s   2GB
Feb 16 19:37:23 Starting compiler/backend
Feb 16 19:41:31 Finished compiler/backend                                      4m08s   3GB
Feb 16 19:41:31 Starting compiler/encoders/asm
Feb 16 19:41:52 Finished compiler/encoders/asm                                   20s 824MB
Feb 16 19:41:52 Starting compiler/encoders/x64
Feb 16 19:42:46 Finished compiler/encoders/x64                                   53s 997MB
Feb 16 19:42:46 Starting compiler/encoders/arm7
Feb 16 19:44:30 Finished compiler/encoders/arm7                                1m43s   1GB
Feb 16 19:44:30 Starting compiler/encoders/arm8
Feb 16 19:45:01 Finished compiler/encoders/arm8                                  31s 923MB
Feb 16 19:45:01 Starting compiler/encoders/mips
Feb 16 19:46:07 Finished compiler/encoders/mips                                1m05s 923MB
Feb 16 19:46:07 Starting compiler/encoders/riscv
Feb 16 19:47:24 Finished compiler/encoders/riscv                               1m17s   1GB
Feb 16 19:47:25 Starting compiler/encoders/ag32
Feb 16 19:47:41 Finished compiler/encoders/ag32                                  16s 762MB
Feb 16 19:47:41 Starting compiler/backend/x64
Feb 16 19:47:58 Finished compiler/backend/x64                                    16s   1GB
Feb 16 19:47:58 Starting compiler/backend/arm7
Feb 16 19:48:17 Finished compiler/backend/arm7                                   18s   1GB
Feb 16 19:48:17 Starting compiler/backend/arm8
Feb 16 19:48:34 Finished compiler/backend/arm8                                   16s   1GB
Feb 16 19:48:34 Starting compiler/backend/mips
Feb 16 19:48:52 Finished compiler/backend/mips                                   18s   1GB
Feb 16 19:48:52 Starting compiler/backend/riscv
Feb 16 19:49:10 Finished compiler/backend/riscv                                  18s   1GB
Feb 16 19:49:10 Starting compiler/backend/ag32
Feb 16 19:50:15 Finished compiler/backend/ag32                                 1m04s   1GB
Feb 16 19:50:16 Starting compiler/parsing/proofs
Feb 16 19:56:01 Finished compiler/parsing/proofs                               5m44s 860MB
Feb 16 19:56:01 Starting compiler/inference/proofs
Feb 16 19:58:50 Finished compiler/inference/proofs                             2m48s   1GB
Feb 16 19:58:50 Starting compiler/backend/semantics
Feb 16 20:24:41 Finished compiler/backend/semantics                           25m50s   2GB
Feb 16 20:24:41 Starting compiler/backend/reg_alloc/proofs
Feb 16 20:27:56 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Feb 16 20:27:56 Starting compiler/backend/proofs
Feb 16 21:26:03 Finished compiler/backend/proofs                              58m07s  12GB
Feb 16 21:26:03 Starting compiler/encoders/x64/proofs
Feb 16 21:34:58 Finished compiler/encoders/x64/proofs                          8m54s   5GB
Feb 16 21:34:58 Starting compiler/encoders/arm7/proofs
Feb 16 21:46:58 Finished compiler/encoders/arm7/proofs                        11m59s   3GB
Feb 16 21:46:58 Starting compiler/encoders/arm8/proofs
Feb 16 21:52:59 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
Feb 16 21:52:59 Starting compiler/encoders/mips/proofs
Feb 16 22:02:05 Finished compiler/encoders/mips/proofs                         9m05s   2GB
Feb 16 22:02:05 Starting compiler/encoders/riscv/proofs
Feb 16 22:10:04 Finished compiler/encoders/riscv/proofs                        7m58s   1GB
Feb 16 22:10:04 Starting compiler/encoders/ag32/proofs
Feb 16 22:12:26 Finished compiler/encoders/ag32/proofs                         2m22s 643MB
Feb 16 22:12:26 Starting compiler/backend/x64/proofs
Feb 16 22:12:46 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 16 22:12:46 Starting compiler/backend/arm7/proofs
Feb 16 22:13:07 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 16 22:13:07 Starting compiler/backend/arm8/proofs
Feb 16 22:13:28 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 16 22:13:28 Starting compiler/backend/mips/proofs
Feb 16 22:13:48 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 16 22:13:48 Starting compiler/backend/riscv/proofs
Feb 16 22:14:07 Finished compiler/backend/riscv/proofs                           18s   1GB
Feb 16 22:14:07 Starting compiler/backend/ag32/proofs
Feb 16 22:26:14 Finished compiler/backend/ag32/proofs                         12m05s   1GB
Feb 16 22:26:14 Starting compiler/proofs
Feb 16 22:27:54 Finished compiler/proofs                                       1m39s   3GB
Feb 16 22:27:54 Starting candle/set-theory
Feb 16 22:28:21 Finished candle/set-theory                                       27s 733MB
Feb 16 22:28:21 Starting candle/syntax-lib
Feb 16 22:28:31 Finished candle/syntax-lib                                       10s 689MB
Feb 16 22:28:31 Starting candle/standard/syntax
Feb 16 22:30:16 Finished candle/standard/syntax                                1m44s   1GB
Feb 16 22:30:16 Starting candle/standard/semantics
Feb 16 22:31:55 Finished candle/standard/semantics                             1m38s   1GB
Feb 16 22:31:55 Starting candle/standard/monadic
Feb 16 22:33:28 Finished candle/standard/monadic                               1m33s   1GB
Feb 16 22:33:28 Starting candle/standard/ml_kernel
Feb 16 22:38:19 Finished candle/standard/ml_kernel                             4m50s   5GB
Feb 16 22:38:19 Starting candle/standard/opentheory
Feb 16 22:46:53 Finished candle/standard/opentheory                            8m33s   3GB
Feb 16 22:46:53 Starting candle/standard/opentheory/compilation
Feb 16 23:17:01 Finished candle/standard/opentheory/compilation               30m08s  13GB
Feb 16 23:17:02 Starting candle/standard/opentheory/compilation/proofs
Feb 16 23:17:37 Finished candle/standard/opentheory/compilation/proofs           35s   3GB
Feb 16 23:17:37 Starting characteristic/examples
Feb 16 23:18:47 Finished characteristic/examples                               1m09s   3GB
Feb 16 23:18:47 Starting tutorial/solutions
Feb 16 23:32:30 Finished tutorial/solutions                                   13m41s   8GB
Feb 16 23:32:30 Starting translator/monadic/examples
Feb 16 23:35:18 Finished translator/monadic/examples                           2m47s   2GB
Feb 16 23:35:18 Starting examples
Feb 16 23:42:34 Finished examples                                              7m16s   4GB
Feb 16 23:42:35 Starting examples/compilation/x64
Feb 17 01:51:52 Finished examples/compilation/x64                           2h09m15s  12GB
Feb 17 01:51:52 Starting examples/compilation/x64/proofs
Feb 17 01:53:16 Finished examples/compilation/x64/proofs                       1m24s   3GB
Feb 17 01:53:16 Starting examples/compilation/ag32
Feb 17 02:23:06 Finished examples/compilation/ag32                            29m49s   6GB
Feb 17 02:23:06 Starting examples/compilation/ag32/proofs
Feb 17 02:23:54 Finished examples/compilation/ag32/proofs                        47s   3GB
Feb 17 02:23:54 Starting examples/cost
Feb 17 03:02:29 Finished examples/cost                                        38m35s   6GB
Feb 17 03:02:29 Starting examples/lpr_checker
Feb 17 03:05:56 Finished examples/lpr_checker                                  3m26s   2GB
Feb 17 03:05:56 Starting examples/lpr_checker/compilation
Feb 17 03:21:34 Finished examples/lpr_checker/compilation                     15m37s   8GB
Feb 17 03:21:34 Starting examples/lpr_checker/compilation/proofs
Feb 17 03:22:09 Finished examples/lpr_checker/compilation/proofs                 35s   3GB
Feb 17 03:22:09 Starting examples/lpr_checker/array
Feb 17 03:29:34 Finished examples/lpr_checker/array                            7m24s   2GB
Feb 17 03:29:35 Starting examples/lpr_checker/array/compilation
Feb 17 03:44:18 Finished examples/lpr_checker/array/compilation               14m43s   8GB
Feb 17 03:44:18 Starting examples/lpr_checker/array/compilation/proofs
Feb 17 03:44:57 Finished examples/lpr_checker/array/compilation/proofs           39s   3GB
Feb 17 03:44:57 Starting translator/okasaki-examples
Feb 17 03:48:57 Finished translator/okasaki-examples                           3m59s   2GB
Feb 17 03:48:57 Starting translator/other-examples
Feb 17 03:50:48 Finished translator/other-examples                             1m50s   1GB
Feb 17 03:50:48 Starting compiler/parsing/tests
Feb 17 03:51:12 Finished compiler/parsing/tests                                  24s 644MB
Feb 17 03:51:12 Starting compiler/inference/tests
Feb 17 03:55:30 Finished compiler/inference/tests                              4m17s   3GB
Feb 17 03:55:30 Starting compiler/bootstrap/translation
Feb 17 07:18:09 Finished compiler/bootstrap/translation                     3h22m37s  40GB
Feb 17 07:18:09 Starting unverified/sexpr-bootstrap/x64/64
Feb 17 07:32:59 Finished unverified/sexpr-bootstrap/x64/64                    14m49s   5GB
Feb 17 07:32:59 Starting unverified/sexpr-bootstrap/x64/32
Feb 17 07:43:30 Finished unverified/sexpr-bootstrap/x64/32                    10m30s   8GB
Feb 17 07:43:30 Starting compiler/benchmarks
Feb 17 07:43:32 Finished compiler/benchmarks                                      1s  35MB
Feb 17 07:43:32 Starting compiler/bootstrap/compilation/x64/64
Feb 17 21:39:32 Finished compiler/bootstrap/compilation/x64/64             13h55m59s  64GB
Feb 17 21:39:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 17 21:42:40 Finished compiler/bootstrap/compilation/x64/64/proofs          3m07s  13GB
Feb 17 21:42:40 Starting compiler/bootstrap/compilation/x64/32
Feb 18 09:39:56 Finished compiler/bootstrap/compilation/x64/32             11h57m16s  64GB
Feb 18 09:39:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 18 09:42:56 Finished compiler/bootstrap/compilation/x64/32/proofs          2m59s  13GB
Feb 18 09:42:56 Starting compiler/bootstrap/compilation/ag32/32
Feb 20 10:40:09 Resuming compiler/bootstrap/compilation/ag32/32
Feb 20 15:10:48 Finished compiler/bootstrap/compilation/ag32/32             4h30m38s  64GB
Feb 20 15:10:48 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 20 15:37:31 Finished compiler/bootstrap/compilation/ag32/32/proofs        26m43s  30GB
Feb 20 15:37:31 SUCCESS