Job 1108

CakeML:c472a5c9eeea5c1d67e039697cb3e0f1c4e10831
  Fix a proof and some terrible indentation [Nov 28 06:33:56]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:stove 4.15.0-55-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

Nov 28 06:34:14 Claimed job
Nov 28 06:34:16 Reusing HOL
Nov 28 06:35:01 Starting developers
Nov 28 06:35:05 Finished developers                                               3s 112MB
Nov 28 06:35:05 Starting developers/bin
Nov 28 06:35:11 Finished developers/bin                                           5s 964MB
Nov 28 06:35:11 Starting semantics/ffi
Nov 28 06:35:20 Finished semantics/ffi                                            9s 241MB
Nov 28 06:35:20 Starting semantics
Nov 28 06:36:34 Finished semantics                                             1m14s 905MB
Nov 28 06:36:34 Starting semantics/proofs
Nov 28 06:39:29 Finished semantics/proofs                                      2m54s   1GB
Nov 28 06:39:29 Starting semantics/alt_semantics
Nov 28 06:39:36 Finished semantics/alt_semantics                                  7s 301MB
Nov 28 06:39:36 Starting semantics/alt_semantics/proofs
Nov 28 06:41:20 Finished semantics/alt_semantics/proofs                        1m44s 813MB
Nov 28 06:41:20 Starting basis/pure
Nov 28 06:42:06 Finished basis/pure                                              45s 696MB
Nov 28 06:42:06 Starting translator
Nov 28 06:43:47 Finished translator                                            1m40s   1GB
Nov 28 06:43:47 Starting compiler/parsing
Nov 28 06:44:49 Finished compiler/parsing                                      1m01s   2GB
Nov 28 06:44:49 Starting characteristic
Nov 28 06:49:57 Finished characteristic                                        5m08s   1GB
Nov 28 06:49:57 Starting translator/monadic
Nov 28 06:51:22 Finished translator/monadic                                    1m24s   1GB
Nov 28 06:51:22 Starting basis
Nov 28 07:10:32 Finished basis                                                19m09s   2GB
Nov 28 07:10:32 Starting compiler/inference
Nov 28 07:12:13 Finished compiler/inference                                    1m41s   1GB
Nov 28 07:12:13 Starting compiler/backend/reg_alloc
Nov 28 07:13:10 Finished compiler/backend/reg_alloc                              56s   1GB
Nov 28 07:13:10 Starting compiler/backend/gc
Nov 28 07:16:09 Finished compiler/backend/gc                                   2m58s   1GB
Nov 28 07:16:09 Starting compiler/backend
Nov 28 07:19:40 Finished compiler/backend                                      3m30s   2GB
Nov 28 07:19:40 Starting compiler/encoders/asm
Nov 28 07:19:59 Finished compiler/encoders/asm                                   19s 891MB
Nov 28 07:19:59 Starting compiler/encoders/x64
Nov 28 07:20:50 Finished compiler/encoders/x64                                   51s 961MB
Nov 28 07:20:50 Starting compiler/encoders/arm7
Nov 28 07:22:24 Finished compiler/encoders/arm7                                1m33s   1GB
Nov 28 07:22:24 Starting compiler/encoders/arm8
Nov 28 07:22:54 Finished compiler/encoders/arm8                                  29s 704MB
Nov 28 07:22:54 Starting compiler/encoders/mips
Nov 28 07:23:57 Finished compiler/encoders/mips                                1m02s   1GB
Nov 28 07:23:57 Starting compiler/encoders/riscv
Nov 28 07:25:11 Finished compiler/encoders/riscv                               1m13s   1GB
Nov 28 07:25:11 Starting compiler/encoders/ag32
Nov 28 07:25:26 Finished compiler/encoders/ag32                                  15s 813MB
Nov 28 07:25:26 Starting compiler/backend/x64
Nov 28 07:25:43 Finished compiler/backend/x64                                    16s   1GB
Nov 28 07:25:43 Starting compiler/backend/arm7
Nov 28 07:26:01 Finished compiler/backend/arm7                                   17s   1GB
Nov 28 07:26:01 Starting compiler/backend/arm8
Nov 28 07:26:17 Finished compiler/backend/arm8                                   15s   1GB
Nov 28 07:26:17 Starting compiler/backend/mips
Nov 28 07:26:33 Finished compiler/backend/mips                                   16s   1GB
Nov 28 07:26:33 Starting compiler/backend/riscv
Nov 28 07:26:51 Finished compiler/backend/riscv                                  17s   1GB
Nov 28 07:26:51 Starting compiler/backend/ag32
Nov 28 07:27:53 Finished compiler/backend/ag32                                 1m01s   1GB
Nov 28 07:27:53 Starting compiler/parsing/proofs
Nov 28 07:33:25 Finished compiler/parsing/proofs                               5m31s 968MB
Nov 28 07:33:25 Starting compiler/inference/proofs
Nov 28 07:36:04 Finished compiler/inference/proofs                             2m39s   1GB
Nov 28 07:36:04 Starting compiler/backend/semantics
Nov 28 07:41:32 Finished compiler/backend/semantics                            5m27s   2GB
Nov 28 07:41:32 Starting compiler/backend/reg_alloc/proofs
Nov 28 07:44:39 Finished compiler/backend/reg_alloc/proofs                     3m06s 813MB
Nov 28 07:44:39 Starting compiler/backend/proofs
Nov 28 08:20:55 Finished compiler/backend/proofs                              36m15s   4GB
Nov 28 08:20:55 Starting compiler/encoders/x64/proofs
Nov 28 08:29:28 Finished compiler/encoders/x64/proofs                          8m33s   4GB
Nov 28 08:29:28 Starting compiler/encoders/arm7/proofs
Nov 28 08:41:10 Finished compiler/encoders/arm7/proofs                        11m41s   3GB
Nov 28 08:41:10 Starting compiler/encoders/arm8/proofs
Nov 28 08:47:02 Finished compiler/encoders/arm8/proofs                         5m51s   1GB
Nov 28 08:47:02 Starting compiler/encoders/mips/proofs
Nov 28 08:55:57 Finished compiler/encoders/mips/proofs                         8m55s   2GB
Nov 28 08:55:57 Starting compiler/encoders/riscv/proofs
Nov 28 09:03:51 Finished compiler/encoders/riscv/proofs                        7m52s   1GB
Nov 28 09:03:51 Starting compiler/encoders/ag32/proofs
Nov 28 09:06:08 Finished compiler/encoders/ag32/proofs                         2m17s 852MB
Nov 28 09:06:08 Starting compiler/backend/x64/proofs
Nov 28 09:06:25 Finished compiler/backend/x64/proofs                             16s 853MB
Nov 28 09:06:25 Starting compiler/backend/arm7/proofs
Nov 28 09:06:42 Finished compiler/backend/arm7/proofs                            16s   1GB
Nov 28 09:06:42 Starting compiler/backend/arm8/proofs
Nov 28 09:06:59 Finished compiler/backend/arm8/proofs                            17s 761MB
Nov 28 09:06:59 Starting compiler/backend/mips/proofs
Nov 28 09:07:16 Finished compiler/backend/mips/proofs                            16s   1GB
Nov 28 09:07:16 Starting compiler/backend/riscv/proofs
Nov 28 09:07:34 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 28 09:07:34 Starting compiler/backend/ag32/proofs
Nov 28 09:15:59 Finished compiler/backend/ag32/proofs                          8m24s   2GB
Nov 28 09:15:59 Starting compiler/proofs
Nov 28 09:17:34 Finished compiler/proofs                                       1m35s   2GB
Nov 28 09:17:34 Starting candle/set-theory
Nov 28 09:18:00 Finished candle/set-theory                                       25s 825MB
Nov 28 09:18:00 Starting candle/syntax-lib
Nov 28 09:18:10 Finished candle/syntax-lib                                        9s 671MB
Nov 28 09:18:10 Starting candle/standard/syntax
Nov 28 09:19:48 Finished candle/standard/syntax                                1m37s 925MB
Nov 28 09:19:48 Starting candle/standard/semantics
Nov 28 09:21:20 Finished candle/standard/semantics                             1m32s   1GB
Nov 28 09:21:20 Starting candle/standard/monadic
Nov 28 09:22:47 Finished candle/standard/monadic                               1m26s   1GB
Nov 28 09:22:47 Starting candle/standard/ml_kernel
Nov 28 09:26:36 Finished candle/standard/ml_kernel                             3m49s   3GB
Nov 28 09:26:36 Starting candle/standard/opentheory
Nov 28 09:35:05 Finished candle/standard/opentheory                            8m28s   4GB
Nov 28 09:35:05 Starting candle/standard/opentheory/compilation
Nov 28 10:02:57 Finished candle/standard/opentheory/compilation               27m51s  22GB
Nov 28 10:02:57 Starting candle/standard/opentheory/compilation/proofs
Nov 28 10:03:38 Finished candle/standard/opentheory/compilation/proofs           40s   2GB
Nov 28 10:03:38 Starting characteristic/examples
Nov 28 10:05:00 Finished characteristic/examples                               1m22s   1GB
Nov 28 10:05:00 Starting tutorial/solutions
Nov 28 10:17:11 Finished tutorial/solutions                                   12m10s   6GB
Nov 28 10:17:11 Starting translator/monadic/examples
Nov 28 10:19:52 Finished translator/monadic/examples                           2m41s   2GB
Nov 28 10:19:52 Starting examples
Nov 28 10:27:53 Finished examples                                              8m01s   4GB
Nov 28 10:27:54 Starting examples/compilation/x64
Nov 28 12:23:59 Finished examples/compilation/x64                           1h56m05s  12GB
Nov 28 12:23:59 Starting examples/compilation/x64/proofs
Nov 28 12:25:52 Finished examples/compilation/x64/proofs                       1m52s   2GB
Nov 28 12:25:52 Starting examples/compilation/ag32
Nov 28 12:52:53 Finished examples/compilation/ag32                            27m00s   5GB
Nov 28 12:52:53 Starting examples/compilation/ag32/proofs
Nov 28 12:53:38 Finished examples/compilation/ag32/proofs                        45s   2GB
Nov 28 12:53:38 Starting translator/okasaki-examples
Nov 28 12:57:27 Finished translator/okasaki-examples                           3m48s   1GB
Nov 28 12:57:27 Starting translator/other-examples
Nov 28 12:59:06 Finished translator/other-examples                             1m38s   1GB
Nov 28 12:59:06 Starting compiler/parsing/tests
Nov 28 12:59:29 Finished compiler/parsing/tests                                  22s 561MB
Nov 28 12:59:29 Starting compiler/inference/tests
Nov 28 13:03:33 Finished compiler/inference/tests                              4m03s   4GB
Nov 28 13:03:33 Starting compiler/bootstrap/translation
Nov 28 15:25:56 Finished compiler/bootstrap/translation                     2h22m22s  46GB
Nov 28 15:25:56 Starting unverified/sexpr-bootstrap/x64/64
Nov 28 15:38:15 Finished unverified/sexpr-bootstrap/x64/64                    12m18s   3GB
Nov 28 15:38:15 Starting unverified/sexpr-bootstrap/x64/32
Nov 28 15:47:14 Finished unverified/sexpr-bootstrap/x64/32                     8m58s   6GB
Nov 28 15:47:14 Starting compiler/benchmarks
Nov 28 15:47:16 Finished compiler/benchmarks                                      1s  35MB
Nov 28 15:47:16 Starting compiler/bootstrap/compilation/x64/64
Nov 29 03:04:11 Finished compiler/bootstrap/compilation/x64/64             11h16m54s  64GB
Nov 29 03:04:11 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 29 03:07:56 Finished compiler/bootstrap/compilation/x64/64/proofs          3m44s   5GB
Nov 29 03:07:56 Starting compiler/bootstrap/compilation/x64/32
Nov 29 13:34:57 Finished compiler/bootstrap/compilation/x64/32             10h27m01s  64GB
Nov 29 13:34:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 29 13:37:52 Finished compiler/bootstrap/compilation/x64/32/proofs          2m54s   5GB
Nov 29 13:37:52 Starting compiler/bootstrap/compilation/ag32/32 Nov 29 13:37:52 2424s