Job 893

CakeML:21975585998034b43aee723e21c7043f250a58fd
  Merge pull request #635 from CakeML/thm [May 22 08:49:19]
HOL:15a1e85b5308eeb3ca329cafe2c409f1fd21edfd
  Fix Holmake regressions arising from b03aecf7b [May 20 00:34:31]
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

May 22 08:51:42 Claimed job
May 22 08:51:46 Reusing HOL
May 22 08:51:52 Starting developers
May 22 08:51:52 Finished developers                                               0s  30MB
May 22 08:51:53 Starting developers/bin
May 22 08:51:56 Finished developers/bin                                           2s 144MB
May 22 08:51:56 Starting semantics/ffi
May 22 08:52:05 Finished semantics/ffi                                            8s 216MB
May 22 08:52:05 Starting semantics
May 22 08:53:22 Finished semantics                                             1m16s   1GB
May 22 08:53:22 Starting semantics/proofs
May 22 08:56:18 Finished semantics/proofs                                      2m55s   1GB
May 22 08:56:18 Starting basis/pure
May 22 08:57:02 Finished basis/pure                                              43s 636MB
May 22 08:57:02 Starting translator
May 22 08:58:39 Finished translator                                            1m36s   1GB
May 22 08:58:39 Starting compiler/parsing
May 22 08:59:36 Finished compiler/parsing                                        56s   1GB
May 22 08:59:36 Starting characteristic
May 22 09:04:41 Finished characteristic                                        5m04s   1GB
May 22 09:04:41 Starting translator/monadic
May 22 09:06:06 Finished translator/monadic                                    1m24s   1GB
May 22 09:06:06 Starting basis
May 22 09:22:53 Finished basis                                                16m46s   1GB
May 22 09:22:53 Starting compiler/inference
May 22 09:24:22 Finished compiler/inference                                    1m28s   1GB
May 22 09:24:23 Starting compiler/backend/reg_alloc
May 22 09:25:20 Finished compiler/backend/reg_alloc                              57s   1GB
May 22 09:25:21 Starting compiler/backend/gc
May 22 09:33:08 Finished compiler/backend/gc                                   7m47s   1GB
May 22 09:33:08 Starting compiler/backend
May 22 09:33:09 Finished compiler/backend                                         0s  43MB
May 22 09:33:10 Starting compiler/encoders/asm
May 22 09:33:10 Finished compiler/encoders/asm                                    0s  36MB
May 22 09:33:10 Starting compiler/encoders/x64
May 22 09:33:33 Finished compiler/encoders/x64                                   22s 761MB
May 22 09:33:33 Starting compiler/encoders/arm6
May 22 09:34:19 Finished compiler/encoders/arm6                                  45s   1GB
May 22 09:34:19 Starting compiler/encoders/arm8
May 22 09:34:31 Finished compiler/encoders/arm8                                  11s 550MB
May 22 09:34:31 Starting compiler/encoders/mips
May 22 09:34:47 Finished compiler/encoders/mips                                  15s 981MB
May 22 09:34:47 Starting compiler/encoders/riscv
May 22 09:35:00 Finished compiler/encoders/riscv                                 12s 814MB
May 22 09:35:01 Starting compiler/encoders/ag32
May 22 09:35:15 Finished compiler/encoders/ag32                                  14s 619MB
May 22 09:35:16 Starting compiler/backend/x64
May 22 09:35:31 Finished compiler/backend/x64                                    15s 855MB
May 22 09:35:32 Starting compiler/backend/arm6
May 22 09:35:50 Finished compiler/backend/arm6                                   17s   1GB
May 22 09:35:50 Starting compiler/backend/arm8
May 22 09:36:06 Finished compiler/backend/arm8                                   15s   1GB
May 22 09:36:06 Starting compiler/backend/mips
May 22 09:36:21 Finished compiler/backend/mips                                   14s 794MB
May 22 09:36:21 Starting compiler/backend/riscv
May 22 09:36:38 Finished compiler/backend/riscv                                  16s   1GB
May 22 09:36:38 Starting compiler/backend/ag32
May 22 09:37:44 Finished compiler/backend/ag32                                 1m05s   1GB
May 22 09:37:45 Starting compiler/parsing/proofs
May 22 09:43:15 Finished compiler/parsing/proofs                               5m29s 818MB
May 22 09:43:15 Starting compiler/inference/proofs
May 22 09:45:52 Finished compiler/inference/proofs                             2m36s   1GB
May 22 09:45:52 Starting compiler/backend/semantics
May 22 09:52:43 Finished compiler/backend/semantics                            6m50s   2GB
May 22 09:52:43 Starting compiler/backend/reg_alloc/proofs
May 22 09:55:59 Finished compiler/backend/reg_alloc/proofs                     3m15s 763MB
May 22 09:56:00 Starting compiler/backend/proofs
May 22 10:33:08 Finished compiler/backend/proofs                              37m07s   4GB
May 22 10:33:08 Starting compiler/encoders/x64/proofs
May 22 10:42:10 Finished compiler/encoders/x64/proofs                          9m01s   5GB
May 22 10:42:10 Starting compiler/encoders/arm6/proofs
May 22 10:54:21 Finished compiler/encoders/arm6/proofs                        12m10s   3GB
May 22 10:54:21 Starting compiler/encoders/arm8/proofs
May 22 11:00:46 Finished compiler/encoders/arm8/proofs                         6m24s   1GB
May 22 11:00:46 Starting compiler/encoders/mips/proofs
May 22 11:10:03 Finished compiler/encoders/mips/proofs                         9m17s   2GB
May 22 11:10:04 Starting compiler/encoders/riscv/proofs
May 22 11:18:20 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
May 22 11:18:20 Starting compiler/encoders/ag32/proofs
May 22 11:20:47 Finished compiler/encoders/ag32/proofs                         2m26s 686MB
May 22 11:20:47 Starting compiler/backend/x64/proofs
May 22 11:21:04 Finished compiler/backend/x64/proofs                             15s   1GB
May 22 11:21:04 Starting compiler/backend/arm6/proofs
May 22 11:21:22 Finished compiler/backend/arm6/proofs                            17s 832MB
May 22 11:21:22 Starting compiler/backend/arm8/proofs
May 22 11:21:38 Finished compiler/backend/arm8/proofs                            15s   1GB
May 22 11:21:38 Starting compiler/backend/mips/proofs
May 22 11:21:55 Finished compiler/backend/mips/proofs                            16s 945MB
May 22 11:21:55 Starting compiler/backend/riscv/proofs
May 22 11:22:11 Finished compiler/backend/riscv/proofs                           15s 955MB
May 22 11:22:11 Starting compiler/backend/ag32/proofs
May 22 11:31:08 Finished compiler/backend/ag32/proofs                          8m56s   1GB
May 22 11:31:09 Starting compiler/proofs
May 22 11:32:35 Finished compiler/proofs                                       1m25s   3GB
May 22 11:32:35 Starting candle/set-theory
May 22 11:33:00 Finished candle/set-theory                                       24s 673MB
May 22 11:33:00 Starting candle/syntax-lib
May 22 11:33:10 Finished candle/syntax-lib                                        9s 626MB
May 22 11:33:11 Starting candle/standard/syntax
May 22 11:34:50 Finished candle/standard/syntax                                1m39s   1GB
May 22 11:34:50 Starting candle/standard/semantics
May 22 11:36:23 Finished candle/standard/semantics                             1m32s   1GB
May 22 11:36:23 Starting candle/standard/monadic
May 22 11:37:56 Finished candle/standard/monadic                               1m31s 978MB
May 22 11:37:56 Starting candle/standard/ml_kernel
May 22 11:41:40 Finished candle/standard/ml_kernel                             3m44s   3GB
May 22 11:41:41 Starting candle/standard/opentheory
May 22 11:50:01 Finished candle/standard/opentheory                            8m20s   3GB
May 22 11:50:02 Starting candle/standard/opentheory/compilation
May 22 12:19:28 Finished candle/standard/opentheory/compilation               29m26s  14GB
May 22 12:19:28 Starting candle/standard/opentheory/compilation/proofs
May 22 12:20:13 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
May 22 12:20:13 Starting characteristic/examples
May 22 12:21:37 Finished characteristic/examples                               1m23s   2GB
May 22 12:21:37 Starting tutorial/solutions
May 22 12:34:33 Finished tutorial/solutions                                   12m54s   6GB
May 22 12:34:33 Starting translator/monadic/examples
May 22 12:37:22 Finished translator/monadic/examples                           2m48s   2GB
May 22 12:37:22 Starting examples
May 22 12:46:01 Finished examples                                              8m38s   2GB
May 22 12:46:01 Starting examples/compilation/x64
May 22 14:46:17 Finished examples/compilation/x64                           2h00m14s  12GB
May 22 14:46:18 Starting examples/compilation/x64/proofs
May 22 14:47:43 Finished examples/compilation/x64/proofs                       1m25s   2GB
May 22 14:47:44 Starting examples/compilation/ag32
May 22 15:15:23 Finished examples/compilation/ag32                            27m39s   6GB
May 22 15:15:24 Starting examples/compilation/ag32/proofs
May 22 15:16:09 Finished examples/compilation/ag32/proofs                        45s   3GB
May 22 15:16:09 Starting translator/okasaki-examples
May 22 15:20:11 Finished translator/okasaki-examples                           4m00s   1GB
May 22 15:20:11 Starting translator/other-examples
May 22 15:23:26 Finished translator/other-examples                             3m14s   1GB
May 22 15:23:26 Starting compiler/parsing/tests
May 22 15:23:50 Finished compiler/parsing/tests                                  23s 591MB
May 22 15:23:51 Starting compiler/inference/tests
May 22 15:27:51 Finished compiler/inference/tests                              4m00s   4GB
May 22 15:27:51 Starting compiler/bootstrap/translation
May 22 17:53:30 Finished compiler/bootstrap/translation                     2h25m37s  43GB
May 22 17:53:30 Starting unverified/sexpr-bootstrap/x64/64
May 22 18:00:48 Finished unverified/sexpr-bootstrap/x64/64                     7m16s   2GB
May 22 18:00:48 Starting unverified/sexpr-bootstrap/x64/32
May 22 18:05:21 Finished unverified/sexpr-bootstrap/x64/32                     4m32s   6GB
May 22 18:05:21 Starting compiler/benchmarks
May 22 18:43:02 Finished compiler/benchmarks                                  37m39s   1GB
May 22 18:43:02 Starting compiler/bootstrap/compilation/x64/64
May 23 05:56:58 Finished compiler/bootstrap/compilation/x64/64             11h13m55s  64GB
May 23 05:56:59 Starting compiler/bootstrap/compilation/x64/64/proofs
May 23 05:59:34 Finished compiler/bootstrap/compilation/x64/64/proofs          2m35s  10GB
May 23 05:59:34 Starting compiler/bootstrap/compilation/x64/32
May 23 15:03:37 Finished compiler/bootstrap/compilation/x64/32              9h04m01s  64GB
May 23 15:03:38 Starting compiler/bootstrap/compilation/x64/32/proofs
May 23 15:06:33 Finished compiler/bootstrap/compilation/x64/32/proofs          2m54s   5GB
May 23 15:06:33 Starting compiler/bootstrap/compilation/ag32/32
May 24 00:42:32 Finished compiler/bootstrap/compilation/ag32/32             9h35m58s  64GB
May 24 00:42:33 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 24 01:15:14 Finished compiler/bootstrap/compilation/ag32/32/proofs        32m41s  14GB
May 24 01:15:14 SUCCESS