Job 1879

CakeML:4c966fba47c4550a982b3512dc6a08cc1ee4f7da
  Translate new mlmap functions [Apr 12 08:48:57]
#881 (mlmap-additions)
Merging into:c2be5d64270ec1538eded2eed51612b7708c5d50
  Merge pull request #872 from talsewell/printing-type-check-each-dec [Apr 26 09:47:56]
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
  Fix some overlong lines [Apr 20 03:46:17]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 26 21:00:17 Claimed job
Apr 26 21:00:19 Reusing HOL
Apr 26 21:01:00 Starting developers
Apr 26 21:01:05 Finished developers                                               4s 129MB
Apr 26 21:01:05 Starting developers/bin
Apr 26 21:01:15 Finished developers/bin                                           9s   1GB
Apr 26 21:01:15 Starting semantics/ffi
Apr 26 21:01:31 Finished semantics/ffi                                           15s 192MB
Apr 26 21:01:31 Starting semantics
Apr 26 21:03:58 Finished semantics                                             2m26s   1GB
Apr 26 21:03:58 Starting semantics/proofs
Apr 26 21:09:55 Finished semantics/proofs                                      5m56s   1GB
Apr 26 21:09:55 Starting semantics/alt_semantics
Apr 26 21:10:23 Finished semantics/alt_semantics                                 27s 480MB
Apr 26 21:10:23 Starting semantics/alt_semantics/proofs
Apr 26 21:14:22 Finished semantics/alt_semantics/proofs                        3m58s 654MB
Apr 26 21:14:22 Starting basis/pure
Apr 26 21:15:48 Finished basis/pure                                            1m25s 687MB
Apr 26 21:15:48 Starting translator
Apr 26 21:19:54 Finished translator                                            4m05s 958MB
Apr 26 21:19:54 Starting compiler/parsing
Apr 26 21:21:41 Finished compiler/parsing                                      1m46s 738MB
Apr 26 21:21:41 Starting characteristic
Apr 26 21:31:00 Finished characteristic                                        9m19s 786MB
Apr 26 21:31:00 Starting translator/monadic
Apr 26 21:34:16 Finished translator/monadic                                    3m15s 569MB
Apr 26 21:34:16 Starting basis
Apr 26 22:40:38 Finished basis                                              1h06m20s   2GB
Apr 26 22:40:38 Starting compiler/inference
Apr 26 22:42:20 Finished compiler/inference                                    1m41s   1GB
Apr 26 22:42:20 Starting compiler/backend/reg_alloc
Apr 26 22:44:39 Finished compiler/backend/reg_alloc                            2m18s 441MB
Apr 26 22:44:39 Starting compiler/backend/gc
Apr 26 22:50:36 Finished compiler/backend/gc                                   5m56s   1GB
Apr 26 22:50:36 Starting compiler/backend
Apr 26 22:58:38 Finished compiler/backend                                      8m02s   1GB
Apr 26 22:58:38 Starting compiler/encoders/asm
Apr 26 22:59:19 Finished compiler/encoders/asm                                   40s 449MB
Apr 26 22:59:19 Starting compiler/encoders/x64
Apr 26 23:00:43 Finished compiler/encoders/x64                                 1m22s 619MB
Apr 26 23:00:43 Starting compiler/encoders/arm7
Apr 26 23:03:28 Finished compiler/encoders/arm7                                2m43s 959MB
Apr 26 23:03:28 Starting compiler/encoders/arm8
Apr 26 23:04:24 Finished compiler/encoders/arm8                                  55s 810MB
Apr 26 23:04:24 Starting compiler/encoders/arm8_asl
Apr 27 02:01:41 Finished compiler/encoders/arm8_asl                         2h57m16s   9GB
Apr 27 02:01:41 Starting compiler/encoders/mips
Apr 27 02:03:36 Finished compiler/encoders/mips                                1m54s   1GB
Apr 27 02:03:36 Starting compiler/encoders/riscv
Apr 27 02:05:54 Finished compiler/encoders/riscv                               2m16s   1GB
Apr 27 02:05:54 Starting compiler/encoders/ag32
Apr 27 02:06:22 Finished compiler/encoders/ag32                                  27s 838MB
Apr 27 02:06:22 Starting compiler/backend/x64
Apr 27 02:06:57 Finished compiler/backend/x64                                    34s 690MB
Apr 27 02:06:58 Starting compiler/backend/arm7
Apr 27 02:07:25 Finished compiler/backend/arm7                                   27s   1GB
Apr 27 02:07:26 Starting compiler/backend/arm8
Apr 27 02:07:58 Finished compiler/backend/arm8                                   31s 744MB
Apr 27 02:07:58 Starting compiler/backend/mips
Apr 27 02:08:23 Finished compiler/backend/mips                                   25s   1GB
Apr 27 02:08:23 Starting compiler/backend/riscv
Apr 27 02:08:54 Finished compiler/backend/riscv                                  29s 715MB
Apr 27 02:08:54 Starting compiler/backend/ag32
Apr 27 02:10:37 Finished compiler/backend/ag32                                 1m42s   1GB
Apr 27 02:10:38 Starting compiler/parsing/proofs
Apr 27 02:15:41 Finished compiler/parsing/proofs                               5m03s 684MB
Apr 27 02:15:41 Starting compiler/inference/proofs
Apr 27 02:18:44 Finished compiler/inference/proofs                             3m02s   1GB
Apr 27 02:18:44 Starting compiler/backend/semantics
Apr 27 02:59:36 Finished compiler/backend/semantics                           40m51s 791MB
Apr 27 02:59:36 Starting compiler/backend/reg_alloc/proofs
Apr 27 03:03:52 Finished compiler/backend/reg_alloc/proofs                     4m15s 881MB
Apr 27 03:03:52 Starting compiler/backend/proofs
Apr 27 04:19:46 Finished compiler/backend/proofs                            1h15m51s   5GB
Apr 27 04:19:46 Starting compiler/backend/serialiser
Apr 27 04:21:58 Finished compiler/backend/serialiser                           2m11s 907MB
Apr 27 04:21:58 Starting compiler/encoders/x64/proofs
Apr 27 04:34:59 Finished compiler/encoders/x64/proofs                         13m01s   1GB
Apr 27 04:35:00 Starting compiler/encoders/arm7/proofs
Apr 27 04:51:56 Finished compiler/encoders/arm7/proofs                        16m55s   1GB
Apr 27 04:51:56 Starting compiler/encoders/arm8/proofs
Apr 27 05:00:16 Finished compiler/encoders/arm8/proofs                         8m20s 825MB
Apr 27 05:00:17 Starting compiler/encoders/arm8_asl/proofs
Apr 27 06:02:23 Finished compiler/encoders/arm8_asl/proofs                  1h02m05s   2GB
Apr 27 06:02:23 Starting compiler/encoders/mips/proofs
Apr 27 06:14:46 Finished compiler/encoders/mips/proofs                        12m22s   1GB
Apr 27 06:14:46 Starting compiler/encoders/riscv/proofs
Apr 27 06:25:39 Finished compiler/encoders/riscv/proofs                       10m52s 597MB
Apr 27 06:25:39 Starting compiler/encoders/ag32/proofs
Apr 27 06:28:50 Finished compiler/encoders/ag32/proofs                         3m11s 519MB
Apr 27 06:28:50 Starting compiler/backend/x64/proofs
Apr 27 06:29:37 Finished compiler/backend/x64/proofs                             46s 871MB
Apr 27 06:29:38 Starting compiler/backend/arm7/proofs
Apr 27 06:30:20 Finished compiler/backend/arm7/proofs                            42s   1GB
Apr 27 06:30:21 Starting compiler/backend/arm8/proofs
Apr 27 06:30:53 Finished compiler/backend/arm8/proofs                            32s   1GB
Apr 27 06:30:54 Starting compiler/backend/arm8_asl
Apr 27 06:31:38 Finished compiler/backend/arm8_asl                               44s 821MB
Apr 27 06:31:39 Starting compiler/backend/mips/proofs
Apr 27 06:32:24 Finished compiler/backend/mips/proofs                            45s 834MB
Apr 27 06:32:25 Starting compiler/backend/riscv/proofs
Apr 27 06:33:14 Finished compiler/backend/riscv/proofs                           49s 996MB
Apr 27 06:33:14 Starting compiler/backend/ag32/proofs
Apr 27 06:50:06 Finished compiler/backend/ag32/proofs                         16m51s   1GB
Apr 27 06:50:06 Starting compiler/proofs
Apr 27 06:53:46 Finished compiler/proofs                                       3m39s   1GB
Apr 27 06:53:46 Starting candle/set-theory
Apr 27 06:54:27 Finished candle/set-theory                                       40s 983MB
Apr 27 06:54:27 Starting candle/syntax-lib
Apr 27 06:54:43 Finished candle/syntax-lib                                       15s 650MB
Apr 27 06:54:43 Starting candle/standard/syntax
Apr 27 06:57:10 Finished candle/standard/syntax                                2m26s 970MB
Apr 27 06:57:10 Starting candle/standard/semantics
Apr 27 06:59:32 Finished candle/standard/semantics                             2m21s   1GB
Apr 27 06:59:32 Starting candle/standard/monadic
Apr 27 07:01:47 Finished candle/standard/monadic                               2m14s   1GB
Apr 27 07:01:47 Starting candle/standard/ml_kernel
Apr 27 07:10:35 Finished candle/standard/ml_kernel                             8m45s   1GB
Apr 27 07:10:35 Starting candle/overloading/syntax
Apr 27 07:14:34 Finished candle/overloading/syntax                             3m58s 599MB
Apr 27 07:14:34 Starting candle/overloading/semantics
Apr 27 07:29:04 Finished candle/overloading/semantics                         14m29s   1GB
Apr 27 07:29:04 Starting candle/overloading/monadic
Apr 27 07:32:29 Finished candle/overloading/monadic                            3m24s 388MB
Apr 27 07:32:29 Starting candle/overloading/ml_kernel
Apr 27 07:43:36 Finished candle/overloading/ml_kernel                         11m06s   1GB
Apr 27 07:43:36 Starting candle/overloading/ml_checker
Apr 27 07:47:00 Finished candle/overloading/ml_checker                         3m23s   1GB
Apr 27 07:47:00 Starting candle/prover
Apr 27 08:00:45 Finished candle/prover                                        13m44s   1GB
Apr 27 08:00:46 Starting pancake
Apr 27 08:05:41 Finished pancake                                               4m54s   1GB
Apr 27 08:05:41 Starting pancake/ffi
Apr 27 08:05:42 Finished pancake/ffi                                              0s  12MB
Apr 27 08:05:42 Starting pancake/semantics
Apr 27 08:08:51 Finished pancake/semantics                                     3m09s 860MB
Apr 27 08:08:52 Starting pancake/proofs
Apr 27 08:25:33 Finished pancake/proofs                                       16m40s   2GB
Apr 27 08:25:33 Starting characteristic/examples
Apr 27 08:27:39 Finished characteristic/examples                               2m06s 905MB
Apr 27 08:27:39 Starting tutorial/solutions
Apr 27 08:51:49 Finished tutorial/solutions                                   24m08s   2GB
Apr 27 08:51:49 Starting translator/monadic/examples
Apr 27 08:57:27 Finished translator/monadic/examples                           5m37s   1GB
Apr 27 08:57:27 Starting examples
Apr 27 09:12:58 Finished examples                                             15m30s   1GB
Apr 27 09:12:58 Starting examples/compilation/x64
Apr 27 12:50:57 Finished examples/compilation/x64                           3h37m58s   3GB
Apr 27 12:50:57 Starting examples/compilation/x64/proofs
Apr 27 12:55:23 Finished examples/compilation/x64/proofs                       4m25s   2GB
Apr 27 12:55:23 Starting examples/compilation/ag32
Apr 27 13:49:36 Finished examples/compilation/ag32                            54m12s   2GB
Apr 27 13:49:36 Starting examples/compilation/ag32/proofs
Apr 27 13:51:32 Finished examples/compilation/ag32/proofs                      1m55s   1GB
Apr 27 13:51:33 Starting examples/cost
Apr 27 15:13:30 Finished examples/cost                                      1h21m56s   2GB
Apr 27 15:13:30 Starting examples/lpr_checker
Apr 27 15:14:45 Finished examples/lpr_checker                                  1m15s   1GB
Apr 27 15:14:45 Starting examples/lpr_checker/array
Apr 27 15:51:20 Finished examples/lpr_checker/array                           36m34s   1GB
Apr 27 15:51:20 Starting examples/lpr_checker/array/compilation
Apr 27 18:03:07 Finished examples/lpr_checker/array/compilation             2h11m46s   6GB
Apr 27 18:03:07 Starting examples/lpr_checker/array/compilation/proofs
Apr 27 18:06:06 Finished examples/lpr_checker/array/compilation/proofs         2m58s   2GB
Apr 27 18:06:06 Starting examples/opentheory
Apr 27 18:19:16 Finished examples/opentheory                                  13m09s   2GB
Apr 27 18:19:16 Starting examples/opentheory
Apr 27 18:19:18 Finished examples/opentheory                                      1s  19MB
Apr 27 18:19:18 Starting examples/opentheory/compilation
Apr 27 19:26:47 Finished examples/opentheory/compilation                    1h07m28s   3GB
Apr 27 19:26:47 Starting examples/opentheory/compilation/proofs
Apr 27 19:28:57 Finished examples/opentheory/compilation/proofs                2m09s   2GB
Apr 27 19:28:57 Starting examples/opentheory/compilation/ag32
Apr 27 20:33:59 Finished examples/opentheory/compilation/ag32               1h04m58s   3GB
Apr 27 20:33:59 Starting examples/opentheory/compilation/ag32/proofs Apr 27 20:33:59 139s