Job 646

CakeML:5fde2ea383d1fb3e1d09be9e216ab14d3ea90fbb
  Document namespace.lem [Dec 23 19:04:57]
#589 (compiler-exit-code)
Merging into:75614126e5170e953dbab330960f90b715bf38b3
  Fix to_bvlProg [Dec 22 15:37:42]
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
  Fix bug: TypeBase.simpls_of not being filled in on load [Dec 21 04:04:45]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Dec 23 19:07:42 Claimed job
Dec 23 19:07:48 Reusing HOL
Dec 23 19:07:58 Starting developers
Dec 23 19:08:00 Finished developers                                               0s  21MB
Dec 23 19:08:01 Starting developers/bin
Dec 23 19:08:37 Finished developers/bin                                          35s 140MB
Dec 23 19:08:38 Starting semantics/ffi
Dec 23 19:08:48 Finished semantics/ffi                                            9s 217MB
Dec 23 19:08:49 Starting semantics
Dec 23 19:10:16 Finished semantics                                             1m26s   1GB
Dec 23 19:10:17 Starting semantics/proofs
Dec 23 19:13:35 Finished semantics/proofs                                      3m17s   1GB
Dec 23 19:13:36 Starting basis/pure
Dec 23 19:14:27 Finished basis/pure                                              50s 579MB
Dec 23 19:14:28 Starting translator
Dec 23 19:16:07 Finished translator                                            1m38s   1GB
Dec 23 19:16:08 Starting compiler/parsing
Dec 23 19:17:13 Finished compiler/parsing                                      1m04s   1GB
Dec 23 19:17:14 Starting characteristic
Dec 23 19:20:29 Finished characteristic                                        3m13s   1GB
Dec 23 19:20:30 Starting translator/monadic
Dec 23 19:21:58 Finished translator/monadic                                    1m27s   1GB
Dec 23 19:21:58 Starting basis
Dec 23 19:38:08 Finished basis                                                16m08s   3GB
Dec 23 19:38:09 Starting compiler/inference
Dec 23 19:39:50 Finished compiler/inference                                    1m40s   1GB
Dec 23 19:39:51 Starting compiler/backend/reg_alloc
Dec 23 19:40:43 Finished compiler/backend/reg_alloc                              51s   1GB
Dec 23 19:40:44 Starting compiler/backend/gc
Dec 23 19:48:43 Finished compiler/backend/gc                                   7m58s   1GB
Dec 23 19:48:44 Starting compiler/backend
Dec 23 19:48:46 Finished compiler/backend                                         1s  17MB
Dec 23 19:48:47 Starting compiler/encoders/asm
Dec 23 19:48:49 Finished compiler/encoders/asm                                    0s  17MB
Dec 23 19:48:49 Starting compiler/encoders/x64
Dec 23 19:49:15 Finished compiler/encoders/x64                                   24s 958MB
Dec 23 19:49:15 Starting compiler/encoders/arm6
Dec 23 19:50:07 Finished compiler/encoders/arm6                                  51s   1GB
Dec 23 19:50:08 Starting compiler/encoders/arm8
Dec 23 19:50:22 Finished compiler/encoders/arm8                                  12s 858MB
Dec 23 19:50:22 Starting compiler/encoders/mips
Dec 23 19:50:40 Finished compiler/encoders/mips                                  16s   1GB
Dec 23 19:50:41 Starting compiler/encoders/riscv
Dec 23 19:50:55 Finished compiler/encoders/riscv                                 13s 848MB
Dec 23 19:50:56 Starting compiler/encoders/ag32
Dec 23 19:51:13 Finished compiler/encoders/ag32                                  15s 848MB
Dec 23 19:51:13 Starting compiler/backend/x64
Dec 23 19:51:30 Finished compiler/backend/x64                                    16s 892MB
Dec 23 19:51:31 Starting compiler/backend/arm6
Dec 23 19:51:49 Finished compiler/backend/arm6                                   17s   1GB
Dec 23 19:51:50 Starting compiler/backend/arm8
Dec 23 19:52:08 Finished compiler/backend/arm8                                   17s   1GB
Dec 23 19:52:09 Starting compiler/backend/mips
Dec 23 19:52:28 Finished compiler/backend/mips                                   17s   1GB
Dec 23 19:52:29 Starting compiler/backend/riscv
Dec 23 19:52:48 Finished compiler/backend/riscv                                  18s   1GB
Dec 23 19:52:49 Starting compiler/backend/ag32
Dec 23 19:54:02 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 23 19:54:03 Starting compiler/parsing/proofs
Dec 23 20:00:15 Finished compiler/parsing/proofs                               6m10s   1GB
Dec 23 21:01:51 Resuming compiler/inference/proofs
Dec 23 21:04:47 Finished compiler/inference/proofs                             2m54s   1GB
Dec 23 21:04:48 Starting compiler/backend/semantics
Dec 23 21:12:30 Finished compiler/backend/semantics                            7m41s   2GB
Dec 23 21:12:31 Starting compiler/backend/reg_alloc/proofs
Dec 23 21:15:15 Finished compiler/backend/reg_alloc/proofs                     2m43s 912MB
Dec 23 21:15:16 Starting compiler/backend/proofs
Dec 23 21:55:27 Finished compiler/backend/proofs                              40m09s   3GB
Dec 23 21:55:28 Starting compiler/encoders/x64/proofs
Dec 23 22:05:37 Finished compiler/encoders/x64/proofs                         10m06s   4GB
Dec 23 22:05:38 Starting compiler/encoders/arm6/proofs
Dec 23 22:19:43 Finished compiler/encoders/arm6/proofs                        14m04s   3GB
Dec 23 22:19:44 Starting compiler/encoders/arm8/proofs
Dec 23 22:25:52 Finished compiler/encoders/arm8/proofs                         6m07s   1GB
Dec 23 22:25:53 Starting compiler/encoders/mips/proofs
Dec 23 22:36:47 Finished compiler/encoders/mips/proofs                        10m53s   2GB
Dec 23 22:36:48 Starting compiler/encoders/riscv/proofs
Dec 23 22:44:52 Finished compiler/encoders/riscv/proofs                        8m03s   1GB
Dec 23 22:44:53 Starting compiler/encoders/ag32/proofs
Dec 23 22:47:39 Finished compiler/encoders/ag32/proofs                         2m45s 668MB
Dec 23 22:47:40 Starting compiler/backend/x64/proofs
Dec 23 22:48:00 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 23 22:48:00 Starting compiler/backend/arm6/proofs
Dec 23 22:48:23 Finished compiler/backend/arm6/proofs                            21s   1GB
Dec 23 22:48:23 Starting compiler/backend/arm8/proofs
Dec 23 22:48:42 Finished compiler/backend/arm8/proofs                            17s   1GB
Dec 23 22:48:43 Starting compiler/backend/mips/proofs
Dec 23 22:49:03 Finished compiler/backend/mips/proofs                            19s   1GB
Dec 23 22:49:04 Starting compiler/backend/riscv/proofs
Dec 23 22:49:24 Finished compiler/backend/riscv/proofs                           19s   1GB
Dec 23 22:49:25 Starting compiler/backend/ag32/proofs
Dec 23 22:59:13 Finished compiler/backend/ag32/proofs                          9m47s   2GB
Dec 23 22:59:14 Starting compiler/proofs
Dec 23 23:00:35 Finished compiler/proofs                                       1m20s   3GB
Dec 23 23:00:36 Starting candle/set-theory
Dec 23 23:01:01 Finished candle/set-theory                                       24s 676MB
Dec 23 23:01:02 Starting candle/syntax-lib
Dec 23 23:01:13 Finished candle/syntax-lib                                        9s 658MB
Dec 23 23:01:13 Starting candle/standard/syntax
Dec 23 23:03:03 Finished candle/standard/syntax                                1m48s   1GB
Dec 23 23:03:04 Starting candle/standard/semantics
Dec 23 23:04:43 Finished candle/standard/semantics                             1m38s   1GB
Dec 23 23:04:44 Starting candle/standard/monadic
Dec 23 23:06:30 Finished candle/standard/monadic                               1m43s   1GB
Dec 23 23:06:31 Starting candle/standard/ml_kernel
Dec 23 23:22:18 Finished candle/standard/ml_kernel                            15m46s   3GB
Dec 23 23:22:18 Starting candle/standard/opentheory
Dec 23 23:31:05 Finished candle/standard/opentheory                            8m46s   5GB
Dec 23 23:31:06 Starting candle/standard/opentheory/compilation
Dec 24 00:01:28 Finished candle/standard/opentheory/compilation               30m21s  15GB
Dec 24 00:01:29 Starting candle/standard/opentheory/compilation/proofs
Dec 24 00:02:13 Finished candle/standard/opentheory/compilation/proofs           42s   4GB
Dec 24 00:02:14 Starting characteristic/examples
Dec 24 00:03:49 Finished characteristic/examples                               1m34s   3GB
Dec 24 00:03:49 Starting tutorial/solutions
Dec 24 00:17:13 Finished tutorial/solutions                                   13m22s   9GB
Dec 24 00:17:14 Starting translator/monadic/examples
Dec 24 00:19:23 Finished translator/monadic/examples                           2m08s   2GB
Dec 24 00:19:24 Starting examples
Dec 24 00:27:14 Finished examples                                              7m49s   4GB
Dec 24 00:27:15 Starting examples/compilation/x64
Dec 24 02:30:49 Finished examples/compilation/x64                           2h03m33s  11GB
Dec 24 02:30:50 Starting examples/compilation/x64/proofs
Dec 24 02:32:42 Finished examples/compilation/x64/proofs                       1m51s   4GB
Dec 24 02:32:43 Starting examples/compilation/ag32
Dec 24 03:00:39 Finished examples/compilation/ag32                            27m55s   5GB
Dec 24 03:00:40 Starting examples/compilation/ag32/proofs
Dec 24 03:01:27 Finished examples/compilation/ag32/proofs                        46s   3GB
Dec 24 03:01:28 Starting translator/okasaki-examples
Dec 24 03:05:34 Finished translator/okasaki-examples                           4m04s   2GB
Dec 24 03:05:34 Starting translator/other-examples
Dec 24 03:06:16 Finished translator/other-examples                               40s   1GB
Dec 24 03:06:17 Starting compiler/parsing/tests
Dec 24 03:06:45 Finished compiler/parsing/tests                                  26s 443MB
Dec 24 03:06:45 Starting compiler/inference/tests
Dec 24 03:10:46 Finished compiler/inference/tests                              3m59s   4GB
Dec 24 03:10:47 Starting compiler/bootstrap/translation
Dec 24 06:33:12 Finished compiler/bootstrap/translation                     3h22m24s  53GB
Dec 24 06:33:13 Starting unverified/sexpr-bootstrap/x64/64
Dec 24 06:36:48 Finished unverified/sexpr-bootstrap/x64/64                     3m34s  14GB
Dec 24 06:36:48 Starting unverified/sexpr-bootstrap/x64/32
Dec 24 06:38:49 Finished unverified/sexpr-bootstrap/x64/32                     1m59s  20GB
Dec 24 06:38:50 Starting compiler/bootstrap/compilation/x64/64
Dec 24 16:50:40 Finished compiler/bootstrap/compilation/x64/64             10h11m49s  63GB
Dec 24 16:50:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 24 16:56:52 Finished compiler/bootstrap/compilation/x64/64/proofs          6m10s  32GB
Dec 24 16:56:53 Starting compiler/bootstrap/compilation/x64/32
Dec 25 01:57:50 Finished compiler/bootstrap/compilation/x64/32              9h00m55s  64GB
Dec 25 01:57:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 25 02:03:54 Finished compiler/bootstrap/compilation/x64/32/proofs          6m02s  31GB
Dec 25 02:03:54 SUCCESS