Job 655

CakeML:6669d99667b1f4dbb60de32048f97f611277f41e
  Remove unused parsing gitignore [Dec 30 12:28:23]
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 30 12:43:20 Claimed job
Dec 30 12:43:25 Reusing HOL
Dec 30 12:43:36 Starting developers
Dec 30 12:43:37 Finished developers                                               0s  21MB
Dec 30 12:43:38 Starting developers/bin
Dec 30 12:44:10 Finished developers/bin                                          31s 139MB
Dec 30 12:44:11 Starting semantics/ffi
Dec 30 12:44:20 Finished semantics/ffi                                            8s 225MB
Dec 30 12:44:20 Starting semantics
Dec 30 12:45:42 Finished semantics                                             1m21s   1GB
Dec 30 12:45:43 Starting semantics/proofs
Dec 30 12:49:05 Finished semantics/proofs                                      3m21s   1GB
Dec 30 12:49:06 Starting basis/pure
Dec 30 12:49:57 Finished basis/pure                                              50s 656MB
Dec 30 12:49:58 Starting translator
Dec 30 12:51:39 Finished translator                                            1m39s   1GB
Dec 30 12:51:39 Starting compiler/parsing
Dec 30 12:52:47 Finished compiler/parsing                                      1m07s   2GB
Dec 30 12:52:48 Starting characteristic
Dec 30 12:56:03 Finished characteristic                                        3m13s   1GB
Dec 30 12:56:04 Starting translator/monadic
Dec 30 12:57:33 Finished translator/monadic                                    1m28s   1GB
Dec 30 12:57:34 Starting basis
Dec 30 13:13:59 Finished basis                                                16m24s   3GB
Dec 30 13:14:00 Starting compiler/inference
Dec 30 13:15:38 Finished compiler/inference                                    1m37s   1GB
Dec 30 13:15:39 Starting compiler/backend/reg_alloc
Dec 30 13:16:31 Finished compiler/backend/reg_alloc                              51s   1GB
Dec 30 13:16:32 Starting compiler/backend/gc
Dec 30 13:24:31 Finished compiler/backend/gc                                   7m59s   1GB
Dec 30 13:24:32 Starting compiler/backend
Dec 30 13:24:35 Finished compiler/backend                                         1s  28MB
Dec 30 13:24:35 Starting compiler/encoders/asm
Dec 30 13:24:37 Finished compiler/encoders/asm                                    0s  21MB
Dec 30 13:24:38 Starting compiler/encoders/x64
Dec 30 13:25:03 Finished compiler/encoders/x64                                   24s 922MB
Dec 30 13:25:04 Starting compiler/encoders/arm6
Dec 30 13:25:56 Finished compiler/encoders/arm6                                  51s   1GB
Dec 30 13:25:57 Starting compiler/encoders/arm8
Dec 30 13:26:10 Finished compiler/encoders/arm8                                  12s 890MB
Dec 30 13:26:11 Starting compiler/encoders/mips
Dec 30 13:26:28 Finished compiler/encoders/mips                                  16s   1GB
Dec 30 13:26:29 Starting compiler/encoders/riscv
Dec 30 13:26:44 Finished compiler/encoders/riscv                                 13s 710MB
Dec 30 13:26:44 Starting compiler/encoders/ag32
Dec 30 13:27:01 Finished compiler/encoders/ag32                                  15s 692MB
Dec 30 13:27:02 Starting compiler/backend/x64
Dec 30 13:27:19 Finished compiler/backend/x64                                    16s 804MB
Dec 30 13:27:20 Starting compiler/backend/arm6
Dec 30 13:27:40 Finished compiler/backend/arm6                                   19s   1GB
Dec 30 13:27:40 Starting compiler/backend/arm8
Dec 30 13:27:59 Finished compiler/backend/arm8                                   17s 893MB
Dec 30 13:28:00 Starting compiler/backend/mips
Dec 30 13:28:18 Finished compiler/backend/mips                                   17s 937MB
Dec 30 13:28:19 Starting compiler/backend/riscv
Dec 30 13:28:37 Finished compiler/backend/riscv                                  17s   1GB
Dec 30 13:28:37 Starting compiler/backend/ag32
Dec 30 13:29:52 Finished compiler/backend/ag32                                 1m13s   1GB
Dec 30 13:29:53 Starting compiler/parsing/proofs
Dec 30 13:36:12 Finished compiler/parsing/proofs                               6m18s 922MB
Dec 30 13:36:13 Starting compiler/inference/proofs
Dec 30 13:39:09 Finished compiler/inference/proofs                             2m54s   1GB
Dec 30 13:39:09 Starting compiler/backend/semantics
Dec 30 13:46:57 Finished compiler/backend/semantics                            7m47s   1GB
Dec 30 13:46:58 Starting compiler/backend/reg_alloc/proofs
Dec 30 13:49:47 Finished compiler/backend/reg_alloc/proofs                     2m48s   1GB
Dec 30 13:49:48 Starting compiler/backend/proofs
Dec 30 14:29:57 Finished compiler/backend/proofs                              40m08s   4GB
Dec 30 14:29:58 Starting compiler/encoders/x64/proofs
Dec 30 14:39:59 Finished compiler/encoders/x64/proofs                         10m00s   5GB
Dec 30 14:40:00 Starting compiler/encoders/arm6/proofs
Dec 30 14:54:15 Finished compiler/encoders/arm6/proofs                        14m13s   3GB
Dec 30 14:54:16 Starting compiler/encoders/arm8/proofs
Dec 30 15:00:23 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
Dec 30 15:00:23 Starting compiler/encoders/mips/proofs
Dec 30 15:11:02 Finished compiler/encoders/mips/proofs                        10m38s   3GB
Dec 30 15:11:03 Starting compiler/encoders/riscv/proofs
Dec 30 15:19:01 Finished compiler/encoders/riscv/proofs                        7m57s   1GB
Dec 30 15:19:02 Starting compiler/encoders/ag32/proofs
Dec 30 15:21:49 Finished compiler/encoders/ag32/proofs                         2m46s 669MB
Dec 30 15:21:50 Starting compiler/backend/x64/proofs
Dec 30 15:22:10 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 30 15:22:10 Starting compiler/backend/arm6/proofs
Dec 30 15:22:32 Finished compiler/backend/arm6/proofs                            20s 981MB
Dec 30 15:22:32 Starting compiler/backend/arm8/proofs
Dec 30 15:22:51 Finished compiler/backend/arm8/proofs                            18s   1GB
Dec 30 15:22:52 Starting compiler/backend/mips/proofs
Dec 30 15:23:12 Finished compiler/backend/mips/proofs                            18s 938MB
Dec 30 15:23:13 Starting compiler/backend/riscv/proofs
Dec 30 15:23:33 Finished compiler/backend/riscv/proofs                           19s   1GB
Dec 30 15:23:34 Starting compiler/backend/ag32/proofs
Dec 30 15:33:09 Finished compiler/backend/ag32/proofs                          9m34s   2GB
Dec 30 15:33:10 Starting compiler/proofs
Dec 30 15:34:32 Finished compiler/proofs                                       1m21s   3GB
Dec 30 15:34:33 Starting candle/set-theory
Dec 30 15:34:59 Finished candle/set-theory                                       25s 652MB
Dec 30 15:35:00 Starting candle/syntax-lib
Dec 30 15:35:11 Finished candle/syntax-lib                                        9s 641MB
Dec 30 15:35:11 Starting candle/standard/syntax
Dec 30 15:37:02 Finished candle/standard/syntax                                1m49s   1GB
Dec 30 15:37:03 Starting candle/standard/semantics
Dec 30 15:38:44 Finished candle/standard/semantics                             1m40s   1GB
Dec 30 15:38:44 Starting candle/standard/monadic
Dec 30 15:40:28 Finished candle/standard/monadic                               1m43s   1GB
Dec 30 15:40:29 Starting candle/standard/ml_kernel
Dec 30 15:56:35 Finished candle/standard/ml_kernel                            16m04s   3GB
Dec 30 15:56:36 Starting candle/standard/opentheory
Dec 30 16:05:38 Finished candle/standard/opentheory                            9m01s   4GB
Dec 30 16:05:39 Starting candle/standard/opentheory/compilation
Dec 30 16:34:57 Finished candle/standard/opentheory/compilation               29m17s  25GB
Dec 30 16:34:58 Starting candle/standard/opentheory/compilation/proofs
Dec 30 16:35:46 Finished candle/standard/opentheory/compilation/proofs           47s   5GB
Dec 30 16:35:47 Starting characteristic/examples
Dec 30 16:37:18 Finished characteristic/examples                               1m30s   2GB
Dec 30 16:37:19 Starting tutorial/solutions
Dec 30 16:50:34 Finished tutorial/solutions                                   13m14s   6GB
Dec 30 16:50:35 Starting translator/monadic/examples
Dec 30 16:52:46 Finished translator/monadic/examples                           2m10s   2GB
Dec 30 16:52:47 Starting examples
Dec 30 17:00:53 Finished examples                                              8m05s   3GB
Dec 30 17:00:54 Starting examples/compilation/x64
Dec 30 19:02:43 Finished examples/compilation/x64                           2h01m48s  13GB
Dec 30 19:02:44 Starting examples/compilation/x64/proofs
Dec 30 19:04:36 Finished examples/compilation/x64/proofs                       1m50s   5GB
Dec 30 19:04:37 Starting examples/compilation/ag32
Dec 30 19:33:14 Finished examples/compilation/ag32                            28m37s   5GB
Dec 30 19:33:15 Starting examples/compilation/ag32/proofs
Dec 30 19:34:04 Finished examples/compilation/ag32/proofs                        47s   4GB
Dec 30 19:34:04 Starting translator/okasaki-examples
Dec 30 19:38:22 Finished translator/okasaki-examples                           4m16s   1GB
Dec 30 19:38:22 Starting translator/other-examples
Dec 30 19:39:05 Finished translator/other-examples                               41s   1GB
Dec 30 19:39:06 Starting compiler/parsing/tests
Dec 30 19:39:33 Finished compiler/parsing/tests                                  26s 611MB
Dec 30 19:39:34 Starting compiler/inference/tests
Dec 30 19:43:41 Finished compiler/inference/tests                              4m06s   4GB
Dec 30 19:43:42 Starting compiler/bootstrap/translation Dec 30 19:43:42 19519s