Job 714

CakeML:1088d0f2956d24e224dd3041806ec59df0060606
  Fix exception-of occurrences in compiler/benchmarks/mlton_benchmarks/ [Feb 03 04:18:30]
#613 (gh611)
Merging into:2d7c75fa02a5b1347dd76fa2b7150e0af74d940b
  Fix some uses of Theorem syntax [Jan 31 16:15:24]
HOL:84a78371f3039405c39422eabe0fea18c497b2c7
  Fix type signature of mp_then in Docfile [Feb 01 09:40:28]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 03 09:16:20 Claimed job
Feb 03 09:16:46 Building HOL
Feb 03 09:25:49 Starting developers
Feb 03 09:25:52 Finished developers                                               2s  20MB
Feb 03 09:25:52 Starting developers/bin
Feb 03 09:27:03 Finished developers/bin                                        1m09s 918MB
Feb 03 09:27:03 Starting semantics/ffi
Feb 03 09:27:42 Finished semantics/ffi                                           37s 570MB
Feb 03 09:27:43 Starting semantics
Feb 03 09:29:18 Finished semantics                                             1m35s   1GB
Feb 03 09:29:19 Starting semantics/proofs
Feb 03 09:32:29 Finished semantics/proofs                                      3m09s   1GB
Feb 03 09:32:30 Starting basis/pure
Feb 03 09:36:02 Finished basis/pure                                            3m31s 766MB
Feb 03 09:36:02 Starting translator
Feb 03 09:37:43 Finished translator                                            1m39s   1GB
Feb 03 09:37:43 Starting compiler/parsing
Feb 03 09:38:42 Finished compiler/parsing                                        58s   2GB
Feb 03 09:38:43 Starting characteristic
Feb 03 09:43:04 Finished characteristic                                        4m20s   1GB
Feb 03 09:43:05 Starting translator/monadic
Feb 03 09:44:33 Finished translator/monadic                                    1m27s   1GB
Feb 03 09:44:34 Starting basis
Feb 03 10:00:36 Finished basis                                                16m00s   3GB
Feb 03 10:00:36 Starting compiler/inference
Feb 03 10:02:27 Finished compiler/inference                                    1m49s   1GB
Feb 03 10:02:27 Starting compiler/backend/reg_alloc
Feb 03 10:03:19 Finished compiler/backend/reg_alloc                              51s   1GB
Feb 03 10:03:20 Starting compiler/backend/gc
Feb 03 10:12:14 Finished compiler/backend/gc                                   8m53s   2GB
Feb 03 10:12:14 Starting compiler/backend
Feb 03 10:12:18 Finished compiler/backend                                         2s  17MB
Feb 03 10:12:18 Starting compiler/encoders/asm
Feb 03 10:12:20 Finished compiler/encoders/asm                                    1s  19MB
Feb 03 10:12:21 Starting compiler/encoders/x64
Feb 03 10:13:22 Finished compiler/encoders/x64                                 1m00s 691MB
Feb 03 10:13:23 Starting compiler/encoders/arm6
Feb 03 10:15:07 Finished compiler/encoders/arm6                                1m44s   1GB
Feb 03 10:15:08 Starting compiler/encoders/arm8
Feb 03 10:15:40 Finished compiler/encoders/arm8                                  31s 818MB
Feb 03 10:15:41 Starting compiler/encoders/mips
Feb 03 10:16:47 Finished compiler/encoders/mips                                1m05s   1GB
Feb 03 10:16:47 Starting compiler/encoders/riscv
Feb 03 10:17:54 Finished compiler/encoders/riscv                               1m05s 945MB
Feb 03 10:17:54 Starting compiler/encoders/ag32
Feb 03 10:18:12 Finished compiler/encoders/ag32                                  17s 777MB
Feb 03 10:18:13 Starting compiler/backend/x64
Feb 03 10:18:32 Finished compiler/backend/x64                                    18s   1GB
Feb 03 10:18:33 Starting compiler/backend/arm6
Feb 03 10:18:52 Finished compiler/backend/arm6                                   18s   1GB
Feb 03 10:18:52 Starting compiler/backend/arm8
Feb 03 10:19:11 Finished compiler/backend/arm8                                   18s   1GB
Feb 03 10:19:12 Starting compiler/backend/mips
Feb 03 10:19:31 Finished compiler/backend/mips                                   19s   1GB
Feb 03 10:19:32 Starting compiler/backend/riscv
Feb 03 10:19:51 Finished compiler/backend/riscv                                  18s   1GB
Feb 03 10:19:52 Starting compiler/backend/ag32
Feb 03 10:20:59 Finished compiler/backend/ag32                                 1m06s   1GB
Feb 03 10:21:00 Starting compiler/parsing/proofs
Feb 03 10:26:38 Finished compiler/parsing/proofs                               5m38s   1GB
Feb 03 10:26:39 Starting compiler/inference/proofs
Feb 03 10:29:19 Finished compiler/inference/proofs                             2m39s   1GB
Feb 03 10:29:20 Starting compiler/backend/semantics
Feb 03 10:36:09 Finished compiler/backend/semantics                            6m48s   1GB
Feb 03 10:36:09 Starting compiler/backend/reg_alloc/proofs
Feb 03 10:38:44 Finished compiler/backend/reg_alloc/proofs                     2m34s 800MB
Feb 03 10:38:45 Starting compiler/backend/proofs
Feb 03 11:14:44 Finished compiler/backend/proofs                              35m58s   3GB
Feb 03 11:14:45 Starting compiler/encoders/x64/proofs
Feb 03 11:24:40 Finished compiler/encoders/x64/proofs                          9m54s   4GB
Feb 03 11:24:40 Starting compiler/encoders/arm6/proofs
Feb 03 11:37:42 Finished compiler/encoders/arm6/proofs                        13m01s   6GB
Feb 03 11:37:43 Starting compiler/encoders/arm8/proofs
Feb 03 11:43:21 Finished compiler/encoders/arm8/proofs                         5m37s   1GB
Feb 03 11:43:22 Starting compiler/encoders/mips/proofs
Feb 03 11:53:15 Finished compiler/encoders/mips/proofs                         9m52s   1GB
Feb 03 11:53:15 Starting compiler/encoders/riscv/proofs
Feb 03 12:00:50 Finished compiler/encoders/riscv/proofs                        7m33s   1GB
Feb 03 12:00:50 Starting compiler/encoders/ag32/proofs
Feb 03 12:03:17 Finished compiler/encoders/ag32/proofs                         2m26s 656MB
Feb 03 12:03:18 Starting compiler/backend/x64/proofs
Feb 03 12:03:38 Finished compiler/backend/x64/proofs                             19s 860MB
Feb 03 12:03:38 Starting compiler/backend/arm6/proofs
Feb 03 12:04:00 Finished compiler/backend/arm6/proofs                            21s 948MB
Feb 03 12:04:01 Starting compiler/backend/arm8/proofs
Feb 03 12:04:20 Finished compiler/backend/arm8/proofs                            18s 825MB
Feb 03 12:04:21 Starting compiler/backend/mips/proofs
Feb 03 12:04:41 Finished compiler/backend/mips/proofs                            19s 930MB
Feb 03 12:04:42 Starting compiler/backend/riscv/proofs
Feb 03 12:05:02 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 03 12:05:03 Starting compiler/backend/ag32/proofs
Feb 03 12:13:40 Finished compiler/backend/ag32/proofs                          8m36s   2GB
Feb 03 12:13:41 Starting compiler/proofs
Feb 03 12:15:03 Finished compiler/proofs                                       1m21s   3GB
Feb 03 12:15:04 Starting candle/set-theory
Feb 03 12:15:32 Finished candle/set-theory                                       27s 775MB
Feb 03 12:15:32 Starting candle/syntax-lib
Feb 03 12:15:44 Finished candle/syntax-lib                                       11s 511MB
Feb 03 12:15:45 Starting candle/standard/syntax
Feb 03 12:17:30 Finished candle/standard/syntax                                1m44s   1GB
Feb 03 12:17:30 Starting candle/standard/semantics
Feb 03 12:19:07 Finished candle/standard/semantics                             1m36s   1GB
Feb 03 12:19:08 Starting candle/standard/monadic
Feb 03 12:20:39 Finished candle/standard/monadic                               1m30s   1GB
Feb 03 12:20:39 Starting candle/standard/ml_kernel
Feb 03 12:24:27 Finished candle/standard/ml_kernel                             3m46s   3GB
Feb 03 12:24:27 Starting candle/standard/opentheory
Feb 03 12:32:52 Finished candle/standard/opentheory                            8m23s   3GB
Feb 03 12:32:52 Starting candle/standard/opentheory/compilation
Feb 03 13:01:32 Finished candle/standard/opentheory/compilation               28m39s  24GB
Feb 03 13:01:33 Starting candle/standard/opentheory/compilation/proofs
Feb 03 13:02:18 Finished candle/standard/opentheory/compilation/proofs           44s   4GB
Feb 03 13:02:19 Starting characteristic/examples
Feb 03 13:03:49 Finished characteristic/examples                               1m29s   3GB
Feb 03 13:03:49 Starting tutorial/solutions
Feb 03 13:17:01 Finished tutorial/solutions                                   13m10s   6GB
Feb 03 13:17:01 Starting translator/monadic/examples
Feb 03 13:19:16 Finished translator/monadic/examples                           2m13s   2GB
Feb 03 13:19:16 Starting examples
Feb 03 13:26:53 Finished examples                                              7m36s   5GB
Feb 03 13:26:54 Starting examples/compilation/x64
Feb 03 15:17:58 Finished examples/compilation/x64                           1h51m02s  10GB
Feb 03 15:17:58 Starting examples/compilation/x64/proofs
Feb 03 15:19:46 Finished examples/compilation/x64/proofs                       1m47s   4GB
Feb 03 15:19:47 Starting examples/compilation/ag32
Feb 03 15:47:20 Finished examples/compilation/ag32                            27m32s   5GB
Feb 03 15:47:21 Starting examples/compilation/ag32/proofs
Feb 03 15:48:10 Finished examples/compilation/ag32/proofs                        48s   4GB
Feb 03 15:48:11 Starting translator/okasaki-examples
Feb 03 15:52:16 Finished translator/okasaki-examples                           4m05s   1GB
Feb 03 15:52:17 Starting translator/other-examples
Feb 03 15:55:51 Finished translator/other-examples                             3m33s   1GB
Feb 03 15:55:52 Starting compiler/parsing/tests
Feb 03 15:56:19 Finished compiler/parsing/tests                                  26s 577MB
Feb 03 15:56:19 Starting compiler/inference/tests
Feb 03 16:00:19 Finished compiler/inference/tests                              3m58s   4GB
Feb 03 16:00:19 Starting compiler/bootstrap/translation
Feb 03 18:25:13 Finished compiler/bootstrap/translation                     2h24m52s  46GB
Feb 03 18:25:14 Starting unverified/sexpr-bootstrap/x64/64
Feb 03 18:33:53 Finished unverified/sexpr-bootstrap/x64/64                     8m38s  14GB
Feb 03 18:33:54 Starting unverified/sexpr-bootstrap/x64/32
Feb 03 18:39:06 Finished unverified/sexpr-bootstrap/x64/32                     5m10s  19GB
Feb 03 18:39:06 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 03 18:39:39 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            31s   1GB
Feb 03 18:39:40 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 03 18:40:30 Finished compiler/benchmarks/mlton_benchmarks/cakeml             49s   1GB
Feb 03 18:40:30 Starting compiler/bootstrap/compilation/x64/64
Feb 04 05:24:01 Finished compiler/bootstrap/compilation/x64/64             10h43m29s  64GB
Feb 04 05:24:02 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 04 05:31:06 Finished compiler/bootstrap/compilation/x64/64/proofs          7m03s  35GB
Feb 04 05:31:07 Starting compiler/bootstrap/compilation/x64/32
Feb 04 14:50:20 Finished compiler/bootstrap/compilation/x64/32              9h19m12s  64GB
Feb 04 14:50:21 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 04 14:56:10 Finished compiler/bootstrap/compilation/x64/32/proofs          5m48s  27GB
Feb 04 14:56:11 SUCCESS