Job 1977

CakeML:9a04a0166f0c1b2fc7003674a540bbd8e086dced
  Move no_install definition to wordProps (placed with no_alloc) [Sep 06 01:33:40]
#907 (word_to_word_Pancake)
Merging into:1afd9c2ae712011d1edddfc51a00c38d36bbb43a
  Merge pull request #906 from CakeML/candle-features [Aug 25 05:11:25]
HOL:2639637652b5be738521f6efa56cbf8a10e52599
  Start to revise simplifier documentation to capture recent changes [Sep 06 07:08:33]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Sep 07 09:22:24 Claimed job
Sep 07 09:23:57 Building HOL
Sep 07 09:36:12 Starting developers
Sep 07 09:36:17 Finished developers                                               5s 112MB
Sep 07 09:36:17 Starting developers/bin
Sep 07 09:38:04 Finished developers/bin                                        1m46s   1GB
Sep 07 09:38:04 Starting semantics/ffi
Sep 07 09:38:14 Finished semantics/ffi                                            9s 221MB
Sep 07 09:38:14 Starting semantics
Sep 07 09:40:56 Finished semantics                                             2m42s   1GB
Sep 07 09:40:57 Starting semantics/proofs
Sep 07 09:50:05 Finished semantics/proofs                                      9m07s   1GB
Sep 07 09:50:05 Starting semantics/alt_semantics
Sep 07 09:50:33 Finished semantics/alt_semantics                                 27s 516MB
Sep 07 09:50:33 Starting semantics/alt_semantics/proofs
Sep 07 10:06:44 Finished semantics/alt_semantics/proofs                       16m11s   2GB
Sep 07 10:06:45 Starting basis/pure
Sep 07 10:10:35 Finished basis/pure                                            3m50s   1GB
Sep 07 10:10:35 Starting translator
Sep 07 10:18:28 Finished translator                                            7m52s   2GB
Sep 07 10:18:28 Starting compiler/parsing
Sep 07 10:20:03 Finished compiler/parsing                                      1m34s   4GB
Sep 07 10:20:03 Starting characteristic
Sep 07 10:27:28 Finished characteristic                                        7m24s   1GB
Sep 07 10:27:28 Starting translator/monadic
Sep 07 10:29:31 Finished translator/monadic                                    2m02s   1GB
Sep 07 10:29:31 Starting basis
Sep 07 11:24:46 Finished basis                                                55m15s  13GB
Sep 07 11:24:47 Starting compiler/inference
Sep 07 11:26:29 Finished compiler/inference                                    1m42s   1GB
Sep 07 11:26:29 Starting compiler/backend/reg_alloc
Sep 07 11:28:16 Finished compiler/backend/reg_alloc                            1m46s   1GB
Sep 07 11:28:16 Starting compiler/backend/gc
Sep 07 11:32:53 Finished compiler/backend/gc                                   4m37s   1GB
Sep 07 11:32:54 Starting compiler/backend
Sep 07 11:38:51 Finished compiler/backend                                      5m57s   2GB
Sep 07 11:38:51 Starting compiler/encoders/asm
Sep 07 11:39:22 Finished compiler/encoders/asm                                   30s 964MB
Sep 07 11:39:23 Starting compiler/encoders/x64
Sep 07 11:40:34 Finished compiler/encoders/x64                                 1m11s   1GB
Sep 07 11:40:34 Starting compiler/encoders/arm7
Sep 07 11:42:57 Finished compiler/encoders/arm7                                2m22s   1GB
Sep 07 11:42:57 Starting compiler/encoders/arm8
Sep 07 11:43:41 Finished compiler/encoders/arm8                                  43s   1GB
Sep 07 11:43:42 Starting compiler/encoders/arm8_asl
Sep 07 14:13:30 Finished compiler/encoders/arm8_asl                         2h29m48s  24GB
Sep 07 14:13:31 Starting compiler/encoders/mips
Sep 07 14:15:13 Finished compiler/encoders/mips                                1m42s   1GB
Sep 07 14:15:14 Starting compiler/encoders/riscv
Sep 07 14:17:15 Finished compiler/encoders/riscv                               2m01s   1GB
Sep 07 14:17:15 Starting compiler/encoders/ag32
Sep 07 14:17:37 Finished compiler/encoders/ag32                                  21s 914MB
Sep 07 14:17:37 Starting compiler/backend/x64
Sep 07 14:17:59 Finished compiler/backend/x64                                    21s   1GB
Sep 07 14:17:59 Starting compiler/backend/arm7
Sep 07 14:18:22 Finished compiler/backend/arm7                                   23s   1GB
Sep 07 14:18:23 Starting compiler/backend/arm8
Sep 07 14:18:45 Finished compiler/backend/arm8                                   22s   1GB
Sep 07 14:18:45 Starting compiler/backend/mips
Sep 07 14:19:08 Finished compiler/backend/mips                                   22s   1GB
Sep 07 14:19:08 Starting compiler/backend/riscv
Sep 07 14:19:31 Finished compiler/backend/riscv                                  22s   1GB
Sep 07 14:19:32 Starting compiler/backend/ag32
Sep 07 14:21:02 Finished compiler/backend/ag32                                 1m30s   1GB
Sep 07 14:21:02 Starting compiler/parsing/proofs
Sep 07 14:25:20 Finished compiler/parsing/proofs                               4m17s   1GB
Sep 07 14:25:21 Starting compiler/inference/proofs
Sep 07 14:28:20 Finished compiler/inference/proofs                             2m59s 912MB
Sep 07 14:28:21 Starting compiler/backend/semantics
Sep 07 14:58:58 Finished compiler/backend/semantics                           30m36s   3GB
Sep 07 14:58:58 Starting compiler/backend/reg_alloc/proofs
Sep 07 15:02:58 Finished compiler/backend/reg_alloc/proofs                     3m59s   1GB
Sep 07 15:02:58 Starting compiler/backend/proofs
Sep 07 16:45:23 Finished compiler/backend/proofs                            1h42m23s  15GB
Sep 07 16:45:23 Starting compiler/backend/serialiser
Sep 07 16:47:06 Finished compiler/backend/serialiser                           1m43s   2GB
Sep 07 16:47:06 Starting compiler/encoders/x64/proofs
Sep 07 16:57:40 Finished compiler/encoders/x64/proofs                         10m33s   4GB
Sep 07 16:57:40 Starting compiler/encoders/arm7/proofs
Sep 07 17:12:30 Finished compiler/encoders/arm7/proofs                        14m49s   3GB
Sep 07 17:12:31 Starting compiler/encoders/arm8/proofs
Sep 07 17:19:58 Finished compiler/encoders/arm8/proofs                         7m27s   1GB
Sep 07 17:19:59 Starting compiler/encoders/arm8_asl/proofs
Sep 07 18:16:37 Finished compiler/encoders/arm8_asl/proofs                    56m37s   9GB
Sep 07 18:16:37 Starting compiler/encoders/mips/proofs
Sep 07 18:27:43 Finished compiler/encoders/mips/proofs                        11m05s   2GB
Sep 07 18:27:43 Starting compiler/encoders/riscv/proofs
Sep 07 18:37:17 Finished compiler/encoders/riscv/proofs                        9m33s   1GB
Sep 07 18:37:17 Starting compiler/encoders/ag32/proofs
Sep 07 18:40:09 Finished compiler/encoders/ag32/proofs                         2m51s 830MB
Sep 07 18:40:09 Starting compiler/backend/x64/proofs
Sep 07 18:40:35 Finished compiler/backend/x64/proofs                             25s   1GB
Sep 07 18:40:35 Starting compiler/backend/arm7/proofs
Sep 07 18:41:02 Finished compiler/backend/arm7/proofs                            26s   1GB
Sep 07 18:41:02 Starting compiler/backend/arm8/proofs
Sep 07 18:41:28 Finished compiler/backend/arm8/proofs                            26s   1GB
Sep 07 18:41:29 Starting compiler/backend/arm8_asl
Sep 07 18:41:50 Finished compiler/backend/arm8_asl                               20s   1GB
Sep 07 18:41:50 Starting compiler/backend/mips/proofs
Sep 07 18:42:16 Finished compiler/backend/mips/proofs                            26s   1GB
Sep 07 18:42:17 Starting compiler/backend/riscv/proofs
Sep 07 18:42:43 Finished compiler/backend/riscv/proofs                           26s   1GB
Sep 07 18:42:44 Starting compiler/backend/ag32/proofs
Sep 07 18:57:30 Finished compiler/backend/ag32/proofs                         14m46s   2GB
Sep 07 18:57:30 Starting compiler/proofs
Sep 07 19:00:00 Finished compiler/proofs                                       2m29s   5GB
Sep 07 19:00:00 Starting candle/set-theory
Sep 07 19:00:35 Finished candle/set-theory                                       34s   1GB
Sep 07 19:00:36 Starting candle/syntax-lib
Sep 07 19:00:49 Finished candle/syntax-lib                                       12s 583MB
Sep 07 19:00:49 Starting candle/standard/syntax
Sep 07 19:02:56 Finished candle/standard/syntax                                2m06s   1GB
Sep 07 19:02:56 Starting candle/standard/semantics
Sep 07 19:04:44 Finished candle/standard/semantics                             1m48s   1GB
Sep 07 19:04:45 Starting candle/standard/monadic
Sep 07 19:06:44 Finished candle/standard/monadic                               1m59s   1GB
Sep 07 19:06:44 Starting candle/standard/ml_kernel
Sep 07 19:13:59 Finished candle/standard/ml_kernel                             7m13s   3GB
Sep 07 19:13:59 Starting candle/overloading/syntax
Sep 07 19:17:44 Finished candle/overloading/syntax                             3m44s   1GB
Sep 07 19:17:44 Starting candle/overloading/semantics
Sep 07 19:30:23 Finished candle/overloading/semantics                         12m39s   2GB
Sep 07 19:30:24 Starting candle/overloading/monadic
Sep 07 19:33:12 Finished candle/overloading/monadic                            2m48s   1GB
Sep 07 19:33:13 Starting candle/overloading/ml_kernel
Sep 07 19:41:14 Finished candle/overloading/ml_kernel                          8m00s   3GB
Sep 07 19:41:14 Starting candle/overloading/ml_checker
Sep 07 19:43:42 Finished candle/overloading/ml_checker                         2m27s   5GB
Sep 07 19:43:42 Starting candle/prover
Sep 07 20:10:06 Finished candle/prover                                        26m23s   4GB
Sep 07 20:10:06 Starting pancake
Sep 07 20:13:20 Finished pancake                                               3m13s   4GB
Sep 07 20:13:20 Starting pancake/ffi
Sep 07 20:13:21 Finished pancake/ffi                                              0s   8MB
Sep 07 20:13:21 Starting pancake/semantics
Sep 07 20:16:00 Finished pancake/semantics                                     2m39s   1GB
Sep 07 20:16:01 Starting pancake/proofs
Sep 07 20:29:32 Finished pancake/proofs                                       13m29s   4GB
Sep 07 20:29:32 Starting characteristic/examples
Sep 07 20:31:02 Finished characteristic/examples                               1m29s   3GB
Sep 07 20:31:03 Starting tutorial/solutions
Sep 07 20:47:40 Finished tutorial/solutions                                   16m36s   9GB
Sep 07 20:47:40 Starting translator/monadic/examples
Sep 07 20:51:41 Finished translator/monadic/examples                           4m00s   2GB
Sep 07 20:51:41 Starting examples
Sep 07 21:02:46 Finished examples                                             11m04s   6GB
Sep 07 21:02:46 Starting examples/compilation/x64
Sep 07 23:11:02 Finished examples/compilation/x64                           2h08m14s  13GB
Sep 07 23:11:03 Starting examples/compilation/x64/proofs
Sep 07 23:13:03 Finished examples/compilation/x64/proofs                       2m00s   3GB
Sep 07 23:13:03 Starting examples/compilation/ag32
Sep 07 23:47:06 Finished examples/compilation/ag32                            34m02s   8GB
Sep 07 23:47:06 Starting examples/compilation/ag32/proofs
Sep 07 23:48:00 Finished examples/compilation/ag32/proofs                        53s   4GB
Sep 07 23:48:00 Starting examples/lpr_checker
Sep 07 23:48:59 Finished examples/lpr_checker                                    58s   1GB
Sep 07 23:48:59 Starting examples/lpr_checker/array
Sep 08 00:25:38 Finished examples/lpr_checker/array                           36m37s   7GB
Sep 08 00:25:38 Starting examples/lpr_checker/array/compilation
Sep 08 01:07:11 Finished examples/lpr_checker/array/compilation               41m33s  21GB
Sep 08 01:07:11 Starting examples/lpr_checker/array/compilation/proofs
Sep 08 01:08:32 Finished examples/lpr_checker/array/compilation/proofs         1m20s   6GB
Sep 08 01:08:32 Starting examples/opentheory
Sep 08 01:19:29 Finished examples/opentheory                                  10m56s   5GB
Sep 08 01:19:29 Starting examples/opentheory
Sep 08 01:19:31 Finished examples/opentheory                                      1s  22MB
Sep 08 01:19:31 Starting examples/opentheory/compilation
Sep 08 01:58:22 Finished examples/opentheory/compilation                      38m50s  27GB
Sep 08 01:58:23 Starting examples/opentheory/compilation/proofs
Sep 08 01:59:12 Finished examples/opentheory/compilation/proofs                  49s   4GB
Sep 08 01:59:12 Starting examples/opentheory/compilation/ag32
Sep 08 02:34:50 Finished examples/opentheory/compilation/ag32                 35m36s  21GB
Sep 08 02:34:50 Starting examples/opentheory/compilation/ag32/proofs
Sep 08 02:36:37 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
Sep 08 02:36:37 Starting examples/sat_encodings
Sep 08 02:38:28 Finished examples/sat_encodings                                1m51s 712MB
Sep 08 02:38:28 Starting examples/sat_encodings/case_studies
Sep 08 02:40:13 Finished examples/sat_encodings/case_studies                   1m44s 737MB
Sep 08 02:40:13 Starting examples/sat_encodings/translation
Sep 08 02:46:15 Finished examples/sat_encodings/translation                    6m01s   3GB
Sep 08 02:46:15 Starting examples/sat_encodings/translation/compilation
Sep 08 03:37:35 Finished examples/sat_encodings/translation/compilation       51m19s  21GB
Sep 08 03:37:35 Starting examples/deflate
Sep 08 03:38:28 Finished examples/deflate                                        52s 689MB
Sep 08 03:38:28 Starting examples/deflate/translation
Sep 08 03:40:08 Finished examples/deflate/translation                          1m39s   3GB
Sep 08 03:40:08 Starting examples/deflate/translation/compilation
Sep 08 04:03:35 Finished examples/deflate/translation/compilation             23m26s  16GB
Sep 08 04:03:35 Starting translator/okasaki-examples
Sep 08 04:08:49 Finished translator/okasaki-examples                           5m12s   1GB
Sep 08 04:08:49 Starting translator/other-examples
Sep 08 04:11:20 Finished translator/other-examples                             2m31s   1GB
Sep 08 04:11:20 Starting compiler/parsing/tests
Sep 08 04:11:52 Finished compiler/parsing/tests                                  30s 664MB
Sep 08 04:11:52 Starting compiler/inference/tests
Sep 08 04:20:33 Finished compiler/inference/tests                              8m40s   4GB
Sep 08 04:20:33 Starting compiler/printing/test
Sep 08 04:24:20 Finished compiler/printing/test                                3m46s   3GB
Sep 08 04:24:20 Starting icing/flover
Sep 08 05:15:40 Finished icing/flover                                         51m19s   1GB
Sep 08 05:15:40 Starting icing/
Sep 08 06:33:18 Finished icing/                                             1h17m36s   6GB
Sep 08 06:33:18 Starting icing/examples
Sep 08 06:34:57 Finished icing/examples                                        1m38s   6GB
Sep 08 06:34:57 Starting compiler/repl
Sep 08 09:11:05 Finished compiler/repl                                      2h36m07s  24GB
Sep 08 09:11:05 Starting compiler/bootstrap/translation
Sep 08 14:02:48 Finished compiler/bootstrap/translation                     4h51m42s  44GB
Sep 08 14:02:49 Starting unverified/sexpr-bootstrap/x64/64
Sep 08 14:14:31 Finished unverified/sexpr-bootstrap/x64/64                    11m42s   8GB
Sep 08 14:14:32 Starting unverified/sexpr-bootstrap/x64/32
Sep 08 14:23:25 Finished unverified/sexpr-bootstrap/x64/32                     8m52s  11GB
Sep 08 14:23:25 Starting compiler/benchmarks
Sep 08 14:23:28 Finished compiler/benchmarks                                      3s  31MB
Sep 08 14:23:28 Starting compiler/bootstrap/compilation/x64/64
Sep 09 02:35:19 Finished compiler/bootstrap/compilation/x64/64             12h11m48s  64GB
Sep 09 02:35:20 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 09 02:56:04 Finished compiler/bootstrap/compilation/x64/64/proofs         20m43s  35GB
Sep 09 02:56:04 Starting compiler/bootstrap/compilation/x64/32
Sep 09 09:41:23 Finished compiler/bootstrap/compilation/x64/32              6h45m18s  62GB
Sep 09 09:41:23 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 09 09:44:16 Finished compiler/bootstrap/compilation/x64/32/proofs          2m52s  15GB
Sep 09 09:44:16 Starting compiler/bootstrap/compilation/ag32/32
Sep 09 16:52:41 Finished compiler/bootstrap/compilation/ag32/32             7h08m24s  64GB
Sep 09 16:52:41 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 09 17:03:56 Finished compiler/bootstrap/compilation/ag32/32/proofs        11m14s  18GB
Sep 09 17:03:56 SUCCESS