Job 1976

CakeML:b58c4c0c1fc5377adaf1973a094089120c8830c4
  Prove compile_single correctness for no_alloc & no_install [Aug 25 05:35:50]
#907 (word_to_word_Pancake)
Merging into:1afd9c2ae712011d1edddfc51a00c38d36bbb43a
  Merge pull request #906 from CakeML/candle-features [Aug 25 05:11:25]
HOL:2760fe927ddeb4f3149e8ece6018c9d49086ad77
  Tweak custom string-literal p/printing to not insert extra spaces [Aug 16 00:30:34]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 25 12:10:03 Claimed job
Aug 25 12:10:06 Reusing HOL
Aug 25 12:10:46 Starting developers
Aug 25 12:10:52 Finished developers                                               5s 114MB
Aug 25 12:10:52 Starting developers/bin
Aug 25 12:12:37 Finished developers/bin                                        1m44s   1GB
Aug 25 12:12:37 Starting semantics/ffi
Aug 25 12:12:47 Finished semantics/ffi                                            9s 192MB
Aug 25 12:12:47 Starting semantics
Aug 25 12:15:21 Finished semantics                                             2m33s   1GB
Aug 25 12:15:21 Starting semantics/proofs
Aug 25 12:22:56 Finished semantics/proofs                                      7m33s   1GB
Aug 25 12:22:56 Starting semantics/alt_semantics
Aug 25 12:23:24 Finished semantics/alt_semantics                                 28s 562MB
Aug 25 12:23:25 Starting semantics/alt_semantics/proofs
Aug 25 12:36:01 Finished semantics/alt_semantics/proofs                       12m36s   1GB
Aug 25 12:36:01 Starting basis/pure
Aug 25 12:37:08 Finished basis/pure                                            1m06s 921MB
Aug 25 12:37:08 Starting translator
Aug 25 12:41:04 Finished translator                                            3m55s   1GB
Aug 25 12:41:05 Starting compiler/parsing
Aug 25 12:42:33 Finished compiler/parsing                                      1m27s   3GB
Aug 25 12:42:33 Starting characteristic
Aug 25 12:49:41 Finished characteristic                                        7m07s   1GB
Aug 25 12:49:41 Starting translator/monadic
Aug 25 12:51:41 Finished translator/monadic                                    1m58s   1GB
Aug 25 12:51:41 Starting basis
Aug 25 13:48:22 Finished basis                                                56m40s  10GB
Aug 25 13:48:22 Starting compiler/inference
Aug 25 13:49:55 Finished compiler/inference                                    1m33s   1GB
Aug 25 13:49:56 Starting compiler/backend/reg_alloc
Aug 25 13:51:43 Finished compiler/backend/reg_alloc                            1m47s   1GB
Aug 25 13:51:43 Starting compiler/backend/gc
Aug 25 13:56:21 Finished compiler/backend/gc                                   4m37s   2GB
Aug 25 13:56:21 Starting compiler/backend
Aug 25 14:02:19 Finished compiler/backend                                      5m57s   2GB
Aug 25 14:02:19 Starting compiler/encoders/asm
Aug 25 14:02:50 Finished compiler/encoders/asm                                   30s 999MB
Aug 25 14:02:50 Starting compiler/encoders/x64
Aug 25 14:03:20 Finished compiler/encoders/x64                                   29s 821MB
Aug 25 14:03:20 Starting compiler/encoders/arm7
Aug 25 14:04:22 Finished compiler/encoders/arm7                                1m01s 828MB
Aug 25 14:04:22 Starting compiler/encoders/arm8
Aug 25 14:04:40 Finished compiler/encoders/arm8                                  17s 620MB
Aug 25 14:04:40 Starting compiler/encoders/arm8_asl
Aug 25 14:07:40 Finished compiler/encoders/arm8_asl                            2m59s   1GB
Aug 25 14:07:40 Starting compiler/encoders/mips
Aug 25 14:08:01 Finished compiler/encoders/mips                                  21s   1GB
Aug 25 14:08:02 Starting compiler/encoders/riscv
Aug 25 14:08:21 Finished compiler/encoders/riscv                                 19s   1GB
Aug 25 14:08:21 Starting compiler/encoders/ag32
Aug 25 14:08:43 Finished compiler/encoders/ag32                                  21s 740MB
Aug 25 14:08:44 Starting compiler/backend/x64
Aug 25 14:09:05 Finished compiler/backend/x64                                    21s   1GB
Aug 25 14:09:06 Starting compiler/backend/arm7
Aug 25 14:09:30 Finished compiler/backend/arm7                                   23s   1GB
Aug 25 14:09:30 Starting compiler/backend/arm8
Aug 25 14:09:52 Finished compiler/backend/arm8                                   21s   1GB
Aug 25 14:09:52 Starting compiler/backend/mips
Aug 25 14:10:14 Finished compiler/backend/mips                                   22s   1GB
Aug 25 14:10:15 Starting compiler/backend/riscv
Aug 25 14:10:37 Finished compiler/backend/riscv                                  22s   1GB
Aug 25 14:10:37 Starting compiler/backend/ag32
Aug 25 14:12:07 Finished compiler/backend/ag32                                 1m29s   1GB
Aug 25 14:12:07 Starting compiler/parsing/proofs
Aug 25 14:16:13 Finished compiler/parsing/proofs                               4m06s   1GB
Aug 25 14:16:14 Starting compiler/inference/proofs
Aug 25 14:19:06 Finished compiler/inference/proofs                             2m51s   1GB
Aug 25 14:19:06 Starting compiler/backend/semantics
Aug 25 14:49:57 Finished compiler/backend/semantics                           30m51s   2GB
Aug 25 14:49:58 Starting compiler/backend/reg_alloc/proofs
Aug 25 14:54:01 Finished compiler/backend/reg_alloc/proofs                     4m02s 796MB
Aug 25 14:54:01 Starting compiler/backend/proofs
Aug 25 15:56:06 Finished compiler/backend/proofs                            1h02m04s  17GB
Aug 25 15:56:06 Starting compiler/backend/serialiser
Aug 25 15:57:37 Finished compiler/backend/serialiser                           1m30s   2GB
Aug 25 15:57:37 Starting compiler/encoders/x64/proofs
Aug 25 16:08:12 Finished compiler/encoders/x64/proofs                         10m34s   4GB
Aug 25 16:08:12 Starting compiler/encoders/arm7/proofs
Aug 25 16:22:58 Finished compiler/encoders/arm7/proofs                        14m45s   3GB
Aug 25 16:22:59 Starting compiler/encoders/arm8/proofs
Aug 25 16:30:31 Finished compiler/encoders/arm8/proofs                         7m31s   1GB
Aug 25 16:30:31 Starting compiler/encoders/arm8_asl/proofs
Aug 25 16:47:29 Finished compiler/encoders/arm8_asl/proofs                    16m57s   2GB
Aug 25 16:47:29 Starting compiler/encoders/mips/proofs
Aug 25 16:58:46 Finished compiler/encoders/mips/proofs                        11m15s   2GB
Aug 25 16:58:46 Starting compiler/encoders/riscv/proofs
Aug 25 17:08:33 Finished compiler/encoders/riscv/proofs                        9m47s   1GB
Aug 25 17:08:34 Starting compiler/encoders/ag32/proofs
Aug 25 17:11:26 Finished compiler/encoders/ag32/proofs                         2m52s 648MB
Aug 25 17:11:26 Starting compiler/backend/x64/proofs
Aug 25 17:11:52 Finished compiler/backend/x64/proofs                             25s   1GB
Aug 25 17:11:53 Starting compiler/backend/arm7/proofs
Aug 25 17:12:20 Finished compiler/backend/arm7/proofs                            27s   1GB
Aug 25 17:12:20 Starting compiler/backend/arm8/proofs
Aug 25 17:12:47 Finished compiler/backend/arm8/proofs                            26s   1GB
Aug 25 17:12:47 Starting compiler/backend/arm8_asl
Aug 25 17:13:09 Finished compiler/backend/arm8_asl                               21s   1GB
Aug 25 17:13:09 Starting compiler/backend/mips/proofs
Aug 25 17:13:35 Finished compiler/backend/mips/proofs                            25s   1GB
Aug 25 17:13:35 Starting compiler/backend/riscv/proofs
Aug 25 17:14:01 Finished compiler/backend/riscv/proofs                           25s   1GB
Aug 25 17:14:02 Starting compiler/backend/ag32/proofs
Aug 25 17:28:23 Finished compiler/backend/ag32/proofs                         14m20s   2GB
Aug 25 17:28:23 Starting compiler/proofs
Aug 25 17:30:29 Finished compiler/proofs                                       2m05s   3GB
Aug 25 17:30:30 Starting candle/set-theory
Aug 25 17:31:05 Finished candle/set-theory                                       35s 936MB
Aug 25 17:31:05 Starting candle/syntax-lib
Aug 25 17:31:18 Finished candle/syntax-lib                                       12s 654MB
Aug 25 17:31:19 Starting candle/standard/syntax
Aug 25 17:33:26 Finished candle/standard/syntax                                2m06s 968MB
Aug 25 17:33:26 Starting candle/standard/semantics
Aug 25 17:35:12 Finished candle/standard/semantics                             1m46s   1GB
Aug 25 17:35:13 Starting candle/standard/monadic
Aug 25 17:37:14 Finished candle/standard/monadic                               2m01s   2GB
Aug 25 17:37:14 Starting candle/standard/ml_kernel
Aug 25 17:44:21 Finished candle/standard/ml_kernel                             7m05s   3GB
Aug 25 17:44:21 Starting candle/overloading/syntax
Aug 25 17:47:47 Finished candle/overloading/syntax                             3m25s 971MB
Aug 25 17:47:47 Starting candle/overloading/semantics
Aug 25 18:00:21 Finished candle/overloading/semantics                         12m33s   2GB
Aug 25 18:00:21 Starting candle/overloading/monadic
Aug 25 18:03:05 Finished candle/overloading/monadic                            2m43s   2GB
Aug 25 18:03:05 Starting candle/overloading/ml_kernel
Aug 25 18:11:04 Finished candle/overloading/ml_kernel                          7m58s   4GB
Aug 25 18:11:05 Starting candle/overloading/ml_checker
Aug 25 18:13:52 Finished candle/overloading/ml_checker                         2m46s   3GB
Aug 25 18:13:52 Starting candle/prover
Aug 25 18:30:26 Finished candle/prover                                        16m33s   4GB
Aug 25 18:30:26 Starting pancake
Aug 25 18:33:31 Finished pancake                                               3m04s   3GB
Aug 25 18:33:31 Starting pancake/ffi
Aug 25 18:33:32 Finished pancake/ffi                                              0s   9MB
Aug 25 18:33:32 Starting pancake/semantics
Aug 25 18:36:07 Finished pancake/semantics                                     2m34s   1GB
Aug 25 18:36:07 Starting pancake/proofs
Aug 25 18:49:34 Finished pancake/proofs                                       13m26s   5GB
Aug 25 18:49:34 Starting characteristic/examples
Aug 25 18:51:02 Finished characteristic/examples                               1m27s   3GB
Aug 25 18:51:02 Starting tutorial/solutions
Aug 25 19:07:29 Finished tutorial/solutions                                   16m26s   8GB
Aug 25 19:07:30 Starting translator/monadic/examples
Aug 25 19:11:28 Finished translator/monadic/examples                           3m57s   2GB
Aug 25 19:11:28 Starting examples
Aug 25 19:22:15 Finished examples                                             10m46s   4GB
Aug 25 19:22:15 Starting examples/compilation/x64
Aug 25 21:30:24 Finished examples/compilation/x64                           2h08m07s  14GB
Aug 25 21:30:25 Starting examples/compilation/x64/proofs
Aug 25 21:32:44 Finished examples/compilation/x64/proofs                       2m19s   3GB
Aug 25 21:32:44 Starting examples/compilation/ag32
Aug 25 22:07:25 Finished examples/compilation/ag32                            34m39s   6GB
Aug 25 22:07:25 Starting examples/compilation/ag32/proofs
Aug 25 22:08:19 Finished examples/compilation/ag32/proofs                        53s   4GB
Aug 25 22:08:19 Starting examples/lpr_checker
Aug 25 22:09:19 Finished examples/lpr_checker                                    59s   1GB
Aug 25 22:09:19 Starting examples/lpr_checker/array
Aug 26 14:14:42 Resuming examples/lpr_checker/array
Aug 26 14:14:44 Finished examples/lpr_checker/array                               1s  27MB
Aug 26 14:14:44 Starting examples/lpr_checker/array/compilation
Aug 26 14:56:11 Finished examples/lpr_checker/array/compilation               41m23s  32GB
Aug 26 14:56:11 Starting examples/lpr_checker/array/compilation/proofs
Aug 26 14:57:33 Finished examples/lpr_checker/array/compilation/proofs         1m21s   6GB
Aug 26 14:57:33 Starting examples/opentheory
Aug 26 15:08:37 Finished examples/opentheory                                  11m04s   4GB
Aug 26 15:08:38 Starting examples/opentheory
Aug 26 15:08:39 Finished examples/opentheory                                      1s  19MB
Aug 26 15:08:40 Starting examples/opentheory/compilation
Aug 26 15:47:45 Finished examples/opentheory/compilation                      39m05s  27GB
Aug 26 15:47:45 Starting examples/opentheory/compilation/proofs
Aug 26 15:48:35 Finished examples/opentheory/compilation/proofs                  49s   4GB
Aug 26 15:48:36 Starting examples/opentheory/compilation/ag32
Aug 26 16:24:35 Finished examples/opentheory/compilation/ag32                 35m58s  20GB
Aug 26 16:24:35 Starting examples/opentheory/compilation/ag32/proofs
Aug 26 16:26:29 Finished examples/opentheory/compilation/ag32/proofs           1m54s   4GB
Aug 26 16:26:30 Starting examples/sat_encodings
Aug 26 16:28:21 Finished examples/sat_encodings                                1m50s 723MB
Aug 26 16:28:21 Starting examples/sat_encodings/case_studies
Aug 26 16:30:05 Finished examples/sat_encodings/case_studies                   1m44s 666MB
Aug 26 16:30:05 Starting examples/sat_encodings/translation
Aug 26 16:36:06 Finished examples/sat_encodings/translation                    6m00s   4GB
Aug 26 16:36:06 Starting examples/sat_encodings/translation/compilation
Aug 26 17:27:49 Finished examples/sat_encodings/translation/compilation       51m42s  22GB
Aug 26 17:27:49 Starting examples/deflate
Aug 26 17:28:42 Finished examples/deflate                                        53s 673MB
Aug 26 17:28:42 Starting examples/deflate/translation
Aug 26 17:30:24 Finished examples/deflate/translation                          1m41s   3GB
Aug 26 17:30:24 Starting examples/deflate/translation/compilation
Aug 26 17:53:49 Finished examples/deflate/translation/compilation             23m24s  15GB
Aug 26 17:53:49 Starting translator/okasaki-examples
Aug 26 17:59:03 Finished translator/okasaki-examples                           5m13s   1GB
Aug 26 17:59:04 Starting translator/other-examples
Aug 26 17:59:54 Finished translator/other-examples                               49s   1GB
Aug 26 17:59:54 Starting compiler/parsing/tests
Aug 26 18:00:25 Finished compiler/parsing/tests                                  30s 628MB
Aug 26 18:00:25 Starting compiler/inference/tests
Aug 26 18:09:06 Finished compiler/inference/tests                              8m40s   5GB
Aug 26 18:09:06 Starting compiler/printing/test
Aug 26 18:12:55 Finished compiler/printing/test                                3m48s   2GB
Aug 26 18:12:55 Starting icing/flover
Aug 26 19:04:48 Finished icing/flover                                         51m53s 984MB
Aug 26 19:04:48 Starting icing/
Aug 26 20:21:56 Finished icing/                                             1h17m05s   5GB
Aug 26 20:21:56 Starting icing/examples
Aug 26 20:23:31 Finished icing/examples                                        1m34s   5GB
Aug 26 20:23:31 Starting compiler/repl
Aug 26 22:59:59 Finished compiler/repl                                      2h36m27s  24GB
Aug 26 22:59:59 Starting compiler/bootstrap/translation
Aug 27 03:49:21 Finished compiler/bootstrap/translation                     4h49m19s  40GB
Aug 27 03:49:21 Starting unverified/sexpr-bootstrap/x64/64
Aug 27 04:00:15 Finished unverified/sexpr-bootstrap/x64/64                    10m54s  11GB
Aug 27 04:00:15 Starting unverified/sexpr-bootstrap/x64/32
Aug 27 04:09:03 Finished unverified/sexpr-bootstrap/x64/32                     8m47s  11GB
Aug 27 04:09:04 Starting compiler/benchmarks
Aug 27 04:09:08 Finished compiler/benchmarks                                      3s  30MB
Aug 27 04:09:08 Starting compiler/bootstrap/compilation/x64/64
Aug 27 16:12:07 Finished compiler/bootstrap/compilation/x64/64             12h02m58s  64GB
Aug 27 16:12:07 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 27 16:31:02 Finished compiler/bootstrap/compilation/x64/64/proofs         18m55s  19GB
Aug 27 16:31:03 Starting compiler/bootstrap/compilation/x64/32
Aug 27 23:09:52 Finished compiler/bootstrap/compilation/x64/32              6h38m48s  64GB
Aug 27 23:09:53 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 27 23:13:19 Finished compiler/bootstrap/compilation/x64/32/proofs          3m26s  11GB
Aug 27 23:13:19 Starting compiler/bootstrap/compilation/ag32/32
Aug 28 06:01:33 Finished compiler/bootstrap/compilation/ag32/32             6h48m12s  64GB
Aug 28 06:01:33 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 28 06:10:06 Finished compiler/bootstrap/compilation/ag32/32/proofs         8m32s  16GB
Aug 28 06:10:06 SUCCESS