Job 557

CakeML:3fa28c85c940b4edbbe79025687e39763ee2de56
  Fix data_to_word_bignumProof for revision to simp's caching of ARITH [Nov 08 10:34:25]
HOL:de063b7a0efc78ddd089b664f3aa0ce110f45620
  Make more type-abbrevs printing ones to keep word-emit working [Nov 14 09:30:10]
Machine:oven1 4.15.9-300.fc27.x86_64 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 14 13:34:36 Claimed job
Nov 14 13:35:27 Building HOL
Nov 14 13:45:05 Starting developers/bin
Nov 14 13:46:15 Finished developers/bin                                        1m09s 916MB
Nov 14 13:46:16 Starting semantics/ffi
Nov 14 13:46:58 Finished semantics/ffi                                           41s 362MB
Nov 14 13:46:59 Starting semantics
Nov 14 13:48:43 Finished semantics                                             1m43s 964MB
Nov 14 13:48:44 Starting semantics/proofs
Nov 14 13:51:40 Finished semantics/proofs                                      2m55s   1GB
Nov 14 13:51:41 Starting basis/pure
Nov 14 13:55:27 Finished basis/pure                                            3m45s 655MB
Nov 14 13:55:28 Starting translator
Nov 14 13:58:57 Finished translator                                            3m28s 950MB
Nov 14 13:58:58 Starting compiler/parsing
Nov 14 14:00:22 Finished compiler/parsing                                      1m22s   1GB
Nov 14 14:00:22 Starting characteristic
Nov 14 14:02:58 Finished characteristic                                        2m35s   1GB
Nov 14 14:02:59 Starting translator/monadic
Nov 14 14:04:37 Finished translator/monadic                                    1m37s   1GB
Nov 14 14:04:37 Starting basis
Nov 14 14:22:45 Finished basis                                                18m06s   3GB
Nov 14 14:22:46 Starting compiler/inference
Nov 14 14:24:30 Finished compiler/inference                                    1m43s   1GB
Nov 14 14:24:31 Starting compiler/backend/reg_alloc
Nov 14 14:25:20 Finished compiler/backend/reg_alloc                              49s   1GB
Nov 14 14:25:21 Starting compiler/backend/gc
Nov 14 14:33:57 Finished compiler/backend/gc                                   8m34s   1GB
Nov 14 14:33:57 Starting compiler/backend
Nov 14 14:34:00 Finished compiler/backend                                         2s  18MB
Nov 14 14:34:01 Starting compiler/encoders/asm
Nov 14 14:34:03 Finished compiler/encoders/asm                                    1s  14MB
Nov 14 14:34:03 Starting compiler/encoders/x64
Nov 14 14:34:57 Finished compiler/encoders/x64                                   53s 594MB
Nov 14 14:34:58 Starting compiler/encoders/arm6
Nov 14 14:36:44 Finished compiler/encoders/arm6                                1m45s   1GB
Nov 14 14:36:45 Starting compiler/encoders/arm8
Nov 14 14:37:12 Finished compiler/encoders/arm8                                  26s 489MB
Nov 14 14:37:13 Starting compiler/encoders/mips
Nov 14 14:38:14 Finished compiler/encoders/mips                                  59s 900MB
Nov 14 14:38:14 Starting compiler/encoders/riscv
Nov 14 14:39:19 Finished compiler/encoders/riscv                               1m04s 704MB
Nov 14 14:39:19 Starting compiler/backend/x64
Nov 14 14:39:39 Finished compiler/backend/x64                                    19s   1GB
Nov 14 14:39:40 Starting compiler/backend/arm6
Nov 14 14:40:00 Finished compiler/backend/arm6                                   18s   1GB
Nov 14 14:40:00 Starting compiler/backend/arm8
Nov 14 14:40:18 Finished compiler/backend/arm8                                   17s   1GB
Nov 14 14:40:19 Starting compiler/backend/mips
Nov 14 14:40:38 Finished compiler/backend/mips                                   18s   1GB
Nov 14 14:40:39 Starting compiler/backend/riscv
Nov 14 14:40:57 Finished compiler/backend/riscv                                  18s   1GB
Nov 14 14:40:58 Starting compiler/parsing/proofs
Nov 14 14:47:13 Finished compiler/parsing/proofs                               6m14s   1GB
Nov 14 14:47:14 Starting compiler/inference/proofs
Nov 14 14:50:43 Finished compiler/inference/proofs                             3m28s   1GB
Nov 14 14:50:44 Starting compiler/backend/semantics
Nov 14 15:01:14 Finished compiler/backend/semantics                           10m29s   3GB
Nov 14 15:01:14 Starting compiler/backend/reg_alloc/proofs
Nov 14 15:04:26 Finished compiler/backend/reg_alloc/proofs                     3m10s 554MB
Nov 14 15:04:26 Starting compiler/backend/proofs
Nov 14 16:07:45 Finished compiler/backend/proofs                            1h03m18s   3GB
Nov 14 16:07:46 Starting compiler/encoders/x64/proofs
Nov 14 16:15:40 Finished compiler/encoders/x64/proofs                          7m53s   4GB
Nov 14 16:15:41 Starting compiler/encoders/arm6/proofs
Nov 14 16:23:32 Finished compiler/encoders/arm6/proofs                         7m50s   2GB
Nov 14 16:23:33 Starting compiler/encoders/arm8/proofs
Nov 14 16:29:08 Finished compiler/encoders/arm8/proofs                         5m34s 997MB
Nov 14 16:29:08 Starting compiler/encoders/mips/proofs
Nov 14 16:36:44 Finished compiler/encoders/mips/proofs                         7m34s   1GB
Nov 14 16:36:45 Starting compiler/encoders/riscv/proofs
Nov 14 16:44:58 Finished compiler/encoders/riscv/proofs                        8m12s   1GB
Nov 14 16:44:59 Starting compiler/backend/x64/proofs
Nov 14 16:45:20 Finished compiler/backend/x64/proofs                             20s 873MB
Nov 14 16:45:21 Starting compiler/backend/arm6/proofs
Nov 14 16:45:44 Finished compiler/backend/arm6/proofs                            22s   1GB
Nov 14 16:45:45 Starting compiler/backend/arm8/proofs
Nov 14 16:46:06 Finished compiler/backend/arm8/proofs                            20s   1GB
Nov 14 16:46:07 Starting compiler/backend/mips/proofs
Nov 14 16:46:30 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 14 16:46:31 Starting compiler/backend/riscv/proofs
Nov 14 16:46:53 Finished compiler/backend/riscv/proofs                           21s   1GB
Nov 14 16:46:54 Starting compiler/proofs
Nov 14 16:48:17 Finished compiler/proofs                                       1m22s   2GB
Nov 14 16:48:18 Starting candle/set-theory
Nov 14 16:48:51 Finished candle/set-theory                                       32s 617MB
Nov 14 16:48:52 Starting candle/syntax-lib
Nov 14 16:49:03 Finished candle/syntax-lib                                       10s 516MB
Nov 14 16:49:04 Starting candle/standard/syntax
Nov 14 16:50:41 Finished candle/standard/syntax                                1m36s 578MB
Nov 14 16:50:42 Starting candle/standard/semantics
Nov 14 16:52:06 Finished candle/standard/semantics                             1m23s 997MB
Nov 14 16:52:07 Starting candle/standard/monadic
Nov 14 16:53:43 Finished candle/standard/monadic                               1m35s   1GB
Nov 14 16:53:44 Starting candle/standard/ml_kernel
Nov 14 17:10:20 Finished candle/standard/ml_kernel                            16m35s   4GB
Nov 14 17:10:20 Starting candle/standard/opentheory
Nov 14 17:19:57 Finished candle/standard/opentheory                            9m36s   6GB
Nov 14 17:19:58 Starting candle/standard/opentheory/compilation
Nov 14 18:10:14 Finished candle/standard/opentheory/compilation               50m15s  16GB
Nov 14 18:10:15 Starting candle/standard/opentheory/compilation/proofs
Nov 14 18:10:54 Finished candle/standard/opentheory/compilation/proofs           38s   5GB
Nov 14 18:10:54 Starting characteristic/examples
Nov 14 18:12:42 Finished characteristic/examples                               1m47s   1GB
Nov 14 18:12:43 Starting tutorial/solutions
Nov 14 18:28:33 Finished tutorial/solutions                                   15m49s   6GB
Nov 14 18:28:34 Starting translator/monadic/examples
Nov 14 18:31:40 Finished translator/monadic/examples                           3m05s   2GB
Nov 14 18:31:40 Starting examples
Nov 14 18:38:47 Finished examples                                              7m06s   3GB
Nov 14 18:38:48 Starting examples/compilation
Nov 14 20:42:52 Finished examples/compilation                               2h04m03s  11GB
Nov 14 20:42:53 Starting examples/compilation/proofs
Nov 14 20:44:57 Finished examples/compilation/proofs                           2m03s   3GB
Nov 14 20:44:58 Starting compiler/benchmarks
Nov 14 20:44:59 Finished compiler/benchmarks                                      0s   4MB
Nov 14 20:45:00 Starting translator/okasaki-examples
Nov 14 20:48:45 Finished translator/okasaki-examples                           3m44s   1GB
Nov 14 20:48:46 Starting translator/other-examples
Nov 14 20:52:27 Finished translator/other-examples                             3m40s 988MB
Nov 14 20:52:28 Starting compiler/parsing/tests
Nov 14 20:52:54 Finished compiler/parsing/tests                                  25s 320MB
Nov 14 20:52:54 Starting compiler/inference/tests
Nov 14 20:57:09 Finished compiler/inference/tests                              4m14s   3GB
Nov 14 20:57:10 Starting compiler/bootstrap/translation
Nov 15 05:24:18 Finished compiler/bootstrap/translation                     8h27m07s  44GB
Nov 15 05:24:19 Starting unverified/sexpr-bootstrap/x64/64
Nov 15 05:36:11 Finished unverified/sexpr-bootstrap/x64/64                    11m50s  13GB
Nov 15 05:36:12 Starting unverified/sexpr-bootstrap/x64/32
Nov 15 05:42:17 Finished unverified/sexpr-bootstrap/x64/32                     6m03s  16GB
Nov 15 05:42:18 Starting compiler/bootstrap/compilation/x64/64
Nov 17 20:26:19 Finished compiler/bootstrap/compilation/x64/64             62h43m59s  64GB
Nov 17 20:26:20 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 17 20:30:10 Finished compiler/bootstrap/compilation/x64/64/proofs          3m49s  25GB
Nov 17 20:30:11 Starting compiler/bootstrap/compilation/x64/32
Nov 18 09:38:01 Finished compiler/bootstrap/compilation/x64/32             13h07m48s  55GB
Nov 18 09:38:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 18 09:41:17 Finished compiler/bootstrap/compilation/x64/32/proofs          3m14s  21GB
Nov 18 09:41:18 SUCCESS