Job 572

CakeML:56d88d6c69fd12f518ad93ec119f44c893ec542d
  Add spt_fold to compute lib [Nov 21 09:02:25]
#553 (flat-elim-cleanup)
Merging into:9b491cb24bd22174a6c514574e4bb6c057eafe2f
  Rename "backend_correct" to "encoder_correct" [Nov 20 18:08:31]
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming [Nov 20 05:59:15]
Machine:demi

Nov 21 15:19:19 Claimed job
Nov 21 15:19:24 Reusing HOL
Nov 21 15:20:16 Starting developers/bin
Nov 21 15:20:23 Finished developers/bin                                           6s 935MB
Nov 21 15:20:23 Starting semantics/ffi
Nov 21 15:20:42 Finished semantics/ffi                                           17s 305MB
Nov 21 15:20:42 Starting semantics
Nov 21 15:22:28 Finished semantics                                             1m44s   1GB
Nov 21 15:22:28 Starting semantics/proofs
Nov 21 15:26:41 Finished semantics/proofs                                      4m12s   1GB
Nov 21 15:26:41 Starting basis/pure
Nov 21 15:28:01 Finished basis/pure                                            1m19s 691MB
Nov 21 15:28:02 Starting translator
Nov 21 15:32:34 Finished translator                                            4m31s   1GB
Nov 21 15:32:34 Starting compiler/parsing
Nov 21 15:34:29 Finished compiler/parsing                                      1m54s   2GB
Nov 21 15:34:29 Starting characteristic
Nov 21 15:38:14 Finished characteristic                                        3m44s   1GB
Nov 21 15:38:15 Starting translator/monadic
Nov 21 15:40:20 Finished translator/monadic                                    2m05s   1GB
Nov 21 15:40:21 Starting basis
Nov 21 16:03:30 Finished basis                                                23m08s   2GB
Nov 21 16:03:30 Starting compiler/inference
Nov 21 16:05:30 Finished compiler/inference                                    1m58s   1GB
Nov 21 16:05:30 Starting compiler/backend/reg_alloc
Nov 21 16:06:37 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 21 16:06:38 Starting compiler/backend/gc
Nov 21 16:15:25 Finished compiler/backend/gc                                   8m46s   1GB
Nov 21 16:15:25 Starting compiler/backend
Nov 21 16:15:29 Finished compiler/backend                                         3s  34MB
Nov 21 16:15:30 Starting compiler/encoders/asm
Nov 21 16:15:31 Finished compiler/encoders/asm                                    1s  31MB
Nov 21 16:15:32 Starting compiler/encoders/x64
Nov 21 16:15:56 Finished compiler/encoders/x64                                   23s 427MB
Nov 21 16:15:57 Starting compiler/encoders/arm6
Nov 21 16:17:03 Finished compiler/encoders/arm6                                1m05s 442MB
Nov 21 16:17:03 Starting compiler/encoders/arm8
Nov 21 16:17:14 Finished compiler/encoders/arm8                                  10s 349MB
Nov 21 16:17:15 Starting compiler/encoders/mips
Nov 21 16:17:28 Finished compiler/encoders/mips                                  13s 523MB
Nov 21 16:17:29 Starting compiler/encoders/riscv
Nov 21 16:17:41 Finished compiler/encoders/riscv                                 11s 463MB
Nov 21 16:17:41 Starting compiler/backend/x64
Nov 21 16:18:06 Finished compiler/backend/x64                                    24s   1GB
Nov 21 16:18:06 Starting compiler/backend/arm6
Nov 21 16:18:33 Finished compiler/backend/arm6                                   25s   1GB
Nov 21 16:18:33 Starting compiler/backend/arm8
Nov 21 16:19:00 Finished compiler/backend/arm8                                   25s   1GB
Nov 21 16:19:00 Starting compiler/backend/mips
Nov 21 16:19:29 Finished compiler/backend/mips                                   28s   1GB
Nov 21 16:19:29 Starting compiler/backend/riscv
Nov 21 16:19:58 Finished compiler/backend/riscv                                  27s   1GB
Nov 21 16:19:58 Starting compiler/parsing/proofs
Nov 21 16:29:22 Finished compiler/parsing/proofs                               9m23s 842MB
Nov 21 16:29:22 Starting compiler/inference/proofs
Nov 21 16:33:22 Finished compiler/inference/proofs                             3m58s   2GB
Nov 21 16:33:22 Starting compiler/backend/semantics
Nov 21 16:45:19 Finished compiler/backend/semantics                           11m56s   2GB
Nov 21 16:45:19 Starting compiler/backend/reg_alloc/proofs
Nov 21 16:49:05 Finished compiler/backend/reg_alloc/proofs                     3m44s 511MB
Nov 21 16:49:05 Starting compiler/backend/proofs
Nov 21 17:46:55 Finished compiler/backend/proofs                              57m49s   4GB
Nov 21 17:46:55 Starting compiler/encoders/x64/proofs
Nov 21 17:55:53 Finished compiler/encoders/x64/proofs                          8m57s   1GB
Nov 21 17:55:53 Starting compiler/encoders/arm6/proofs
Nov 21 18:04:33 Finished compiler/encoders/arm6/proofs                         8m39s   1GB
Nov 21 18:04:34 Starting compiler/encoders/arm8/proofs
Nov 21 18:11:42 Finished compiler/encoders/arm8/proofs                         7m07s   1GB
Nov 21 18:11:43 Starting compiler/encoders/mips/proofs
Nov 21 18:20:46 Finished compiler/encoders/mips/proofs                         9m02s   1GB
Nov 21 18:20:47 Starting compiler/encoders/riscv/proofs
Nov 21 18:31:14 Finished compiler/encoders/riscv/proofs                       10m27s   1GB
Nov 21 18:31:15 Starting compiler/backend/x64/proofs
Nov 21 18:31:44 Finished compiler/backend/x64/proofs                             28s   1GB
Nov 21 18:31:45 Starting compiler/backend/arm6/proofs
Nov 21 18:32:17 Finished compiler/backend/arm6/proofs                            31s 889MB
Nov 21 18:32:17 Starting compiler/backend/arm8/proofs
Nov 21 18:32:45 Finished compiler/backend/arm8/proofs                            27s   1GB
Nov 21 18:32:46 Starting compiler/backend/mips/proofs
Nov 21 18:33:16 Finished compiler/backend/mips/proofs                            29s   1GB
Nov 21 18:33:17 Starting compiler/backend/riscv/proofs
Nov 21 18:33:47 Finished compiler/backend/riscv/proofs                           29s   1GB
Nov 21 18:33:47 Starting compiler/proofs
Nov 21 18:35:39 Finished compiler/proofs                                       1m51s   2GB
Nov 21 18:35:39 Starting candle/set-theory
Nov 21 18:36:15 Finished candle/set-theory                                       35s 698MB
Nov 21 18:36:15 Starting candle/syntax-lib
Nov 21 18:36:30 Finished candle/syntax-lib                                       14s 608MB
Nov 21 18:36:30 Starting candle/standard/syntax
Nov 21 18:38:38 Finished candle/standard/syntax                                2m07s 703MB
Nov 21 18:38:39 Starting candle/standard/semantics
Nov 21 18:40:32 Finished candle/standard/semantics                             1m52s 961MB
Nov 21 18:40:32 Starting candle/standard/monadic
Nov 21 18:42:41 Finished candle/standard/monadic                               2m08s 973MB
Nov 21 18:42:42 Starting candle/standard/ml_kernel
Nov 21 19:03:09 Finished candle/standard/ml_kernel                            20m26s   3GB
Nov 21 19:03:09 Starting candle/standard/opentheory
Nov 21 19:13:09 Finished candle/standard/opentheory                            9m59s   3GB
Nov 21 19:13:10 Starting candle/standard/opentheory/compilation
Nov 21 19:53:29 Finished candle/standard/opentheory/compilation               40m18s  16GB
Nov 21 19:53:30 Starting candle/standard/opentheory/compilation/proofs
Nov 21 19:54:20 Finished candle/standard/opentheory/compilation/proofs           49s   4GB
Nov 21 19:54:21 Starting characteristic/examples
Nov 21 19:56:21 Finished characteristic/examples                               1m59s   2GB
Nov 21 19:56:22 Starting tutorial/solutions
Nov 21 20:14:04 Finished tutorial/solutions                                   17m42s   5GB
Nov 21 20:14:05 Starting translator/monadic/examples
Nov 21 20:16:37 Finished translator/monadic/examples                           2m31s   2GB
Nov 21 20:16:38 Starting examples
Nov 21 20:24:02 Finished examples                                              7m23s   2GB
Nov 21 20:24:03 Starting examples/compilation
Nov 21 22:55:03 Finished examples/compilation                               2h31m00s   9GB
Nov 21 22:55:04 Starting examples/compilation/proofs
Nov 21 22:57:52 Finished examples/compilation/proofs                           2m47s   3GB
Nov 21 22:57:53 Starting compiler/benchmarks
Nov 21 22:57:54 Finished compiler/benchmarks                                      0s   7MB
Nov 21 22:57:54 Starting translator/okasaki-examples
Nov 21 23:02:34 Finished translator/okasaki-examples                           4m38s   1GB
Nov 21 23:02:34 Starting translator/other-examples
Nov 21 23:07:24 Finished translator/other-examples                             4m49s 839MB
Nov 21 23:07:24 Starting compiler/parsing/tests
Nov 21 23:07:59 Finished compiler/parsing/tests                                  34s 391MB
Nov 21 23:08:00 Starting compiler/inference/tests
Nov 21 23:13:12 Finished compiler/inference/tests                              5m11s   3GB
Nov 21 23:13:12 Starting compiler/bootstrap/translation
Nov 22 03:29:01 Finished compiler/bootstrap/translation                     4h15m47s  49GB
Nov 22 03:29:01 Starting unverified/sexpr-bootstrap/x64/64
Nov 22 03:39:18 Finished unverified/sexpr-bootstrap/x64/64                    10m15s  14GB
Nov 22 03:39:18 Starting unverified/sexpr-bootstrap/x64/32
Nov 22 03:46:05 Finished unverified/sexpr-bootstrap/x64/32                     6m46s  18GB
Nov 22 03:46:05 Starting compiler/bootstrap/compilation/x64/64
Nov 22 19:08:03 Finished compiler/bootstrap/compilation/x64/64             15h21m56s  61GB
Nov 22 19:08:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 22 19:13:04 Finished compiler/bootstrap/compilation/x64/64/proofs          5m00s  24GB
Nov 22 19:13:05 Starting compiler/bootstrap/compilation/x64/32
Nov 23 05:14:11 Finished compiler/bootstrap/compilation/x64/32             10h01m05s  56GB
Nov 23 05:14:11 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 23 05:17:02 Finished compiler/bootstrap/compilation/x64/32/proofs          2m50s  30GB
Nov 23 05:17:03 SUCCESS