Job 622

CakeML:fc7210e6e390f10177982607373a07ef1e4b5808
  Update for new s-expression syntax (using  [Dec 09 05:04:39]
HOL:5e4369a4a208507b43df4343e08b5fca51872a25
  Slightly extend documentation of fn-update syntax with more example [Dec 08 10:49:26]
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

Dec 09 11:24:55 Claimed job
Dec 09 11:24:58 Reusing HOL
Dec 09 11:25:53 Starting developers
Dec 09 11:25:56 Finished developers                                               2s  21MB
Dec 09 11:25:56 Starting developers/bin
Dec 09 11:27:08 Finished developers/bin                                        1m11s 916MB
Dec 09 11:27:09 Starting semantics/ffi
Dec 09 11:27:20 Finished semantics/ffi                                           10s 227MB
Dec 09 11:27:21 Starting semantics
Dec 09 11:28:42 Finished semantics                                             1m20s 958MB
Dec 09 11:28:43 Starting semantics/proofs
Dec 09 11:31:45 Finished semantics/proofs                                      3m01s   1GB
Dec 09 11:31:45 Starting basis/pure
Dec 09 11:32:39 Finished basis/pure                                              53s 669MB
Dec 09 11:32:40 Starting translator
Dec 09 11:33:57 Finished translator                                            1m16s 980MB
Dec 09 11:33:58 Starting compiler/parsing
Dec 09 11:35:14 Finished compiler/parsing                                      1m15s   1GB
Dec 09 11:35:14 Starting characteristic
Dec 09 11:37:54 Finished characteristic                                        2m38s   1GB
Dec 09 11:37:54 Starting translator/monadic
Dec 09 11:39:24 Finished translator/monadic                                    1m29s   1GB
Dec 09 11:39:25 Starting basis
Dec 09 11:55:47 Finished basis                                                16m21s   2GB
Dec 09 11:55:47 Starting compiler/inference
Dec 09 11:57:32 Finished compiler/inference                                    1m43s   1GB
Dec 09 11:57:33 Starting compiler/backend/reg_alloc
Dec 09 11:58:24 Finished compiler/backend/reg_alloc                              51s   1GB
Dec 09 11:58:25 Starting compiler/backend/gc
Dec 09 12:04:56 Finished compiler/backend/gc                                   6m30s   2GB
Dec 09 12:04:57 Starting compiler/backend
Dec 09 12:05:00 Finished compiler/backend                                         2s  20MB
Dec 09 12:05:00 Starting compiler/encoders/asm
Dec 09 12:05:02 Finished compiler/encoders/asm                                    1s  13MB
Dec 09 12:05:03 Starting compiler/encoders/x64
Dec 09 12:05:55 Finished compiler/encoders/x64                                   50s 611MB
Dec 09 12:05:55 Starting compiler/encoders/arm6
Dec 09 12:07:38 Finished compiler/encoders/arm6                                1m41s   1GB
Dec 09 12:07:38 Starting compiler/encoders/arm8
Dec 09 12:08:06 Finished compiler/encoders/arm8                                  27s 493MB
Dec 09 12:08:07 Starting compiler/encoders/mips
Dec 09 12:09:06 Finished compiler/encoders/mips                                  57s 976MB
Dec 09 12:09:06 Starting compiler/encoders/riscv
Dec 09 12:10:08 Finished compiler/encoders/riscv                               1m01s 666MB
Dec 09 12:10:09 Starting compiler/encoders/ag32
Dec 09 12:10:27 Finished compiler/encoders/ag32                                  17s 526MB
Dec 09 12:10:28 Starting compiler/backend/x64
Dec 09 12:10:46 Finished compiler/backend/x64                                    17s 828MB
Dec 09 12:10:46 Starting compiler/backend/arm6
Dec 09 12:11:06 Finished compiler/backend/arm6                                   19s   1GB
Dec 09 12:11:07 Starting compiler/backend/arm8
Dec 09 12:11:25 Finished compiler/backend/arm8                                   17s 937MB
Dec 09 12:11:26 Starting compiler/backend/mips
Dec 09 12:11:46 Finished compiler/backend/mips                                   18s   1GB
Dec 09 12:11:46 Starting compiler/backend/riscv
Dec 09 12:12:06 Finished compiler/backend/riscv                                  18s   1GB
Dec 09 12:12:06 Starting compiler/backend/ag32
Dec 09 12:13:20 Finished compiler/backend/ag32                                 1m13s 873MB
Dec 09 12:13:21 Starting compiler/parsing/proofs
Dec 09 12:19:25 Finished compiler/parsing/proofs                               6m03s   1GB
Dec 09 12:19:26 Starting compiler/inference/proofs
Dec 09 12:22:18 Finished compiler/inference/proofs                             2m50s   1GB
Dec 09 12:22:18 Starting compiler/backend/semantics
Dec 09 12:31:10 Finished compiler/backend/semantics                            8m50s   2GB
Dec 09 12:31:11 Starting compiler/backend/reg_alloc/proofs
Dec 09 12:33:54 Finished compiler/backend/reg_alloc/proofs                     2m42s 544MB
Dec 09 12:33:55 Starting compiler/backend/proofs
Dec 09 13:15:32 Finished compiler/backend/proofs                              41m36s   3GB
Dec 09 13:15:33 Starting compiler/encoders/x64/proofs
Dec 09 13:25:45 Finished compiler/encoders/x64/proofs                         10m11s   4GB
Dec 09 13:25:46 Starting compiler/encoders/arm6/proofs
Dec 09 13:40:50 Finished compiler/encoders/arm6/proofs                        15m03s   3GB
Dec 09 13:40:51 Starting compiler/encoders/arm8/proofs
Dec 09 13:46:56 Finished compiler/encoders/arm8/proofs                         6m04s   1GB
Dec 09 13:46:56 Starting compiler/encoders/mips/proofs
Dec 09 13:57:36 Finished compiler/encoders/mips/proofs                        10m39s   1GB
Dec 09 13:57:37 Starting compiler/encoders/riscv/proofs
Dec 09 14:05:37 Finished compiler/encoders/riscv/proofs                        7m59s 843MB
Dec 09 14:05:38 Starting compiler/encoders/ag32/proofs
Dec 09 14:08:19 Finished compiler/encoders/ag32/proofs                         2m39s 706MB
Dec 09 14:08:19 Starting compiler/backend/x64/proofs
Dec 09 14:08:39 Finished compiler/backend/x64/proofs                             19s 835MB
Dec 09 14:08:40 Starting compiler/backend/arm6/proofs
Dec 09 14:09:04 Finished compiler/backend/arm6/proofs                            23s   1GB
Dec 09 14:09:05 Starting compiler/backend/arm8/proofs
Dec 09 14:09:26 Finished compiler/backend/arm8/proofs                            20s   1GB
Dec 09 14:09:27 Starting compiler/backend/mips/proofs
Dec 09 14:09:49 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 09 14:09:50 Starting compiler/backend/riscv/proofs
Dec 09 14:10:12 Finished compiler/backend/riscv/proofs                           21s   1GB
Dec 09 14:10:13 Starting compiler/backend/ag32/proofs
Dec 09 14:19:28 Finished compiler/backend/ag32/proofs                          9m14s   2GB
Dec 09 14:19:29 Starting compiler/proofs
Dec 09 14:20:51 Finished compiler/proofs                                       1m21s   2GB
Dec 09 14:20:52 Starting candle/set-theory
Dec 09 14:21:20 Finished candle/set-theory                                       27s 642MB
Dec 09 14:21:21 Starting candle/syntax-lib
Dec 09 14:21:32 Finished candle/syntax-lib                                       10s 628MB
Dec 09 14:21:33 Starting candle/standard/syntax
Dec 09 14:23:10 Finished candle/standard/syntax                                1m36s 822MB
Dec 09 14:23:10 Starting candle/standard/semantics
Dec 09 14:24:33 Finished candle/standard/semantics                             1m21s 830MB
Dec 09 14:24:33 Starting candle/standard/monadic
Dec 09 14:26:10 Finished candle/standard/monadic                               1m35s 975MB
Dec 09 14:26:11 Starting candle/standard/ml_kernel
Dec 09 14:41:00 Finished candle/standard/ml_kernel                            14m49s   3GB
Dec 09 14:41:01 Starting candle/standard/opentheory
Dec 09 14:48:49 Finished candle/standard/opentheory                            7m47s   3GB
Dec 09 14:48:49 Starting candle/standard/opentheory/compilation
Dec 09 15:18:15 Finished candle/standard/opentheory/compilation               29m24s  15GB
Dec 09 15:18:15 Starting candle/standard/opentheory/compilation/proofs
Dec 09 15:18:54 Finished candle/standard/opentheory/compilation/proofs           37s   5GB
Dec 09 15:18:54 Starting characteristic/examples
Dec 09 15:20:24 Finished characteristic/examples                               1m28s   2GB
Dec 09 15:20:24 Starting tutorial/solutions
Dec 09 15:33:24 Finished tutorial/solutions                                   12m57s   6GB
Dec 09 15:33:25 Starting translator/monadic/examples
Dec 09 15:35:15 Finished translator/monadic/examples                           1m50s   2GB
Dec 09 15:35:16 Starting examples
Dec 09 15:41:27 Finished examples                                              6m10s   2GB
Dec 09 15:41:27 Starting examples/compilation/x64
Dec 09 17:35:45 Finished examples/compilation/x64                           1h54m16s  10GB
Dec 09 17:35:45 Starting examples/compilation/x64/proofs
Dec 09 17:37:45 Finished examples/compilation/x64/proofs                       1m58s   3GB
Dec 09 17:37:47 Starting examples/compilation/ag32
Dec 09 18:03:55 Finished examples/compilation/ag32                            26m07s   4GB
Dec 09 18:03:55 Starting examples/compilation/ag32/proofs
Dec 09 18:04:22 Finished examples/compilation/ag32/proofs                        25s   1GB
Dec 09 18:04:22 Starting compiler/benchmarks
Dec 09 18:04:23 Finished compiler/benchmarks                                      0s   5MB
Dec 09 18:04:24 Starting translator/okasaki-examples
Dec 09 18:07:54 Finished translator/okasaki-examples                           3m28s   1GB
Dec 09 18:07:54 Starting translator/other-examples
Dec 09 18:11:18 Finished translator/other-examples                             3m22s   1GB
Dec 09 18:11:18 Starting compiler/parsing/tests
Dec 09 18:11:44 Finished compiler/parsing/tests                                  24s 328MB
Dec 09 18:11:45 Starting compiler/inference/tests
Dec 09 18:15:48 Finished compiler/inference/tests                              4m02s   3GB
Dec 09 18:15:49 Starting compiler/bootstrap/translation
Dec 09 21:24:39 Finished compiler/bootstrap/translation                     3h08m49s  55GB
Dec 09 21:24:40 Starting unverified/sexpr-bootstrap/x64/64
Dec 09 21:32:52 Finished unverified/sexpr-bootstrap/x64/64                     8m10s  13GB
Dec 09 21:32:53 Starting unverified/sexpr-bootstrap/x64/32
Dec 09 21:38:25 Finished unverified/sexpr-bootstrap/x64/32                     5m30s  18GB
Dec 09 21:38:25 Starting compiler/bootstrap/compilation/x64/64
Dec 10 15:21:55 Finished compiler/bootstrap/compilation/x64/64             17h43m27s  64GB
Dec 10 15:21:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 10 15:26:19 Finished compiler/bootstrap/compilation/x64/64/proofs          4m22s  24GB
Dec 10 15:26:20 Starting compiler/bootstrap/compilation/x64/32
Dec 11 02:53:14 Finished compiler/bootstrap/compilation/x64/32             11h26m53s  63GB
Dec 11 02:53:15 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 11 02:56:19 Finished compiler/bootstrap/compilation/x64/32/proofs          3m03s  22GB
Dec 11 02:56:19 SUCCESS