Job 721

CakeML:6bc8e267ebd128227cd90e1c9f9be4fd7f3bbb5a
  Merge remote-tracking branch 'origin/cleanup' [Feb 06 09:47:42]
HOL:08a51fee676681dadabae53e90963868e9720563
  Implement mllex-driven lexing for Theory.dat files [Feb 06 06:13:12]
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

Feb 07 17:30:02 Claimed job
Feb 07 17:30:14 Reusing HOL
Feb 07 17:31:08 Starting developers
Feb 07 17:31:11 Finished developers                                               2s  19MB
Feb 07 17:31:12 Starting developers/bin
Feb 07 17:32:27 Finished developers/bin                                        1m14s 918MB
Feb 07 17:32:28 Starting semantics/ffi
Feb 07 17:32:38 Finished semantics/ffi                                            9s 221MB
Feb 07 17:32:39 Starting semantics
Feb 07 17:34:00 Finished semantics                                             1m20s   1GB
Feb 07 17:34:01 Starting semantics/proofs
Feb 07 17:37:12 Finished semantics/proofs                                      3m10s   1GB
Feb 07 17:37:12 Starting basis/pure
Feb 07 17:38:00 Finished basis/pure                                              47s 700MB
Feb 07 17:38:01 Starting translator
Feb 07 17:39:41 Finished translator                                            1m40s   1GB
Feb 07 17:39:42 Starting compiler/parsing
Feb 07 17:40:40 Finished compiler/parsing                                        57s   1GB
Feb 07 17:40:40 Starting characteristic
Feb 07 17:45:01 Finished characteristic                                        4m19s   1GB
Feb 07 17:45:02 Starting translator/monadic
Feb 07 17:46:29 Finished translator/monadic                                    1m27s   1GB
Feb 07 17:46:30 Starting basis
Feb 07 18:02:54 Finished basis                                                16m23s   2GB
Feb 07 18:02:55 Starting compiler/inference
Feb 07 18:04:27 Finished compiler/inference                                    1m32s   1GB
Feb 07 18:04:28 Starting compiler/backend/reg_alloc
Feb 07 18:05:21 Finished compiler/backend/reg_alloc                              51s   1GB
Feb 07 18:05:21 Starting compiler/backend/gc
Feb 07 18:13:11 Finished compiler/backend/gc                                   7m49s   1GB
Feb 07 18:13:12 Starting compiler/backend
Feb 07 18:13:15 Finished compiler/backend                                         2s  18MB
Feb 07 18:13:16 Starting compiler/encoders/asm
Feb 07 18:13:18 Finished compiler/encoders/asm                                    1s  14MB
Feb 07 18:13:18 Starting compiler/encoders/x64
Feb 07 18:13:43 Finished compiler/encoders/x64                                   24s 747MB
Feb 07 18:13:44 Starting compiler/encoders/arm6
Feb 07 18:14:29 Finished compiler/encoders/arm6                                  44s 730MB
Feb 07 18:14:30 Starting compiler/encoders/arm8
Feb 07 18:14:43 Finished compiler/encoders/arm8                                  13s 868MB
Feb 07 18:14:44 Starting compiler/encoders/mips
Feb 07 18:15:02 Finished compiler/encoders/mips                                  17s   1GB
Feb 07 18:15:02 Starting compiler/encoders/riscv
Feb 07 18:15:17 Finished compiler/encoders/riscv                                 14s 702MB
Feb 07 18:15:18 Starting compiler/encoders/ag32
Feb 07 18:15:36 Finished compiler/encoders/ag32                                  16s 616MB
Feb 07 18:15:36 Starting compiler/backend/x64
Feb 07 18:15:55 Finished compiler/backend/x64                                    18s   1GB
Feb 07 18:15:56 Starting compiler/backend/arm6
Feb 07 18:16:15 Finished compiler/backend/arm6                                   18s 974MB
Feb 07 18:16:16 Starting compiler/backend/arm8
Feb 07 18:16:34 Finished compiler/backend/arm8                                   18s   1GB
Feb 07 18:16:35 Starting compiler/backend/mips
Feb 07 18:16:54 Finished compiler/backend/mips                                   18s   1GB
Feb 07 18:16:55 Starting compiler/backend/riscv
Feb 07 18:17:13 Finished compiler/backend/riscv                                  17s   1GB
Feb 07 18:17:14 Starting compiler/backend/ag32
Feb 07 18:18:19 Finished compiler/backend/ag32                                 1m05s   1GB
Feb 07 18:18:20 Starting compiler/parsing/proofs
Feb 07 18:23:50 Finished compiler/parsing/proofs                               5m29s 959MB
Feb 07 18:23:50 Starting compiler/inference/proofs
Feb 07 18:26:31 Finished compiler/inference/proofs                             2m39s   1GB
Feb 07 18:26:31 Starting compiler/backend/semantics
Feb 07 18:33:22 Finished compiler/backend/semantics                            6m49s   1GB
Feb 07 18:33:22 Starting compiler/backend/reg_alloc/proofs
Feb 07 18:35:55 Finished compiler/backend/reg_alloc/proofs                     2m32s   1GB
Feb 07 18:35:56 Starting compiler/backend/proofs
Feb 07 19:11:54 Finished compiler/backend/proofs                              35m57s   3GB
Feb 07 19:11:55 Starting compiler/encoders/x64/proofs
Feb 07 19:20:52 Finished compiler/encoders/x64/proofs                          8m55s   4GB
Feb 07 19:20:52 Starting compiler/encoders/arm6/proofs
Feb 07 19:33:01 Finished compiler/encoders/arm6/proofs                        12m07s   3GB
Feb 07 19:33:01 Starting compiler/encoders/arm8/proofs
Feb 07 19:38:23 Finished compiler/encoders/arm8/proofs                         5m21s   1GB
Feb 07 19:38:24 Starting compiler/encoders/mips/proofs
Feb 07 19:47:42 Finished compiler/encoders/mips/proofs                         9m18s   2GB
Feb 07 19:47:43 Starting compiler/encoders/riscv/proofs
Feb 07 19:55:11 Finished compiler/encoders/riscv/proofs                        7m27s   1GB
Feb 07 19:55:11 Starting compiler/encoders/ag32/proofs
Feb 07 19:57:37 Finished compiler/encoders/ag32/proofs                         2m25s 662MB
Feb 07 19:57:38 Starting compiler/backend/x64/proofs
Feb 07 19:57:58 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 07 19:57:59 Starting compiler/backend/arm6/proofs
Feb 07 19:58:21 Finished compiler/backend/arm6/proofs                            21s   1GB
Feb 07 19:58:22 Starting compiler/backend/arm8/proofs
Feb 07 19:58:43 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 07 19:58:43 Starting compiler/backend/mips/proofs
Feb 07 19:59:04 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 07 19:59:05 Starting compiler/backend/riscv/proofs
Feb 07 19:59:26 Finished compiler/backend/riscv/proofs                           20s   1GB
Feb 07 19:59:26 Starting compiler/backend/ag32/proofs
Feb 07 20:07:52 Finished compiler/backend/ag32/proofs                          8m25s   3GB
Feb 07 20:07:53 Starting compiler/proofs
Feb 07 20:09:19 Finished compiler/proofs                                       1m25s   3GB
Feb 07 20:09:20 Starting candle/set-theory
Feb 07 20:09:47 Finished candle/set-theory                                       26s 674MB
Feb 07 20:09:48 Starting candle/syntax-lib
Feb 07 20:09:59 Finished candle/syntax-lib                                       10s 687MB
Feb 07 20:10:00 Starting candle/standard/syntax
Feb 07 20:11:42 Finished candle/standard/syntax                                1m42s   1GB
Feb 07 20:11:43 Starting candle/standard/semantics
Feb 07 20:13:19 Finished candle/standard/semantics                             1m35s   1GB
Feb 07 20:13:20 Starting candle/standard/monadic
Feb 07 20:14:52 Finished candle/standard/monadic                               1m31s   1GB
Feb 07 20:14:53 Starting candle/standard/ml_kernel
Feb 07 20:18:37 Finished candle/standard/ml_kernel                             3m43s   3GB
Feb 07 20:18:38 Starting candle/standard/opentheory
Feb 07 20:27:01 Finished candle/standard/opentheory                            8m22s   4GB
Feb 07 20:27:02 Starting candle/standard/opentheory/compilation
Feb 07 20:55:41 Finished candle/standard/opentheory/compilation               28m38s  25GB
Feb 07 20:55:41 Starting candle/standard/opentheory/compilation/proofs
Feb 07 20:56:26 Finished candle/standard/opentheory/compilation/proofs           43s   4GB
Feb 07 20:56:26 Starting characteristic/examples
Feb 07 20:57:53 Finished characteristic/examples                               1m26s   2GB
Feb 07 20:57:54 Starting tutorial/solutions
Feb 07 21:11:07 Finished tutorial/solutions                                   13m13s   6GB
Feb 07 21:11:08 Starting translator/monadic/examples
Feb 07 21:13:22 Finished translator/monadic/examples                           2m13s   2GB
Feb 07 21:13:23 Starting examples
Feb 07 21:21:00 Finished examples                                              7m36s   3GB
Feb 07 21:21:01 Starting examples/compilation/x64
Feb 07 23:15:42 Finished examples/compilation/x64                           1h54m40s   9GB
Feb 07 23:15:42 Starting examples/compilation/x64/proofs
Feb 07 23:17:30 Finished examples/compilation/x64/proofs                       1m46s   5GB
Feb 07 23:17:31 Starting examples/compilation/ag32
Feb 07 23:45:17 Finished examples/compilation/ag32                            27m45s   6GB
Feb 07 23:45:17 Starting examples/compilation/ag32/proofs
Feb 07 23:46:06 Finished examples/compilation/ag32/proofs                        48s   4GB
Feb 07 23:46:07 Starting translator/okasaki-examples
Feb 07 23:50:10 Finished translator/okasaki-examples                           4m03s   1GB
Feb 07 23:50:11 Starting translator/other-examples
Feb 07 23:50:55 Finished translator/other-examples                               42s   1GB
Feb 07 23:50:55 Starting compiler/parsing/tests
Feb 07 23:51:22 Finished compiler/parsing/tests                                  25s 611MB
Feb 07 23:51:23 Starting compiler/inference/tests
Feb 07 23:55:24 Finished compiler/inference/tests                              4m00s   3GB
Feb 07 23:55:24 Starting compiler/bootstrap/translation
Feb 08 02:20:56 Finished compiler/bootstrap/translation                     2h25m31s  50GB
Feb 08 02:20:57 Starting unverified/sexpr-bootstrap/x64/64
Feb 08 02:29:45 Finished unverified/sexpr-bootstrap/x64/64                     8m45s  15GB
Feb 08 02:29:45 Starting unverified/sexpr-bootstrap/x64/32
Feb 08 02:35:01 Finished unverified/sexpr-bootstrap/x64/32                     5m14s  22GB
Feb 08 02:35:02 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 08 02:35:35 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            31s   1GB
Feb 08 02:35:35 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 08 02:36:24 Finished compiler/benchmarks/mlton_benchmarks/cakeml             48s   1GB
Feb 08 02:36:25 Starting compiler/bootstrap/compilation/x64/64
Feb 08 12:44:57 Finished compiler/bootstrap/compilation/x64/64             10h08m30s  64GB
Feb 08 12:44:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 08 12:51:36 Finished compiler/bootstrap/compilation/x64/64/proofs          6m37s  31GB
Feb 08 12:51:37 Starting compiler/bootstrap/compilation/x64/32
Feb 08 21:52:03 Finished compiler/bootstrap/compilation/x64/32              9h00m24s  64GB
Feb 08 21:52:03 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 08 21:58:18 Finished compiler/bootstrap/compilation/x64/32/proofs          6m14s  32GB
Feb 08 21:58:19 SUCCESS