Job 1182

CakeML:658771300986c1238e414b06f1443f7f4f08424a
  Merge pull request #723 from talsewell/explorer-data [Feb 11 23:28:15]
HOL:bbc6f9a1dc624543ead89ce3c72e7a8d773e37db
  Added BOREL_INDUCT (was: Induct_on_Borel_functions) [Feb 09 23:16:11]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 12 18:13:05 Claimed job
Feb 12 18:13:08 Building HOL
Feb 12 18:23:42 Starting developers
Feb 12 18:23:44 Finished developers                                               2s 126MB
Feb 12 18:23:44 Starting developers/bin
Feb 12 18:23:51 Finished developers/bin                                           6s   1GB
Feb 12 18:23:51 Starting semantics/ffi
Feb 12 18:24:00 Finished semantics/ffi                                            8s 244MB
Feb 12 18:24:00 Starting semantics
Feb 12 18:25:25 Finished semantics                                             1m25s   1GB
Feb 12 18:25:26 Starting semantics/proofs
Feb 12 18:28:35 Finished semantics/proofs                                      3m09s   1GB
Feb 12 18:28:35 Starting semantics/alt_semantics
Feb 12 18:28:42 Finished semantics/alt_semantics                                  6s 308MB
Feb 12 18:28:42 Starting semantics/alt_semantics/proofs
Feb 12 18:30:41 Finished semantics/alt_semantics/proofs                        1m58s 905MB
Feb 12 18:30:41 Starting basis/pure
Feb 12 18:33:38 Finished basis/pure                                            2m56s 864MB
Feb 12 18:33:38 Starting translator
Feb 12 18:36:08 Finished translator                                            2m30s   1GB
Feb 12 18:36:09 Starting compiler/parsing
Feb 12 18:37:13 Finished compiler/parsing                                      1m04s   2GB
Feb 12 18:37:13 Starting characteristic
Feb 12 18:42:49 Finished characteristic                                        5m35s   1GB
Feb 12 18:42:49 Starting translator/monadic
Feb 12 18:44:25 Finished translator/monadic                                    1m35s   2GB
Feb 12 18:44:25 Starting basis
Feb 12 19:16:49 Finished basis                                                32m23s  21GB
Feb 12 19:16:49 Starting compiler/inference
Feb 12 19:18:56 Finished compiler/inference                                    2m06s   3GB
Feb 12 19:18:56 Starting compiler/backend/reg_alloc
Feb 12 19:19:56 Finished compiler/backend/reg_alloc                            1m00s   1GB
Feb 12 19:19:57 Starting compiler/backend/gc
Feb 12 19:23:10 Finished compiler/backend/gc                                   3m13s   2GB
Feb 12 19:23:10 Starting compiler/backend
Feb 12 19:27:32 Finished compiler/backend                                      4m21s   3GB
Feb 12 19:27:32 Starting compiler/encoders/asm
Feb 12 19:27:53 Finished compiler/encoders/asm                                   20s 784MB
Feb 12 19:27:53 Starting compiler/encoders/x64
Feb 12 19:28:46 Finished compiler/encoders/x64                                   52s 993MB
Feb 12 19:28:47 Starting compiler/encoders/arm7
Feb 12 19:30:27 Finished compiler/encoders/arm7                                1m40s   1GB
Feb 12 19:30:27 Starting compiler/encoders/arm8
Feb 12 19:30:59 Finished compiler/encoders/arm8                                  31s 849MB
Feb 12 19:30:59 Starting compiler/encoders/mips
Feb 12 19:32:03 Finished compiler/encoders/mips                                1m03s   1GB
Feb 12 19:32:03 Starting compiler/encoders/riscv
Feb 12 19:33:23 Finished compiler/encoders/riscv                               1m20s   1GB
Feb 12 19:33:23 Starting compiler/encoders/ag32
Feb 12 19:33:39 Finished compiler/encoders/ag32                                  15s 784MB
Feb 12 19:33:40 Starting compiler/backend/x64
Feb 12 19:33:57 Finished compiler/backend/x64                                    17s   1GB
Feb 12 19:33:57 Starting compiler/backend/arm7
Feb 12 19:34:16 Finished compiler/backend/arm7                                   19s   1GB
Feb 12 19:34:17 Starting compiler/backend/arm8
Feb 12 19:34:34 Finished compiler/backend/arm8                                   16s   1GB
Feb 12 19:34:34 Starting compiler/backend/mips
Feb 12 19:34:52 Finished compiler/backend/mips                                   18s   1GB
Feb 12 19:34:52 Starting compiler/backend/riscv
Feb 12 19:35:10 Finished compiler/backend/riscv                                  17s   1GB
Feb 12 19:35:10 Starting compiler/backend/ag32
Feb 12 19:36:16 Finished compiler/backend/ag32                                 1m05s   1GB
Feb 12 19:36:16 Starting compiler/parsing/proofs
Feb 12 19:41:54 Finished compiler/parsing/proofs                               5m37s 967MB
Feb 12 19:41:54 Starting compiler/inference/proofs
Feb 12 19:44:47 Finished compiler/inference/proofs                             2m53s   1GB
Feb 12 19:44:47 Starting compiler/backend/semantics
Feb 12 20:11:28 Finished compiler/backend/semantics                           26m40s   3GB
Feb 12 20:11:28 Starting compiler/backend/reg_alloc/proofs
Feb 12 20:14:42 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Feb 12 20:14:42 Starting compiler/backend/proofs
Feb 12 21:15:05 Finished compiler/backend/proofs                            1h00m22s  17GB
Feb 12 21:15:06 Starting compiler/encoders/x64/proofs
Feb 12 21:24:08 Finished compiler/encoders/x64/proofs                          9m02s   4GB
Feb 12 21:24:09 Starting compiler/encoders/arm7/proofs
Feb 12 21:36:12 Finished compiler/encoders/arm7/proofs                        12m02s   3GB
Feb 12 21:36:12 Starting compiler/encoders/arm8/proofs
Feb 12 21:42:20 Finished compiler/encoders/arm8/proofs                         6m07s   1GB
Feb 12 21:42:20 Starting compiler/encoders/mips/proofs
Feb 12 21:51:42 Finished compiler/encoders/mips/proofs                         9m21s   2GB
Feb 12 21:51:42 Starting compiler/encoders/riscv/proofs
Feb 12 22:00:06 Finished compiler/encoders/riscv/proofs                        8m24s   1GB
Feb 12 22:00:06 Starting compiler/encoders/ag32/proofs
Feb 12 22:02:29 Finished compiler/encoders/ag32/proofs                         2m22s 730MB
Feb 12 22:02:29 Starting compiler/backend/x64/proofs
Feb 12 22:02:49 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 12 22:02:49 Starting compiler/backend/arm7/proofs
Feb 12 22:03:11 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 12 22:03:11 Starting compiler/backend/arm8/proofs
Feb 12 22:03:29 Finished compiler/backend/arm8/proofs                            17s 900MB
Feb 12 22:03:29 Starting compiler/backend/mips/proofs
Feb 12 22:03:49 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 12 22:03:49 Starting compiler/backend/riscv/proofs
Feb 12 22:04:09 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 12 22:04:09 Starting compiler/backend/ag32/proofs
Feb 12 22:16:11 Finished compiler/backend/ag32/proofs                         12m01s   3GB
Feb 12 22:16:11 Starting compiler/proofs
Feb 12 22:17:54 Finished compiler/proofs                                       1m42s   3GB
Feb 12 22:17:54 Starting candle/set-theory
Feb 12 22:18:21 Finished candle/set-theory                                       27s 748MB
Feb 12 22:18:22 Starting candle/syntax-lib
Feb 12 22:18:31 Finished candle/syntax-lib                                        9s 655MB
Feb 12 22:18:32 Starting candle/standard/syntax
Feb 12 22:20:16 Finished candle/standard/syntax                                1m43s   1GB
Feb 12 22:20:16 Starting candle/standard/semantics
Feb 12 22:21:55 Finished candle/standard/semantics                             1m39s   1GB
Feb 12 22:21:55 Starting candle/standard/monadic
Feb 12 22:23:29 Finished candle/standard/monadic                               1m33s   1GB
Feb 12 22:23:29 Starting candle/standard/ml_kernel
Feb 12 22:28:31 Finished candle/standard/ml_kernel                             5m02s   3GB
Feb 12 22:28:31 Starting candle/standard/opentheory
Feb 12 22:37:36 Finished candle/standard/opentheory                            9m04s   4GB
Feb 12 22:37:36 Starting candle/standard/opentheory/compilation
Feb 12 23:07:44 Finished candle/standard/opentheory/compilation               30m08s  22GB
Feb 12 23:07:44 Starting candle/standard/opentheory/compilation/proofs
Feb 12 23:08:27 Finished candle/standard/opentheory/compilation/proofs           42s   3GB
Feb 12 23:08:27 Starting characteristic/examples
Feb 12 23:09:57 Finished characteristic/examples                               1m29s   2GB
Feb 12 23:09:57 Starting tutorial/solutions
Feb 12 23:24:45 Finished tutorial/solutions                                   14m47s   6GB
Feb 12 23:24:45 Starting translator/monadic/examples
Feb 12 23:27:44 Finished translator/monadic/examples                           2m58s   2GB
Feb 12 23:27:44 Starting examples
Feb 12 23:37:06 Finished examples                                              9m21s   3GB
Feb 12 23:37:06 Starting examples/compilation/x64
Feb 13 01:51:13 Finished examples/compilation/x64                           2h14m06s  15GB
Feb 13 01:51:13 Starting examples/compilation/x64/proofs
Feb 13 01:52:51 Finished examples/compilation/x64/proofs                       1m37s   2GB
Feb 13 01:52:52 Starting examples/compilation/ag32
Feb 13 02:23:45 Finished examples/compilation/ag32                            30m53s   5GB
Feb 13 02:23:46 Starting examples/compilation/ag32/proofs
Feb 13 02:24:29 Finished examples/compilation/ag32/proofs                        43s   3GB
Feb 13 02:24:30 Starting examples/cost
Feb 13 03:05:06 Finished examples/cost                                        40m35s   7GB
Feb 13 03:05:06 Starting examples/lpr_checker
Feb 13 03:08:46 Finished examples/lpr_checker                                  3m39s   4GB
Feb 13 03:08:46 Starting examples/lpr_checker/compilation
Feb 13 03:25:29 Finished examples/lpr_checker/compilation                     16m43s  10GB
Feb 13 03:25:30 Starting examples/lpr_checker/compilation/proofs
Feb 13 03:26:07 Finished examples/lpr_checker/compilation/proofs                 37s   3GB
Feb 13 03:26:07 Starting examples/lpr_checker/array
Feb 13 03:35:22 Finished examples/lpr_checker/array                            9m14s   3GB
Feb 13 03:35:22 Starting examples/lpr_checker/array/compilation
Feb 13 03:50:56 Finished examples/lpr_checker/array/compilation               15m33s   7GB
Feb 13 03:50:56 Starting examples/lpr_checker/array/compilation/proofs
Feb 13 03:51:43 Finished examples/lpr_checker/array/compilation/proofs           46s   3GB
Feb 13 03:51:43 Starting translator/okasaki-examples
Feb 13 03:55:59 Finished translator/okasaki-examples                           4m16s   1GB
Feb 13 03:56:00 Starting translator/other-examples
Feb 13 03:57:49 Finished translator/other-examples                             1m49s   1GB
Feb 13 03:57:50 Starting compiler/parsing/tests
Feb 13 03:58:14 Finished compiler/parsing/tests                                  24s 611MB
Feb 13 03:58:14 Starting compiler/inference/tests
Feb 13 04:02:37 Finished compiler/inference/tests                              4m22s   3GB
Feb 13 04:02:37 Starting compiler/bootstrap/translation
Feb 13 07:33:35 Finished compiler/bootstrap/translation                     3h30m55s  38GB
Feb 13 07:33:35 Starting unverified/sexpr-bootstrap/x64/64
Feb 13 07:48:58 Finished unverified/sexpr-bootstrap/x64/64                    15m22s   7GB
Feb 13 07:48:58 Starting unverified/sexpr-bootstrap/x64/32
Feb 13 07:59:47 Finished unverified/sexpr-bootstrap/x64/32                    10m48s   9GB
Feb 13 07:59:47 Starting compiler/benchmarks
Feb 13 08:38:43 Finished compiler/benchmarks                                  38m55s   2GB
Feb 13 08:38:43 Starting compiler/bootstrap/compilation/x64/64
Feb 13 23:47:54 Finished compiler/bootstrap/compilation/x64/64             15h09m08s  64GB
Feb 13 23:47:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 13 23:51:52 Finished compiler/bootstrap/compilation/x64/64/proofs          3m58s  16GB
Feb 13 23:51:52 Starting compiler/bootstrap/compilation/x64/32
Feb 14 13:04:44 Finished compiler/bootstrap/compilation/x64/32             13h12m50s  64GB
Feb 14 13:04:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 14 13:08:12 Finished compiler/bootstrap/compilation/x64/32/proofs          3m27s  14GB
Feb 14 13:08:12 Starting compiler/bootstrap/compilation/ag32/32
Feb 15 04:12:09 Finished compiler/bootstrap/compilation/ag32/32            15h03m56s  64GB
Feb 15 04:12:09 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 15 04:27:34 Finished compiler/bootstrap/compilation/ag32/32/proofs        15m24s  33GB
Feb 15 04:27:34 SUCCESS