Job 1769

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:58ece1432c25bfca39de8a22e87decc09bc3516b
  Merge pull request #860 from arolle/cyclicity-check-rebase [Feb 11 10:57:07]
HOL:7d8123fd0cb1e8c2b7e3fffb337516da7cb7c9df
  Reinstate sptreeTheory.lrnext_def, which 8247e5e3a465 had deleted [Feb 10 23:16:16]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 12 06:30:02 Claimed job
Feb 12 06:30:05 Reusing HOL
Feb 12 06:30:45 Starting developers
Feb 12 06:30:50 Finished developers                                               4s  73MB
Feb 12 06:30:50 Starting developers/bin
Feb 12 06:30:55 Finished developers/bin                                           5s 670MB
Feb 12 06:30:56 Starting semantics/ffi
Feb 12 06:31:06 Finished semantics/ffi                                           10s 179MB
Feb 12 06:31:06 Starting semantics
Feb 12 06:32:36 Finished semantics                                             1m29s   1GB
Feb 12 06:32:37 Starting semantics/proofs
Feb 12 06:36:27 Finished semantics/proofs                                      3m49s   1GB
Feb 12 06:36:27 Starting semantics/alt_semantics
Feb 12 06:36:40 Finished semantics/alt_semantics                                 13s 373MB
Feb 12 06:36:40 Starting semantics/alt_semantics/proofs
Feb 12 06:39:21 Finished semantics/alt_semantics/proofs                        2m40s 760MB
Feb 12 06:39:21 Starting basis/pure
Feb 12 06:40:15 Finished basis/pure                                              53s 958MB
Feb 12 06:40:15 Starting translator
Feb 12 06:43:20 Finished translator                                            3m04s   1GB
Feb 12 06:43:20 Starting compiler/parsing
Feb 12 06:44:39 Finished compiler/parsing                                      1m19s   2GB
Feb 12 06:44:40 Starting characteristic
Feb 12 06:50:50 Finished characteristic                                        6m09s   2GB
Feb 12 06:50:50 Starting translator/monadic
Feb 12 06:52:40 Finished translator/monadic                                    1m49s   1GB
Feb 12 06:52:40 Starting basis
Feb 12 07:42:54 Finished basis                                                50m12s  15GB
Feb 12 07:42:54 Starting compiler/inference
Feb 12 07:44:07 Finished compiler/inference                                    1m12s   1GB
Feb 12 07:44:07 Starting compiler/backend/reg_alloc
Feb 12 07:45:17 Finished compiler/backend/reg_alloc                            1m09s   1GB
Feb 12 07:45:17 Starting compiler/backend/gc
Feb 12 07:49:05 Finished compiler/backend/gc                                   3m48s   2GB
Feb 12 07:49:06 Starting compiler/backend
Feb 12 07:54:37 Finished compiler/backend                                      5m31s   3GB
Feb 12 07:54:37 Starting compiler/encoders/asm
Feb 12 07:55:03 Finished compiler/encoders/asm                                   25s 678MB
Feb 12 07:55:03 Starting compiler/encoders/x64
Feb 12 07:55:32 Finished compiler/encoders/x64                                   28s 833MB
Feb 12 07:55:32 Starting compiler/encoders/arm7
Feb 12 07:56:26 Finished compiler/encoders/arm7                                  53s 700MB
Feb 12 07:56:26 Starting compiler/encoders/arm8
Feb 12 07:56:41 Finished compiler/encoders/arm8                                  14s 937MB
Feb 12 07:56:42 Starting compiler/encoders/arm8_asl
Feb 12 07:59:43 Finished compiler/encoders/arm8_asl                            3m00s   1GB
Feb 12 07:59:43 Starting compiler/encoders/mips
Feb 12 08:00:03 Finished compiler/encoders/mips                                  19s   1GB
Feb 12 08:00:03 Starting compiler/encoders/riscv
Feb 12 08:00:20 Finished compiler/encoders/riscv                                 16s 793MB
Feb 12 08:00:20 Starting compiler/encoders/ag32
Feb 12 08:00:41 Finished compiler/encoders/ag32                                  20s 720MB
Feb 12 08:00:41 Starting compiler/backend/x64
Feb 12 08:01:04 Finished compiler/backend/x64                                    23s   1GB
Feb 12 08:01:05 Starting compiler/backend/arm7
Feb 12 08:01:28 Finished compiler/backend/arm7                                   23s   1GB
Feb 12 08:01:29 Starting compiler/backend/arm8
Feb 12 08:01:51 Finished compiler/backend/arm8                                   22s   1GB
Feb 12 08:01:51 Starting compiler/backend/mips
Feb 12 08:02:15 Finished compiler/backend/mips                                   23s   1GB
Feb 12 08:02:15 Starting compiler/backend/riscv
Feb 12 08:02:38 Finished compiler/backend/riscv                                  23s   1GB
Feb 12 08:02:39 Starting compiler/backend/ag32
Feb 12 08:03:54 Finished compiler/backend/ag32                                 1m15s   1GB
Feb 12 08:03:55 Starting compiler/parsing/proofs
Feb 12 08:08:01 Finished compiler/parsing/proofs                               4m06s   1GB
Feb 12 08:08:01 Starting compiler/inference/proofs
Feb 12 08:10:42 Finished compiler/inference/proofs                             2m40s   1GB
Feb 12 08:10:43 Starting compiler/backend/semantics
Feb 12 08:43:48 Finished compiler/backend/semantics                           33m04s   2GB
Feb 12 08:43:48 Starting compiler/backend/reg_alloc/proofs
Feb 12 08:47:37 Finished compiler/backend/reg_alloc/proofs                     3m49s   1GB
Feb 12 08:47:38 Starting compiler/backend/proofs
Feb 12 09:46:49 Finished compiler/backend/proofs                              59m10s  16GB
Feb 12 09:46:49 Starting compiler/backend/serialiser
Feb 12 09:48:20 Finished compiler/backend/serialiser                           1m31s   1GB
Feb 12 09:48:20 Starting compiler/encoders/x64/proofs
Feb 12 09:58:43 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Feb 12 09:58:43 Starting compiler/encoders/arm7/proofs
Feb 12 10:12:43 Finished compiler/encoders/arm7/proofs                        14m00s   6GB
Feb 12 10:12:44 Starting compiler/encoders/arm8/proofs
Feb 12 10:19:53 Finished compiler/encoders/arm8/proofs                         7m08s   1GB
Feb 12 10:19:53 Starting compiler/encoders/arm8_asl/proofs
Feb 12 10:36:31 Finished compiler/encoders/arm8_asl/proofs                    16m37s   1GB
Feb 12 10:36:31 Starting compiler/encoders/mips/proofs
Feb 12 10:47:14 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Feb 12 10:47:14 Starting compiler/encoders/riscv/proofs
Feb 12 10:56:37 Finished compiler/encoders/riscv/proofs                        9m21s   1GB
Feb 12 10:56:37 Starting compiler/encoders/ag32/proofs
Feb 12 10:59:26 Finished compiler/encoders/ag32/proofs                         2m49s 637MB
Feb 12 10:59:27 Starting compiler/backend/x64/proofs
Feb 12 10:59:55 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 12 10:59:55 Starting compiler/backend/arm7/proofs
Feb 12 11:00:24 Finished compiler/backend/arm7/proofs                            29s   1GB
Feb 12 11:00:25 Starting compiler/backend/arm8/proofs
Feb 12 11:00:53 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 12 11:00:53 Starting compiler/backend/arm8_asl
Feb 12 11:01:17 Finished compiler/backend/arm8_asl                               23s   1GB
Feb 12 11:01:17 Starting compiler/backend/mips/proofs
Feb 12 11:01:45 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 12 11:01:45 Starting compiler/backend/riscv/proofs
Feb 12 11:02:14 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 12 11:02:14 Starting compiler/backend/ag32/proofs
Feb 12 11:15:52 Finished compiler/backend/ag32/proofs                         13m37s   2GB
Feb 12 11:15:52 Starting compiler/proofs
Feb 12 11:17:53 Finished compiler/proofs                                       2m00s   3GB
Feb 12 11:17:53 Starting candle/set-theory
Feb 12 11:18:23 Finished candle/set-theory                                       29s 836MB
Feb 12 11:18:23 Starting candle/syntax-lib
Feb 12 11:18:35 Finished candle/syntax-lib                                       11s 690MB
Feb 12 11:18:35 Starting candle/standard/syntax
Feb 12 11:20:30 Finished candle/standard/syntax                                1m55s   1GB
Feb 12 11:20:30 Starting candle/standard/semantics
Feb 12 11:22:23 Finished candle/standard/semantics                             1m52s   1GB
Feb 12 11:22:23 Starting candle/standard/monadic
Feb 12 11:24:07 Finished candle/standard/monadic                               1m42s   1GB
Feb 12 11:24:07 Starting candle/standard/ml_kernel
Feb 12 11:31:19 Finished candle/standard/ml_kernel                             7m11s   3GB
Feb 12 11:31:19 Starting candle/overloading/syntax
Feb 12 11:34:41 Finished candle/overloading/syntax                             3m21s   1GB
Feb 12 11:34:41 Starting candle/overloading/semantics
Feb 12 11:47:09 Finished candle/overloading/semantics                         12m27s   2GB
Feb 12 11:47:09 Starting candle/overloading/monadic
Feb 12 11:49:35 Finished candle/overloading/monadic                            2m25s   1GB
Feb 12 11:49:35 Starting candle/overloading/ml_kernel
Feb 12 11:57:49 Finished candle/overloading/ml_kernel                          8m13s   3GB
Feb 12 11:57:49 Starting candle/overloading/ml_checker
Feb 12 12:00:19 Finished candle/overloading/ml_checker                         2m29s   3GB
Feb 12 12:00:19 Starting candle/prover
Feb 12 12:08:23 Finished candle/prover                                         8m03s   3GB
Feb 12 12:08:23 Starting pancake
Feb 12 12:11:18 Finished pancake                                               2m54s   3GB
Feb 12 12:11:18 Starting pancake/ffi
Feb 12 12:11:19 Finished pancake/ffi                                              0s  19MB
Feb 12 12:11:19 Starting pancake/semantics
Feb 12 12:14:05 Finished pancake/semantics                                     2m45s   1GB
Feb 12 12:14:05 Starting pancake/proofs
Feb 12 12:27:07 Finished pancake/proofs                                       13m01s   6GB
Feb 12 12:27:07 Starting characteristic/examples
Feb 12 12:28:36 Finished characteristic/examples                               1m29s   3GB
Feb 12 12:28:37 Starting tutorial/solutions
Feb 12 12:45:44 Finished tutorial/solutions                                   17m06s   8GB
Feb 12 12:45:44 Starting translator/monadic/examples
Feb 12 12:49:24 Finished translator/monadic/examples                           3m39s   3GB
Feb 12 12:49:24 Starting examples
Feb 12 12:59:46 Finished examples                                             10m21s   3GB
Feb 12 12:59:46 Starting examples/compilation/x64
Feb 12 15:34:29 Finished examples/compilation/x64                           2h34m42s  16GB
Feb 12 15:34:29 Starting examples/compilation/x64/proofs
Feb 12 15:36:50 Finished examples/compilation/x64/proofs                       2m20s   3GB
Feb 12 15:36:50 Starting examples/compilation/ag32
Feb 12 16:12:58 Finished examples/compilation/ag32                            36m06s   8GB
Feb 12 16:12:58 Starting examples/compilation/ag32/proofs
Feb 12 16:14:01 Finished examples/compilation/ag32/proofs                      1m03s   3GB
Feb 12 16:14:01 Starting examples/cost
Feb 12 17:15:26 Finished examples/cost                                      1h01m18s  10GB
Feb 12 17:15:26 Starting examples/lpr_checker
Feb 12 17:16:21 Finished examples/lpr_checker                                    54s   1GB
Feb 12 17:16:21 Starting examples/lpr_checker/array
Feb 12 17:47:14 Finished examples/lpr_checker/array                           30m52s   5GB
Feb 12 17:47:14 Starting examples/lpr_checker/array/compilation
Feb 12 19:15:24 Finished examples/lpr_checker/array/compilation             1h28m06s  36GB
Feb 12 19:15:24 Starting examples/lpr_checker/array/compilation/proofs
Feb 12 19:17:38 Finished examples/lpr_checker/array/compilation/proofs         2m14s   4GB
Feb 12 19:17:39 Starting examples/opentheory
Feb 12 19:28:33 Finished examples/opentheory                                  10m54s   4GB
Feb 12 19:28:33 Starting examples/opentheory
Feb 12 19:28:35 Finished examples/opentheory                                      1s  21MB
Feb 12 19:28:35 Starting examples/opentheory/compilation
Feb 12 20:11:26 Finished examples/opentheory/compilation                      42m51s  25GB
Feb 12 20:11:27 Starting examples/opentheory/compilation/proofs
Feb 12 20:12:25 Finished examples/opentheory/compilation/proofs                  58s   4GB
Feb 12 20:12:25 Starting examples/opentheory/compilation/ag32
Feb 12 20:52:08 Finished examples/opentheory/compilation/ag32                 39m41s  23GB
Feb 12 20:52:08 Starting examples/opentheory/compilation/ag32/proofs
Feb 12 20:54:23 Finished examples/opentheory/compilation/ag32/proofs           2m15s   6GB
Feb 12 20:54:23 Starting examples/sat_encodings
Feb 12 20:56:30 Finished examples/sat_encodings                                2m06s 853MB
Feb 12 20:56:30 Starting examples/sat_encodings/case_studies
Feb 12 20:58:21 Finished examples/sat_encodings/case_studies                   1m50s 728MB
Feb 12 20:58:21 Starting examples/sat_encodings/translation
Feb 12 21:04:30 Finished examples/sat_encodings/translation                    6m08s   3GB
Feb 12 21:04:30 Starting examples/sat_encodings/translation/compilation
Feb 12 21:59:47 Finished examples/sat_encodings/translation/compilation       55m15s  21GB
Feb 12 21:59:47 Starting translator/okasaki-examples
Feb 12 22:04:48 Finished translator/okasaki-examples                           5m01s   1GB
Feb 12 22:04:48 Starting translator/other-examples
Feb 12 22:05:43 Finished translator/other-examples                               53s   1GB
Feb 12 22:05:43 Starting compiler/parsing/tests
Feb 12 22:06:16 Finished compiler/parsing/tests                                  32s 560MB
Feb 12 22:06:16 Starting compiler/inference/tests
Feb 12 22:14:34 Finished compiler/inference/tests                              8m18s   4GB
Feb 12 22:14:35 Starting compiler/bootstrap/translation
Feb 14 18:03:18 Resuming compiler/bootstrap/translation