Job 695

CakeML:132124a020e9f4e4bb00fb0274f9505461195904
  Merge pull request #608 from CakeML/cheats [Jan 21 17:46:50]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 21 22:00:44 Claimed job
Jan 21 22:00:48 Reusing HOL
Jan 21 22:01:39 Starting developers
Jan 21 22:01:42 Finished developers                                               2s  20MB
Jan 21 22:01:42 Starting developers/bin
Jan 21 22:02:48 Finished developers/bin                                        1m04s 916MB
Jan 21 22:02:48 Starting semantics/ffi
Jan 21 22:02:59 Finished semantics/ffi                                            9s 236MB
Jan 21 22:02:59 Starting semantics
Jan 21 22:04:23 Finished semantics                                             1m23s   1GB
Jan 21 22:04:24 Starting semantics/proofs
Jan 21 22:07:41 Finished semantics/proofs                                      3m16s   1GB
Jan 21 22:07:42 Starting basis/pure
Jan 21 22:08:30 Finished basis/pure                                              47s 822MB
Jan 21 22:08:30 Starting translator
Jan 21 22:10:11 Finished translator                                            1m40s   1GB
Jan 21 22:10:12 Starting compiler/parsing
Jan 21 22:11:17 Finished compiler/parsing                                      1m04s   2GB
Jan 21 22:11:18 Starting characteristic
Jan 21 22:14:38 Finished characteristic                                        3m19s   2GB
Jan 21 22:14:38 Starting translator/monadic
Jan 21 22:16:09 Finished translator/monadic                                    1m30s   1GB
Jan 21 22:16:10 Starting basis
Jan 21 22:32:52 Finished basis                                                16m41s   3GB
Jan 21 22:32:52 Starting compiler/inference
Jan 21 22:34:33 Finished compiler/inference                                    1m39s   2GB
Jan 21 22:34:33 Starting compiler/backend/reg_alloc
Jan 21 22:35:26 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 21 22:35:27 Starting compiler/backend/gc
Jan 21 22:43:25 Finished compiler/backend/gc                                   7m57s   1GB
Jan 21 22:43:26 Starting compiler/backend
Jan 21 22:43:29 Finished compiler/backend                                         2s  22MB
Jan 21 22:43:30 Starting compiler/encoders/asm
Jan 21 22:43:32 Finished compiler/encoders/asm                                    1s  26MB
Jan 21 22:43:32 Starting compiler/encoders/x64
Jan 21 22:43:58 Finished compiler/encoders/x64                                   25s   1GB
Jan 21 22:43:59 Starting compiler/encoders/arm6
Jan 21 22:44:52 Finished compiler/encoders/arm6                                  52s 767MB
Jan 21 22:44:53 Starting compiler/encoders/arm8
Jan 21 22:45:06 Finished compiler/encoders/arm8                                  13s 582MB
Jan 21 22:45:07 Starting compiler/encoders/mips
Jan 21 22:45:25 Finished compiler/encoders/mips                                  17s   1GB
Jan 21 22:45:26 Starting compiler/encoders/riscv
Jan 21 22:45:41 Finished compiler/encoders/riscv                                 14s 815MB
Jan 21 22:45:42 Starting compiler/encoders/ag32
Jan 21 22:45:59 Finished compiler/encoders/ag32                                  17s 827MB
Jan 21 22:46:00 Starting compiler/backend/x64
Jan 21 22:46:18 Finished compiler/backend/x64                                    17s   1GB
Jan 21 22:46:19 Starting compiler/backend/arm6
Jan 21 22:46:38 Finished compiler/backend/arm6                                   18s   1GB
Jan 21 22:46:39 Starting compiler/backend/arm8
Jan 21 22:46:58 Finished compiler/backend/arm8                                   18s   1GB
Jan 21 22:46:58 Starting compiler/backend/mips
Jan 21 22:47:16 Finished compiler/backend/mips                                   17s   1GB
Jan 21 22:47:17 Starting compiler/backend/riscv
Jan 21 22:47:37 Finished compiler/backend/riscv                                  19s   1GB
Jan 21 22:47:38 Starting compiler/backend/ag32
Jan 21 22:48:50 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 21 22:48:51 Starting compiler/parsing/proofs
Jan 21 22:54:43 Finished compiler/parsing/proofs                               5m51s   1GB
Jan 21 22:54:44 Starting compiler/inference/proofs
Jan 21 22:57:38 Finished compiler/inference/proofs                             2m53s   1GB
Jan 21 22:57:39 Starting compiler/backend/semantics
Jan 21 23:05:06 Finished compiler/backend/semantics                            7m26s   2GB
Jan 21 23:05:06 Starting compiler/backend/reg_alloc/proofs
Jan 21 23:07:49 Finished compiler/backend/reg_alloc/proofs                     2m42s 971MB
Jan 21 23:07:49 Starting compiler/backend/proofs
Jan 21 23:46:38 Finished compiler/backend/proofs                              38m48s   3GB
Jan 21 23:46:39 Starting compiler/encoders/x64/proofs
Jan 21 23:56:31 Finished compiler/encoders/x64/proofs                          9m50s   4GB
Jan 21 23:56:31 Starting compiler/encoders/arm6/proofs
Jan 22 00:10:21 Finished compiler/encoders/arm6/proofs                        13m49s   6GB
Jan 22 00:10:22 Starting compiler/encoders/arm8/proofs
Jan 22 00:16:22 Finished compiler/encoders/arm8/proofs                         5m59s   1GB
Jan 22 00:16:22 Starting compiler/encoders/mips/proofs
Jan 22 00:26:53 Finished compiler/encoders/mips/proofs                        10m29s   2GB
Jan 22 00:26:54 Starting compiler/encoders/riscv/proofs
Jan 22 00:34:43 Finished compiler/encoders/riscv/proofs                        7m49s   1GB
Jan 22 00:34:44 Starting compiler/encoders/ag32/proofs
Jan 22 00:37:30 Finished compiler/encoders/ag32/proofs                         2m45s 560MB
Jan 22 00:37:30 Starting compiler/backend/x64/proofs
Jan 22 00:37:52 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 22 00:37:53 Starting compiler/backend/arm6/proofs
Jan 22 00:38:15 Finished compiler/backend/arm6/proofs                            21s 931MB
Jan 22 00:38:16 Starting compiler/backend/arm8/proofs
Jan 22 00:38:36 Finished compiler/backend/arm8/proofs                            20s   1GB
Jan 22 00:38:37 Starting compiler/backend/mips/proofs
Jan 22 00:38:58 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 22 00:38:59 Starting compiler/backend/riscv/proofs
Jan 22 00:39:19 Finished compiler/backend/riscv/proofs                           19s 847MB
Jan 22 00:39:19 Starting compiler/backend/ag32/proofs
Jan 22 00:48:39 Finished compiler/backend/ag32/proofs                          9m18s   2GB
Jan 22 00:48:39 Starting compiler/proofs
Jan 22 00:50:03 Finished compiler/proofs                                       1m23s   3GB
Jan 22 00:50:04 Starting candle/set-theory
Jan 22 00:50:32 Finished candle/set-theory                                       27s 702MB
Jan 22 00:50:33 Starting candle/syntax-lib
Jan 22 00:50:44 Finished candle/syntax-lib                                       10s 629MB
Jan 22 00:50:45 Starting candle/standard/syntax
Jan 22 00:52:36 Finished candle/standard/syntax                                1m51s 820MB
Jan 22 00:52:37 Starting candle/standard/semantics
Jan 22 00:54:20 Finished candle/standard/semantics                             1m42s   1GB
Jan 22 00:54:21 Starting candle/standard/monadic
Jan 22 00:56:04 Finished candle/standard/monadic                               1m42s   1GB
Jan 22 00:56:05 Starting candle/standard/ml_kernel
Jan 22 00:59:55 Finished candle/standard/ml_kernel                             3m48s   3GB
Jan 22 00:59:55 Starting candle/standard/opentheory
Jan 22 01:08:47 Finished candle/standard/opentheory                            8m50s   4GB
Jan 22 01:08:47 Starting candle/standard/opentheory/compilation
Jan 22 01:38:32 Finished candle/standard/opentheory/compilation               29m44s  16GB
Jan 22 01:38:33 Starting candle/standard/opentheory/compilation/proofs
Jan 22 01:39:21 Finished candle/standard/opentheory/compilation/proofs           48s   6GB
Jan 22 01:39:22 Starting characteristic/examples
Jan 22 01:40:49 Finished characteristic/examples                               1m26s   3GB
Jan 22 01:40:50 Starting tutorial/solutions
Jan 22 01:54:24 Finished tutorial/solutions                                   13m33s   6GB
Jan 22 01:54:24 Starting translator/monadic/examples
Jan 22 01:56:35 Finished translator/monadic/examples                           2m10s   2GB
Jan 22 01:56:36 Starting examples
Jan 22 02:04:14 Finished examples                                              7m36s   4GB
Jan 22 02:04:14 Starting examples/compilation/x64
Jan 22 03:56:44 Finished examples/compilation/x64                           1h52m28s  11GB
Jan 22 03:56:44 Starting examples/compilation/x64/proofs
Jan 22 03:58:33 Finished examples/compilation/x64/proofs                       1m48s   4GB
Jan 22 03:58:34 Starting examples/compilation/ag32
Jan 22 04:26:41 Finished examples/compilation/ag32                            28m06s   6GB
Jan 22 04:26:42 Starting examples/compilation/ag32/proofs
Jan 22 04:27:30 Finished examples/compilation/ag32/proofs                        47s   3GB
Jan 22 04:27:31 Starting translator/okasaki-examples
Jan 22 04:31:37 Finished translator/okasaki-examples                           4m05s   1GB
Jan 22 04:31:38 Starting translator/other-examples
Jan 22 04:32:21 Finished translator/other-examples                               42s   1GB
Jan 22 04:32:22 Starting compiler/parsing/tests
Jan 22 04:32:49 Finished compiler/parsing/tests                                  26s 554MB
Jan 22 04:32:49 Starting compiler/inference/tests
Jan 22 04:36:51 Finished compiler/inference/tests                              4m01s   5GB
Jan 22 04:36:52 Starting compiler/bootstrap/translation
Jan 22 07:06:20 Finished compiler/bootstrap/translation                     2h29m27s  38GB
Jan 22 07:06:21 Starting unverified/sexpr-bootstrap/x64/64
Jan 22 07:15:12 Finished unverified/sexpr-bootstrap/x64/64                     8m49s  17GB
Jan 22 07:15:13 Starting unverified/sexpr-bootstrap/x64/32
Jan 22 07:20:30 Finished unverified/sexpr-bootstrap/x64/32                     5m15s  19GB
Jan 22 07:20:30 Starting compiler/bootstrap/compilation/x64/64
Jan 22 17:38:28 Finished compiler/bootstrap/compilation/x64/64             10h17m55s  64GB
Jan 22 17:38:28 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 22 17:45:02 Finished compiler/bootstrap/compilation/x64/64/proofs          6m32s  33GB
Jan 22 17:45:02 Starting compiler/bootstrap/compilation/x64/32
Jan 23 02:52:51 Finished compiler/bootstrap/compilation/x64/32              9h07m46s  64GB
Jan 23 02:52:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 23 02:58:41 Finished compiler/bootstrap/compilation/x64/32/proofs          5m49s  29GB
Jan 23 02:58:42 SUCCESS