Job 817

CakeML:5206af9f67eb4da34374600de68d6fd8c1385a43
  Merge pull request #632 from CakeML/extend_arm8 [Apr 25 17:43:37]
HOL:d9d262ad8402d865a72735480268b9f2da63fcd9
  Change ThmSetData to store just theorem names in .dat files [Apr 21 04:26:27]
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

Apr 25 21:00:02 Claimed job
Apr 25 21:00:16 Reusing HOL
Apr 25 21:01:07 Starting developers
Apr 25 21:01:09 Finished developers                                               2s  20MB
Apr 25 21:01:09 Starting developers/bin
Apr 25 21:02:26 Finished developers/bin                                        1m16s 918MB
Apr 25 21:02:26 Starting semantics/ffi
Apr 25 21:02:36 Finished semantics/ffi                                            9s 229MB
Apr 25 21:02:36 Starting semantics
Apr 25 21:03:57 Finished semantics                                             1m20s   1GB
Apr 25 21:03:57 Starting semantics/proofs
Apr 25 21:06:54 Finished semantics/proofs                                      2m56s   1GB
Apr 25 21:06:54 Starting basis/pure
Apr 25 21:07:41 Finished basis/pure                                              46s 644MB
Apr 25 21:07:42 Starting translator
Apr 25 21:09:21 Finished translator                                            1m39s   1GB
Apr 25 21:09:22 Starting compiler/parsing
Apr 25 21:10:19 Finished compiler/parsing                                        57s   2GB
Apr 25 21:10:19 Starting characteristic
Apr 25 21:15:31 Finished characteristic                                        5m11s   1GB
Apr 25 21:15:32 Starting translator/monadic
Apr 25 21:16:59 Finished translator/monadic                                    1m26s   1GB
Apr 25 21:16:59 Starting basis
Apr 25 21:33:24 Finished basis                                                16m24s   2GB
Apr 25 21:33:24 Starting compiler/inference
Apr 25 21:34:56 Finished compiler/inference                                    1m31s   1GB
Apr 25 21:34:56 Starting compiler/backend/reg_alloc
Apr 25 21:35:49 Finished compiler/backend/reg_alloc                              52s   1GB
Apr 25 21:35:49 Starting compiler/backend/gc
Apr 25 21:43:48 Finished compiler/backend/gc                                   7m58s   1GB
Apr 25 21:43:49 Starting compiler/backend
Apr 25 21:43:51 Finished compiler/backend                                         2s  20MB
Apr 25 21:43:52 Starting compiler/encoders/asm
Apr 25 21:43:53 Finished compiler/encoders/asm                                    1s  13MB
Apr 25 21:43:53 Starting compiler/encoders/x64
Apr 25 21:44:18 Finished compiler/encoders/x64                                   24s 649MB
Apr 25 21:44:18 Starting compiler/encoders/arm6
Apr 25 21:45:03 Finished compiler/encoders/arm6                                  44s 700MB
Apr 25 21:45:03 Starting compiler/encoders/arm8
Apr 25 21:45:17 Finished compiler/encoders/arm8                                  13s 886MB
Apr 25 21:45:17 Starting compiler/encoders/mips
Apr 25 21:45:34 Finished compiler/encoders/mips                                  17s   1GB
Apr 25 21:45:34 Starting compiler/encoders/riscv
Apr 25 21:45:49 Finished compiler/encoders/riscv                                 14s 825MB
Apr 25 21:45:50 Starting compiler/encoders/ag32
Apr 25 21:46:07 Finished compiler/encoders/ag32                                  16s 502MB
Apr 25 21:46:07 Starting compiler/backend/x64
Apr 25 21:46:25 Finished compiler/backend/x64                                    17s   1GB
Apr 25 21:46:25 Starting compiler/backend/arm6
Apr 25 21:46:45 Finished compiler/backend/arm6                                   19s   1GB
Apr 25 21:46:45 Starting compiler/backend/arm8
Apr 25 21:47:04 Finished compiler/backend/arm8                                   18s   1GB
Apr 25 21:47:04 Starting compiler/backend/mips
Apr 25 21:47:23 Finished compiler/backend/mips                                   18s   1GB
Apr 25 21:47:23 Starting compiler/backend/riscv
Apr 25 21:47:42 Finished compiler/backend/riscv                                  18s   1GB
Apr 25 21:47:42 Starting compiler/backend/ag32
Apr 25 21:48:49 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 25 21:48:50 Starting compiler/parsing/proofs
Apr 25 21:54:23 Finished compiler/parsing/proofs                               5m33s   1GB
Apr 25 21:54:24 Starting compiler/inference/proofs
Apr 25 21:57:03 Finished compiler/inference/proofs                             2m39s   1GB
Apr 25 21:57:03 Starting compiler/backend/semantics
Apr 25 22:03:56 Finished compiler/backend/semantics                            6m52s   2GB
Apr 25 22:03:56 Starting compiler/backend/reg_alloc/proofs
Apr 25 22:06:36 Finished compiler/backend/reg_alloc/proofs                     2m39s 758MB
Apr 25 22:06:36 Starting compiler/backend/proofs
Apr 25 22:43:52 Finished compiler/backend/proofs                              37m15s   4GB
Apr 25 22:43:52 Starting compiler/encoders/x64/proofs
Apr 25 22:52:50 Finished compiler/encoders/x64/proofs                          8m57s   4GB
Apr 25 22:52:50 Starting compiler/encoders/arm6/proofs
Apr 25 23:04:42 Finished compiler/encoders/arm6/proofs                        11m51s   3GB
Apr 25 23:04:42 Starting compiler/encoders/arm8/proofs
Apr 25 23:11:03 Finished compiler/encoders/arm8/proofs                         6m20s   1GB
Apr 25 23:11:03 Starting compiler/encoders/mips/proofs
Apr 25 23:20:13 Finished compiler/encoders/mips/proofs                         9m10s   3GB
Apr 25 23:20:14 Starting compiler/encoders/riscv/proofs
Apr 25 23:28:20 Finished compiler/encoders/riscv/proofs                        8m06s   1GB
Apr 25 23:28:20 Starting compiler/encoders/ag32/proofs
Apr 25 23:30:47 Finished compiler/encoders/ag32/proofs                         2m26s 706MB
Apr 25 23:30:47 Starting compiler/backend/x64/proofs
Apr 25 23:31:06 Finished compiler/backend/x64/proofs                             18s 834MB
Apr 25 23:31:06 Starting compiler/backend/arm6/proofs
Apr 25 23:31:29 Finished compiler/backend/arm6/proofs                            22s   1GB
Apr 25 23:31:29 Starting compiler/backend/arm8/proofs
Apr 25 23:31:48 Finished compiler/backend/arm8/proofs                            18s 786MB
Apr 25 23:31:49 Starting compiler/backend/mips/proofs
Apr 25 23:32:09 Finished compiler/backend/mips/proofs                            20s   1GB
Apr 25 23:32:10 Starting compiler/backend/riscv/proofs
Apr 25 23:32:30 Finished compiler/backend/riscv/proofs                           19s   1GB
Apr 25 23:32:30 Starting compiler/backend/ag32/proofs
Apr 25 23:41:10 Finished compiler/backend/ag32/proofs                          8m39s   2GB
Apr 25 23:41:10 Starting compiler/proofs
Apr 25 23:42:28 Finished compiler/proofs                                       1m17s   3GB
Apr 25 23:42:28 Starting candle/set-theory
Apr 25 23:42:55 Finished candle/set-theory                                       26s 640MB
Apr 25 23:42:55 Starting candle/syntax-lib
Apr 25 23:43:06 Finished candle/syntax-lib                                       10s 656MB
Apr 25 23:43:06 Starting candle/standard/syntax
Apr 25 23:44:49 Finished candle/standard/syntax                                1m42s 960MB
Apr 25 23:44:50 Starting candle/standard/semantics
Apr 25 23:46:27 Finished candle/standard/semantics                             1m37s   1GB
Apr 25 23:46:27 Starting candle/standard/monadic
Apr 25 23:47:59 Finished candle/standard/monadic                               1m31s   1GB
Apr 25 23:48:00 Starting candle/standard/ml_kernel
Apr 25 23:51:39 Finished candle/standard/ml_kernel                             3m39s   3GB
Apr 25 23:51:40 Starting candle/standard/opentheory
Apr 26 00:00:00 Finished candle/standard/opentheory                            8m19s   4GB
Apr 26 00:00:00 Starting candle/standard/opentheory/compilation
Apr 26 00:28:55 Finished candle/standard/opentheory/compilation               28m54s  13GB
Apr 26 00:28:55 Starting candle/standard/opentheory/compilation/proofs
Apr 26 00:29:40 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
Apr 26 00:29:40 Starting characteristic/examples
Apr 26 00:31:06 Finished characteristic/examples                               1m25s   2GB
Apr 26 00:31:06 Starting tutorial/solutions
Apr 26 00:44:17 Finished tutorial/solutions                                   13m10s   6GB
Apr 26 00:44:17 Starting translator/monadic/examples
Apr 26 00:46:43 Finished translator/monadic/examples                           2m25s   2GB
Apr 26 00:46:43 Starting examples
Apr 26 00:54:57 Finished examples                                              8m14s   4GB
Apr 26 00:54:57 Starting examples/compilation/x64
Apr 26 02:49:42 Finished examples/compilation/x64                           1h54m43s  10GB
Apr 26 02:49:42 Starting examples/compilation/x64/proofs
Apr 26 02:51:10 Finished examples/compilation/x64/proofs                       1m27s   2GB
Apr 26 02:51:10 Starting examples/compilation/ag32
Apr 26 03:19:42 Finished examples/compilation/ag32                            28m31s   5GB
Apr 26 03:19:42 Starting examples/compilation/ag32/proofs
Apr 26 03:20:33 Finished examples/compilation/ag32/proofs                        50s   3GB
Apr 26 03:20:33 Starting translator/okasaki-examples
Apr 26 03:24:35 Finished translator/okasaki-examples                           4m01s   1GB
Apr 26 03:24:35 Starting translator/other-examples
Apr 26 03:25:18 Finished translator/other-examples                               42s   1GB
Apr 26 03:25:18 Starting compiler/parsing/tests
Apr 26 03:25:44 Finished compiler/parsing/tests                                  25s 510MB
Apr 26 03:25:44 Starting compiler/inference/tests
Apr 26 03:29:50 Finished compiler/inference/tests                              4m05s   4GB
Apr 26 03:29:50 Starting compiler/bootstrap/translation
Apr 26 05:49:48 Finished compiler/bootstrap/translation                     2h19m57s  43GB
Apr 26 05:49:48 Starting unverified/sexpr-bootstrap/x64/64
Apr 26 05:56:52 Finished unverified/sexpr-bootstrap/x64/64                     7m03s   2GB
Apr 26 05:56:52 Starting unverified/sexpr-bootstrap/x64/32
Apr 26 06:01:40 Finished unverified/sexpr-bootstrap/x64/32                     4m46s   6GB
Apr 26 06:01:40 Starting compiler/benchmarks
Apr 26 06:01:47 Finished compiler/benchmarks                                      6s  23MB
Apr 26 06:01:47 Starting compiler/bootstrap/compilation/x64/64
Apr 26 16:18:29 Finished compiler/bootstrap/compilation/x64/64             10h16m40s  64GB
Apr 26 16:18:29 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 26 16:22:56 Finished compiler/bootstrap/compilation/x64/64/proofs          4m27s   6GB
Apr 26 16:22:57 Starting compiler/bootstrap/compilation/x64/32
Apr 27 01:34:43 Finished compiler/bootstrap/compilation/x64/32              9h11m45s  64GB
Apr 27 01:34:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 27 01:37:41 Finished compiler/bootstrap/compilation/x64/32/proofs          2m57s   5GB
Apr 27 01:37:41 Starting compiler/bootstrap/compilation/ag32/32
Apr 27 11:25:24 Finished compiler/bootstrap/compilation/ag32/32             9h47m41s  64GB
Apr 27 11:25:24 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 27 11:55:02 Finished compiler/bootstrap/compilation/ag32/32/proofs        29m37s  15GB
Apr 27 11:55:02 SUCCESS