Job 1803

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:f18f45a1f5d90a31c62adc297d68971f6e948c43
  Fix following change in Define in HOL [Feb 25 21:10:34]
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern [Feb 25 06:46:55]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 25 21:18:23 Claimed job
Feb 25 21:18:25 Reusing HOL
Feb 25 21:18:38 Starting developers
Feb 25 21:18:42 Finished developers                                               4s 136MB
Feb 25 21:18:42 Starting developers/bin
Feb 25 21:18:46 Finished developers/bin                                           4s 675MB
Feb 25 21:18:47 Starting semantics/ffi
Feb 25 21:18:56 Finished semantics/ffi                                            9s 224MB
Feb 25 21:18:56 Starting semantics
Feb 25 21:21:00 Finished semantics                                             2m02s   1GB
Feb 25 21:21:00 Starting semantics/proofs
Feb 25 21:24:38 Finished semantics/proofs                                      3m37s   1GB
Feb 25 21:24:38 Starting semantics/alt_semantics
Feb 25 21:24:54 Finished semantics/alt_semantics                                 16s 480MB
Feb 25 21:24:54 Starting semantics/alt_semantics/proofs
Feb 25 21:27:25 Finished semantics/alt_semantics/proofs                        2m30s 839MB
Feb 25 21:27:25 Starting basis/pure
Feb 25 21:28:28 Finished basis/pure                                            1m02s 887MB
Feb 25 21:28:28 Starting translator
Feb 25 21:31:30 Finished translator                                            3m02s   2GB
Feb 25 21:31:30 Starting compiler/parsing
Feb 25 21:32:44 Finished compiler/parsing                                      1m14s   2GB
Feb 25 21:32:45 Starting characteristic
Feb 25 21:39:03 Finished characteristic                                        6m18s   2GB
Feb 25 21:39:04 Starting translator/monadic
Feb 25 21:41:04 Finished translator/monadic                                    2m00s   1GB
Feb 25 21:41:05 Starting basis
Feb 25 22:27:49 Finished basis                                                46m41s  19GB
Feb 25 22:27:50 Starting compiler/inference
Feb 25 22:29:11 Finished compiler/inference                                    1m20s   1GB
Feb 25 22:29:11 Starting compiler/backend/reg_alloc
Feb 25 22:30:55 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 25 22:30:55 Starting compiler/backend/gc
Feb 25 22:35:15 Finished compiler/backend/gc                                   4m19s   1GB
Feb 25 22:35:15 Starting compiler/backend
Feb 25 22:40:43 Finished compiler/backend                                      5m28s   2GB
Feb 25 22:40:43 Starting compiler/encoders/asm
Feb 25 22:41:13 Finished compiler/encoders/asm                                   29s 756MB
Feb 25 22:41:14 Starting compiler/encoders/x64
Feb 25 22:41:43 Finished compiler/encoders/x64                                   29s   1GB
Feb 25 22:41:43 Starting compiler/encoders/arm7
Feb 25 22:42:39 Finished compiler/encoders/arm7                                  56s   1GB
Feb 25 22:42:39 Starting compiler/encoders/arm8
Feb 25 22:42:56 Finished compiler/encoders/arm8                                  16s 955MB
Feb 25 22:42:56 Starting compiler/encoders/arm8_asl
Feb 25 22:45:28 Finished compiler/encoders/arm8_asl                            2m31s 945MB
Feb 25 22:45:28 Starting compiler/encoders/mips
Feb 25 22:45:49 Finished compiler/encoders/mips                                  21s   1GB
Feb 25 22:45:50 Starting compiler/encoders/riscv
Feb 25 22:46:09 Finished compiler/encoders/riscv                                 19s   1GB
Feb 25 22:46:09 Starting compiler/encoders/ag32
Feb 25 22:46:31 Finished compiler/encoders/ag32                                  21s   1GB
Feb 25 22:46:32 Starting compiler/backend/x64
Feb 25 22:46:54 Finished compiler/backend/x64                                    22s   1GB
Feb 25 22:46:54 Starting compiler/backend/arm7
Feb 25 22:47:16 Finished compiler/backend/arm7                                   22s   1GB
Feb 25 22:47:16 Starting compiler/backend/arm8
Feb 25 22:47:38 Finished compiler/backend/arm8                                   21s   1GB
Feb 25 22:47:38 Starting compiler/backend/mips
Feb 25 22:48:00 Finished compiler/backend/mips                                   22s   1GB
Feb 25 22:48:00 Starting compiler/backend/riscv
Feb 25 22:48:23 Finished compiler/backend/riscv                                  22s   1GB
Feb 25 22:48:23 Starting compiler/backend/ag32
Feb 25 22:49:50 Finished compiler/backend/ag32                                 1m27s   1GB
Feb 25 22:49:50 Starting compiler/parsing/proofs
Feb 25 22:53:33 Finished compiler/parsing/proofs                               3m42s   1GB
Feb 25 22:53:33 Starting compiler/inference/proofs
Feb 25 22:56:06 Finished compiler/inference/proofs                             2m33s   1GB
Feb 25 22:56:06 Starting compiler/backend/semantics
Feb 25 23:24:23 Finished compiler/backend/semantics                           28m16s   2GB
Feb 25 23:24:23 Starting compiler/backend/reg_alloc/proofs
Feb 25 23:27:56 Finished compiler/backend/reg_alloc/proofs                     3m30s 880MB
Feb 25 23:27:56 Starting compiler/backend/proofs
Feb 26 00:19:48 Finished compiler/backend/proofs                              51m51s  16GB
Feb 26 00:19:48 Starting compiler/backend/serialiser
Feb 26 00:21:25 Finished compiler/backend/serialiser                           1m36s   2GB
Feb 26 00:21:25 Starting compiler/encoders/x64/proofs
Feb 26 00:30:58 Finished compiler/encoders/x64/proofs                          9m30s   5GB
Feb 26 00:30:58 Starting compiler/encoders/arm7/proofs
Feb 26 00:44:15 Finished compiler/encoders/arm7/proofs                        13m16s   3GB
Feb 26 00:44:15 Starting compiler/encoders/arm8/proofs
Feb 26 00:50:59 Finished compiler/encoders/arm8/proofs                         6m43s   1GB
Feb 26 00:50:59 Starting compiler/encoders/arm8_asl/proofs
Feb 26 01:06:03 Finished compiler/encoders/arm8_asl/proofs                    15m03s   2GB
Feb 26 01:06:03 Starting compiler/encoders/mips/proofs
Feb 26 01:16:11 Finished compiler/encoders/mips/proofs                        10m07s   1GB
Feb 26 01:16:11 Starting compiler/encoders/riscv/proofs
Feb 26 01:25:02 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Feb 26 01:25:02 Starting compiler/encoders/ag32/proofs
Feb 26 01:27:34 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Feb 26 01:27:34 Starting compiler/backend/x64/proofs
Feb 26 01:28:02 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 26 01:28:02 Starting compiler/backend/arm7/proofs
Feb 26 01:28:30 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 26 01:28:31 Starting compiler/backend/arm8/proofs
Feb 26 01:28:58 Finished compiler/backend/arm8/proofs                            27s   1GB
Feb 26 01:28:59 Starting compiler/backend/arm8_asl
Feb 26 01:29:22 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 26 01:29:22 Starting compiler/backend/mips/proofs
Feb 26 01:29:50 Finished compiler/backend/mips/proofs                            28s   1GB
Feb 26 01:29:50 Starting compiler/backend/riscv/proofs
Feb 26 01:30:17 Finished compiler/backend/riscv/proofs                           26s   1GB
Feb 26 01:30:17 Starting compiler/backend/ag32/proofs
Feb 26 01:43:12 Finished compiler/backend/ag32/proofs                         12m52s   2GB
Feb 26 01:43:12 Starting compiler/proofs
Feb 26 01:45:18 Finished compiler/proofs                                       2m05s   3GB
Feb 26 01:45:18 Starting candle/set-theory
Feb 26 01:45:53 Finished candle/set-theory                                       34s   1GB
Feb 26 01:45:53 Starting candle/syntax-lib
Feb 26 01:46:06 Finished candle/syntax-lib                                       12s 690MB
Feb 26 01:46:06 Starting candle/standard/syntax
Feb 26 01:48:09 Finished candle/standard/syntax                                2m02s   1GB
Feb 26 01:48:09 Starting candle/standard/semantics
Feb 26 01:49:58 Finished candle/standard/semantics                             1m49s   1GB
Feb 26 01:49:58 Starting candle/standard/monadic
Feb 26 01:51:50 Finished candle/standard/monadic                               1m52s   1GB
Feb 26 01:51:50 Starting candle/standard/ml_kernel
Feb 26 01:58:00 Finished candle/standard/ml_kernel                             6m09s   3GB
Feb 26 01:58:00 Starting candle/overloading/syntax
Feb 26 02:01:12 Finished candle/overloading/syntax                             3m11s   1GB
Feb 26 02:01:12 Starting candle/overloading/semantics
Feb 26 02:13:00 Finished candle/overloading/semantics                         11m48s   2GB
Feb 26 02:13:00 Starting candle/overloading/monadic
Feb 26 02:15:33 Finished candle/overloading/monadic                            2m32s   1GB
Feb 26 02:15:33 Starting candle/overloading/ml_kernel
Feb 26 02:22:34 Finished candle/overloading/ml_kernel                          7m01s   3GB
Feb 26 02:22:35 Starting candle/overloading/ml_checker
Feb 26 02:25:05 Finished candle/overloading/ml_checker                         2m30s   2GB
Feb 26 02:25:05 Starting candle/prover
Feb 26 02:32:41 Finished candle/prover                                         7m36s   3GB
Feb 26 02:32:41 Starting pancake
Feb 26 02:35:24 Finished pancake                                               2m42s   2GB
Feb 26 02:35:24 Starting pancake/ffi
Feb 26 02:35:24 Finished pancake/ffi                                              0s  35MB
Feb 26 02:35:24 Starting pancake/semantics
Feb 26 02:37:52 Finished pancake/semantics                                     2m27s   1GB
Feb 26 02:37:52 Starting pancake/proofs
Feb 26 02:49:48 Finished pancake/proofs                                       11m54s   6GB
Feb 26 02:49:48 Starting characteristic/examples
Feb 26 02:51:14 Finished characteristic/examples                               1m26s   2GB
Feb 26 02:51:14 Starting tutorial/solutions
Feb 26 03:07:34 Finished tutorial/solutions                                   16m20s  10GB
Feb 26 03:07:35 Starting translator/monadic/examples
Feb 26 03:11:20 Finished translator/monadic/examples                           3m45s   3GB
Feb 26 03:11:20 Starting examples
Feb 26 03:20:28 Finished examples                                              9m08s   3GB
Feb 26 03:20:28 Starting examples/compilation/x64
Feb 26 05:48:42 Finished examples/compilation/x64                           2h28m10s  17GB
Feb 26 05:48:42 Starting examples/compilation/x64/proofs
Feb 26 05:51:17 Finished examples/compilation/x64/proofs                       2m34s   3GB
Feb 26 05:51:17 Starting examples/compilation/ag32
Feb 26 06:26:14 Finished examples/compilation/ag32                            34m56s   8GB
Feb 26 06:26:14 Starting examples/compilation/ag32/proofs
Feb 26 06:27:08 Finished examples/compilation/ag32/proofs                        54s   3GB
Feb 26 06:27:08 Starting examples/cost
Feb 26 07:22:40 Finished examples/cost                                        55m27s   9GB
Feb 26 07:22:41 Starting examples/lpr_checker
Feb 26 07:23:44 Finished examples/lpr_checker                                  1m03s   1GB
Feb 26 07:23:44 Starting examples/lpr_checker/array
Feb 26 07:52:12 Finished examples/lpr_checker/array                           28m27s   9GB
Feb 26 07:52:12 Starting examples/lpr_checker/array/compilation
Feb 26 09:18:17 Finished examples/lpr_checker/array/compilation             1h26m02s  26GB
Feb 26 09:18:17 Starting examples/lpr_checker/array/compilation/proofs
Feb 26 09:19:47 Finished examples/lpr_checker/array/compilation/proofs         1m29s   8GB
Feb 26 09:19:47 Starting examples/opentheory
Feb 26 09:29:30 Finished examples/opentheory                                   9m42s   5GB
Feb 26 09:29:30 Starting examples/opentheory
Feb 26 09:29:31 Finished examples/opentheory                                      1s 130MB
Feb 26 09:29:31 Starting examples/opentheory/compilation
Feb 26 10:08:40 Finished examples/opentheory/compilation                      39m08s  33GB
Feb 26 10:08:40 Starting examples/opentheory/compilation/proofs
Feb 26 10:09:58 Finished examples/opentheory/compilation/proofs                1m18s   3GB
Feb 26 10:09:58 Starting examples/opentheory/compilation/ag32
Feb 26 10:49:49 Finished examples/opentheory/compilation/ag32                 39m49s  29GB
Feb 26 10:49:49 Starting examples/opentheory/compilation/ag32/proofs
Feb 26 10:51:34 Finished examples/opentheory/compilation/ag32/proofs           1m45s   4GB
Feb 26 10:51:34 Starting examples/sat_encodings
Feb 26 10:53:37 Finished examples/sat_encodings                                2m02s   1GB
Feb 26 10:53:37 Starting examples/sat_encodings/case_studies
Feb 26 10:55:19 Finished examples/sat_encodings/case_studies                   1m42s 742MB
Feb 26 10:55:19 Starting examples/sat_encodings/translation
Feb 26 11:01:02 Finished examples/sat_encodings/translation                    5m42s   3GB
Feb 26 11:01:02 Starting examples/sat_encodings/translation/compilation
Feb 26 11:50:34 Finished examples/sat_encodings/translation/compilation       49m30s  18GB
Feb 26 11:50:34 Starting translator/okasaki-examples
Feb 26 11:55:26 Finished translator/okasaki-examples                           4m52s   1GB
Feb 26 11:55:26 Starting translator/other-examples
Feb 26 11:57:24 Finished translator/other-examples                             1m57s   1GB
Feb 26 11:57:24 Starting compiler/parsing/tests
Feb 26 11:57:55 Finished compiler/parsing/tests                                  30s 709MB
Feb 26 11:57:55 Starting compiler/inference/tests
Feb 26 12:06:04 Finished compiler/inference/tests                              8m09s   5GB
Feb 26 12:06:04 Starting compiler/bootstrap/translation Feb 26 12:06:04 32412s