Job 2631

CakeML:dfbdb671e1bb100903b2fc50179b1241bba4b006
  Fix errors [Sep 30 21:15:46]
#1061 (remove-tDefine-paren-matching)
Merging into:f75fcbe801e04eaa9ba012a65a23b09ddb54203a
  Fix proof broken by recent HOL change [Oct 03 03:30:59]
HOL:f109565d4b7a35bcb66d3aa3ab31e8129d1bac46
  Document IgnAsm & NoAsms in DESCRIPTION; mention in release notes [Oct 01 05:38:22]
Machine:pavlova

Oct 03 11:47:50 Claimed job
Oct 03 11:47:59 Building HOL
Oct 03 12:03:08 Starting developers
Oct 03 12:03:12 Finished developers                                               2s 208MB
Oct 03 12:03:13 Starting developers/bin
Oct 03 12:03:35 Finished developers/bin                                          20s   1GB
Oct 03 12:03:36 Starting compiler/proofs
Oct 03 13:52:06 Finished compiler/proofs                                    1h48m28s  42GB
Oct 03 13:52:07 Starting compiler/bootstrap/translation
Oct 03 23:12:28 Finished compiler/bootstrap/translation                     9h20m19s  94GB
Oct 03 23:12:29 Starting semantics/ffi
Oct 03 23:12:38 Finished semantics/ffi                                            8s 644MB
Oct 03 23:12:39 Starting semantics
Oct 03 23:12:40 Finished semantics                                                0s  69MB
Oct 03 23:12:41 Starting semantics/proofs
Oct 03 23:13:06 Finished semantics/proofs                                        23s 796MB
Oct 03 23:13:07 Starting semantics/alt_semantics
Oct 03 23:13:31 Finished semantics/alt_semantics                                 22s 710MB
Oct 03 23:13:31 Starting semantics/alt_semantics/proofs
Oct 03 23:23:48 Finished semantics/alt_semantics/proofs                       10m15s   3GB
Oct 03 23:23:49 Starting basis/pure
Oct 03 23:23:51 Finished basis/pure                                               0s  71MB
Oct 03 23:23:51 Starting translator
Oct 03 23:25:28 Finished translator                                            1m35s   4GB
Oct 03 23:25:29 Starting compiler/parsing
Oct 03 23:25:30 Finished compiler/parsing                                         0s  72MB
Oct 03 23:25:31 Starting characteristic
Oct 03 23:25:33 Finished characteristic                                           0s  95MB
Oct 03 23:25:33 Starting translator/monadic
Oct 03 23:25:35 Finished translator/monadic                                       0s  99MB
Oct 03 23:25:36 Starting basis
Oct 03 23:28:02 Finished basis                                                 2m25s   5GB
Oct 03 23:28:03 Starting compiler/inference
Oct 03 23:28:05 Finished compiler/inference                                       0s  94MB
Oct 03 23:28:06 Starting compiler/backend/reg_alloc
Oct 03 23:28:07 Finished compiler/backend/reg_alloc                               0s  64MB
Oct 03 23:28:08 Starting compiler/backend/gc
Oct 03 23:28:10 Finished compiler/backend/gc                                      1s 140MB
Oct 03 23:28:11 Starting compiler/backend
Oct 03 23:28:17 Finished compiler/backend                                         4s 354MB
Oct 03 23:28:18 Starting compiler/encoders/asm
Oct 03 23:28:20 Finished compiler/encoders/asm                                    0s  90MB
Oct 03 23:28:21 Starting compiler/encoders/x64
Oct 03 23:28:22 Finished compiler/encoders/x64                                    0s  94MB
Oct 03 23:28:23 Starting compiler/encoders/arm7
Oct 03 23:28:25 Finished compiler/encoders/arm7                                   0s  99MB
Oct 03 23:28:26 Starting compiler/encoders/arm8
Oct 03 23:28:27 Finished compiler/encoders/arm8                                   0s  99MB
Oct 03 23:28:28 Starting compiler/encoders/arm8_asl
Oct 04 01:56:53 Finished compiler/encoders/arm8_asl                         2h28m24s  41GB
Oct 04 01:56:54 Starting compiler/encoders/mips
Oct 04 01:56:56 Finished compiler/encoders/mips                                   0s  92MB
Oct 04 01:56:57 Starting compiler/encoders/riscv
Oct 04 01:56:59 Finished compiler/encoders/riscv                                  0s  99MB
Oct 04 01:56:59 Starting compiler/encoders/ag32
Oct 04 01:57:01 Finished compiler/encoders/ag32                                   0s  90MB
Oct 04 01:57:02 Starting compiler/backend/x64
Oct 04 01:57:04 Finished compiler/backend/x64                                     1s 139MB
Oct 04 01:57:05 Starting compiler/backend/arm7
Oct 04 01:57:07 Finished compiler/backend/arm7                                    1s 139MB
Oct 04 01:57:08 Starting compiler/backend/arm8
Oct 04 01:57:10 Finished compiler/backend/arm8                                    1s 139MB
Oct 04 01:57:11 Starting compiler/backend/mips
Oct 04 01:57:13 Finished compiler/backend/mips                                    1s 131MB
Oct 04 01:57:14 Starting compiler/backend/riscv
Oct 04 01:57:16 Finished compiler/backend/riscv                                   1s 131MB
Oct 04 01:57:17 Starting compiler/backend/ag32
Oct 04 01:58:28 Finished compiler/backend/ag32                                 1m10s   2GB
Oct 04 01:58:29 Starting compiler/parsing/proofs
Oct 04 01:58:30 Finished compiler/parsing/proofs                                  0s  75MB
Oct 04 01:58:31 Starting compiler/inference/proofs
Oct 04 01:58:33 Finished compiler/inference/proofs                                0s  99MB
Oct 04 01:58:34 Starting compiler/backend/semantics
Oct 04 02:01:45 Finished compiler/backend/semantics                            3m10s   4GB
Oct 04 02:01:46 Starting compiler/backend/reg_alloc/proofs
Oct 04 02:01:48 Finished compiler/backend/reg_alloc/proofs                        0s 101MB
Oct 04 02:01:48 Starting compiler/backend/proofs
Oct 04 02:02:48 Finished compiler/backend/proofs                                 58s   5GB
Oct 04 02:02:49 Starting compiler/backend/serialiser
Oct 04 02:02:51 Finished compiler/backend/serialiser                              1s 143MB
Oct 04 02:02:52 Starting compiler/encoders/x64/proofs
Oct 04 02:13:09 Finished compiler/encoders/x64/proofs                         10m16s   5GB
Oct 04 02:13:10 Starting compiler/encoders/arm7/proofs
Oct 04 02:26:13 Finished compiler/encoders/arm7/proofs                        13m01s   6GB
Oct 04 02:26:13 Starting compiler/encoders/arm8/proofs
Oct 04 02:33:16 Finished compiler/encoders/arm8/proofs                         7m01s   5GB
Oct 04 02:33:17 Starting compiler/encoders/arm8_asl/proofs
Oct 04 03:24:11 Finished compiler/encoders/arm8_asl/proofs                    50m52s  12GB
Oct 04 03:24:11 Starting compiler/encoders/mips/proofs
Oct 04 03:34:37 Finished compiler/encoders/mips/proofs                        10m24s  10GB
Oct 04 03:34:38 Starting compiler/encoders/riscv/proofs
Oct 04 03:42:56 Finished compiler/encoders/riscv/proofs                        8m16s   4GB
Oct 04 03:42:57 Starting compiler/encoders/ag32/proofs
Oct 04 03:45:53 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Oct 04 03:45:54 Starting compiler/backend/x64/proofs
Oct 04 03:46:43 Finished compiler/backend/x64/proofs                             48s   2GB
Oct 04 03:46:44 Starting compiler/backend/arm7/proofs
Oct 04 03:47:32 Finished compiler/backend/arm7/proofs                            47s   2GB
Oct 04 03:47:33 Starting compiler/backend/arm8/proofs
Oct 04 03:48:18 Finished compiler/backend/arm8/proofs                            44s   3GB
Oct 04 03:48:19 Starting compiler/backend/arm8_asl
Oct 04 03:48:50 Finished compiler/backend/arm8_asl                               29s   2GB
Oct 04 03:48:51 Starting compiler/backend/mips/proofs
Oct 04 03:49:40 Finished compiler/backend/mips/proofs                            48s   3GB
Oct 04 03:49:41 Starting compiler/backend/riscv/proofs
Oct 04 03:50:38 Finished compiler/backend/riscv/proofs                           56s   4GB
Oct 04 03:50:39 Starting compiler/backend/ag32/proofs
Oct 04 04:05:01 Finished compiler/backend/ag32/proofs                         14m21s   6GB
Oct 04 04:05:02 Starting compiler/backend/cv_compute
Oct 04 04:06:54 Finished compiler/backend/cv_compute                           1m51s   3GB
Oct 04 04:06:55 Starting cv_translator
Oct 04 04:26:54 Finished cv_translator                                        19m57s  10GB
Oct 04 04:26:54 Starting candle/set-theory
Oct 04 04:27:42 Finished candle/set-theory                                       46s   1GB
Oct 04 04:27:43 Starting candle/syntax-lib
Oct 04 04:27:45 Finished candle/syntax-lib                                        0s  69MB
Oct 04 04:27:45 Starting candle/standard/syntax
Oct 04 04:28:06 Finished candle/standard/syntax                                  19s   1GB
Oct 04 04:28:07 Starting candle/standard/semantics
Oct 04 04:30:58 Finished candle/standard/semantics                             2m50s   4GB
Oct 04 04:30:59 Starting candle/standard/monadic
Oct 04 04:31:00 Finished candle/standard/monadic                                  0s 106MB
Oct 04 04:31:01 Starting candle/standard/ml_kernel
Oct 04 04:33:07 Finished candle/standard/ml_kernel                             2m05s   5GB
Oct 04 04:33:08 Starting candle/overloading/syntax
Oct 04 04:36:44 Finished candle/overloading/syntax                             3m35s   2GB
Oct 04 04:36:45 Starting candle/overloading/semantics
Oct 04 04:48:22 Finished candle/overloading/semantics                         11m35s   6GB
Oct 04 04:48:23 Starting candle/overloading/monadic
Oct 04 04:50:49 Finished candle/overloading/monadic                            2m25s   2GB
Oct 04 04:50:50 Starting candle/overloading/ml_kernel
Oct 04 04:59:01 Finished candle/overloading/ml_kernel                          8m10s   6GB
Oct 04 04:59:02 Starting candle/overloading/ml_checker
Oct 04 05:01:46 Finished candle/overloading/ml_checker                         2m43s   7GB
Oct 04 05:01:47 Starting candle/prover
Oct 04 05:12:25 Finished candle/prover                                        10m36s   5GB
Oct 04 05:12:26 Starting pancake
Oct 04 05:12:53 Finished pancake                                                 26s 994MB
Oct 04 05:12:54 Starting pancake/ffi
Oct 04 05:12:55 Finished pancake/ffi                                              0s  23MB
Oct 04 05:12:56 Starting pancake/semantics
Oct 04 05:15:11 Finished pancake/semantics                                     2m13s   3GB
Oct 04 05:15:12 Starting pancake/parser
Oct 04 05:15:35 Finished pancake/parser                                          22s 598MB
Oct 04 05:15:36 Starting pancake/proofs
Oct 04 05:31:51 Finished pancake/proofs                                       16m13s   6GB
Oct 04 05:31:52 Starting compiler/dafny
Oct 04 05:34:30 Finished compiler/dafny                                        2m37s   7GB
Oct 04 05:34:31 Starting compiler/dafny/translation
Oct 04 06:03:02 Finished compiler/dafny/translation                           28m30s  14GB
Oct 04 06:03:03 Starting compiler/dafny/compilation
Oct 04 06:06:41 Finished compiler/dafny/compilation                            3m36s  15GB
Oct 04 06:06:42 Starting compiler/dafny/semantics
Oct 04 06:07:20 Finished compiler/dafny/semantics                                36s   1GB
Oct 04 06:07:21 Starting characteristic/examples
Oct 04 06:08:52 Finished characteristic/examples                               1m30s   5GB
Oct 04 06:08:53 Starting tutorial/solutions
Oct 04 06:11:39 Finished tutorial/solutions                                    2m45s   5GB
Oct 04 06:11:40 Starting translator/monadic/examples
Oct 04 06:14:46 Finished translator/monadic/examples                           3m04s   4GB
Oct 04 06:14:47 Starting examples
Oct 04 06:27:16 Finished examples                                             12m28s   5GB
Oct 04 06:27:17 Starting examples/compilation/x64
Oct 04 06:37:18 Finished examples/compilation/x64                              9m59s   6GB
Oct 04 06:37:19 Starting examples/compilation/x64/proofs
Oct 04 06:42:12 Finished examples/compilation/x64/proofs                       4m52s   8GB
Oct 04 06:42:13 Starting examples/compilation/ag32
Oct 04 06:45:04 Finished examples/compilation/ag32                             2m50s   5GB
Oct 04 06:45:05 Starting examples/compilation/ag32/proofs
Oct 04 06:47:03 Finished examples/compilation/ag32/proofs                      1m56s   8GB
Oct 04 06:47:04 Starting examples/compilation/to_word
Oct 04 06:51:22 Finished examples/compilation/to_word                          4m17s  14GB
Oct 04 06:51:23 Starting examples/lpr_checker
Oct 04 06:51:55 Finished examples/lpr_checker                                    30s   1GB
Oct 04 06:51:56 Starting examples/lpr_checker/array
Oct 04 07:18:41 Finished examples/lpr_checker/array                           26m44s  29GB
Oct 04 07:18:42 Starting examples/lpr_checker/array/compilation
Oct 04 07:21:22 Finished examples/lpr_checker/array/compilation                2m38s  10GB
Oct 04 07:21:22 Starting examples/lpr_checker/array/compilation/proofs
Oct 04 07:23:28 Finished examples/lpr_checker/array/compilation/proofs         2m04s   9GB
Oct 04 07:23:29 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 04 07:25:25 Finished examples/lpr_checker/array/compilation/proofsARM8     1m54s   8GB
Oct 04 07:25:26 Starting examples/xlrup_checker
Oct 04 07:26:02 Finished examples/xlrup_checker                                  35s   1GB
Oct 04 07:26:03 Starting examples/xlrup_checker/array
Oct 04 07:39:15 Finished examples/xlrup_checker/array                         13m11s  11GB
Oct 04 07:39:15 Starting examples/xlrup_checker/array/compilation
Oct 04 07:40:46 Finished examples/xlrup_checker/array/compilation              1m29s   7GB
Oct 04 07:40:47 Starting examples/xlrup_checker/array/compilation/proofs
Oct 04 07:42:41 Finished examples/xlrup_checker/array/compilation/proofs       1m52s   7GB
Oct 04 07:42:41 Starting examples/pseudo_bool
Oct 04 07:44:08 Finished examples/pseudo_bool                                  1m25s   1GB
Oct 04 07:44:09 Starting examples/pseudo_bool/cnf_encoding
Oct 04 07:44:51 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Oct 04 07:44:52 Starting examples/pseudo_bool/graph_encoding
Oct 04 07:45:48 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 04 07:45:48 Starting examples/pseudo_bool/array
Oct 04 08:49:52 Finished examples/pseudo_bool/array                         1h04m02s  27GB
Oct 04 08:49:53 Starting examples/pseudo_bool/array/compilation
Oct 04 09:04:02 Finished examples/pseudo_bool/array/compilation               14m08s  32GB
Oct 04 09:04:03 Starting examples/pseudo_bool/array/compilation/proofs
Oct 04 09:08:31 Finished examples/pseudo_bool/array/compilation/proofs         4m27s  10GB
Oct 04 09:08:32 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 04 09:10:28 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m54s   9GB
Oct 04 09:10:28 Starting examples/opentheory
Oct 04 09:19:19 Finished examples/opentheory                                   8m49s   5GB
Oct 04 09:19:20 Starting examples/opentheory
Oct 04 09:19:22 Finished examples/opentheory                                      1s 126MB
Oct 04 09:19:23 Starting examples/opentheory/compilation
Oct 04 09:21:31 Finished examples/opentheory/compilation                       2m07s   9GB
Oct 04 09:21:32 Starting examples/opentheory/compilation/proofs
Oct 04 09:23:24 Finished examples/opentheory/compilation/proofs                1m51s   8GB
Oct 04 09:23:25 Starting examples/opentheory/compilation/ag32
Oct 04 09:25:42 Finished examples/opentheory/compilation/ag32                  2m15s   8GB
Oct 04 09:25:43 Starting examples/opentheory/compilation/ag32/proofs
Oct 04 09:28:20 Finished examples/opentheory/compilation/ag32/proofs           2m36s   9GB
Oct 04 09:28:21 Starting examples/sat_encodings
Oct 04 09:29:24 Finished examples/sat_encodings                                1m01s 910MB
Oct 04 09:29:25 Starting examples/sat_encodings/case_studies
Oct 04 09:31:38 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 04 09:31:39 Starting examples/sat_encodings/translation
Oct 04 09:35:24 Finished examples/sat_encodings/translation                    3m43s   6GB
Oct 04 09:35:25 Starting examples/sat_encodings/translation/compilation
Oct 04 09:37:56 Finished examples/sat_encodings/translation/compilation        2m30s   7GB
Oct 04 09:37:57 Starting examples/deflate
Oct 04 09:38:25 Finished examples/deflate                                        27s 743MB
Oct 04 09:38:26 Starting examples/deflate/translation
Oct 04 09:39:28 Finished examples/deflate/translation                          1m00s   2GB
Oct 04 09:39:29 Starting examples/deflate/translation/compilation
Oct 04 09:40:39 Finished examples/deflate/translation/compilation              1m08s   6GB
Oct 04 09:40:40 Starting examples/vipr
Oct 04 09:44:25 Finished examples/vipr                                         3m44s   4GB
Oct 04 09:44:26 Starting examples/vipr/compilation
Oct 04 09:45:47 Finished examples/vipr/compilation                             1m19s   6GB
Oct 04 09:45:48 Starting translator/okasaki-examples
Oct 04 09:50:08 Finished translator/okasaki-examples                           4m19s   4GB
Oct 04 09:50:09 Starting translator/other-examples
Oct 04 09:55:14 Finished translator/other-examples                             5m04s   3GB
Oct 04 09:55:15 Starting compiler/parsing/tests
Oct 04 09:55:54 Finished compiler/parsing/tests                                  38s   2GB
Oct 04 09:55:55 Starting compiler/inference/tests
Oct 04 09:56:43 Finished compiler/inference/tests                                47s   3GB
Oct 04 09:56:44 Starting compiler/printing/test
Oct 04 09:58:22 Finished compiler/printing/test                                1m37s   7GB
Oct 04 09:58:23 Starting icing/flover
Oct 04 10:35:31 Finished icing/flover                                         37m06s   4GB
Oct 04 10:35:32 Starting icing/
Oct 04 11:03:40 Finished icing/                                               28m07s   9GB
Oct 04 11:03:41 Starting icing/examples
Oct 04 11:05:36 Finished icing/examples                                        1m53s   9GB
Oct 04 11:05:37 Starting compiler/repl
Oct 04 11:14:52 Finished compiler/repl                                         9m13s  10GB
Oct 04 11:14:53 Starting unverified/sexpr-bootstrap/x64/64
Oct 04 11:28:57 Finished unverified/sexpr-bootstrap/x64/64                    14m03s  17GB
Oct 04 11:28:58 Starting unverified/sexpr-bootstrap/x64/32
Oct 04 11:39:48 Finished unverified/sexpr-bootstrap/x64/32                    10m49s  15GB
Oct 04 11:39:49 Starting compiler/benchmarks
Oct 04 11:40:34 Finished compiler/benchmarks                                     44s 710MB
Oct 04 11:40:35 Starting compiler/bootstrap/compilation/x64/64
Oct 04 12:27:53 Finished compiler/bootstrap/compilation/x64/64                47m16s 139GB
Oct 04 12:27:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 04 12:53:10 Finished compiler/bootstrap/compilation/x64/64/proofs         25m14s  51GB
Oct 04 12:53:11 Starting compiler/bootstrap/compilation/x64/32
Oct 04 13:52:35 Finished compiler/bootstrap/compilation/x64/32                59m22s  77GB
Oct 04 13:52:36 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 04 13:57:57 Finished compiler/bootstrap/compilation/x64/32/proofs          5m19s  24GB
Oct 04 13:57:58 Starting compiler/bootstrap/compilation/arm8/64
Oct 04 14:58:39 Finished compiler/bootstrap/compilation/arm8/64             1h00m40s 138GB
Oct 04 14:58:40 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 04 15:04:56 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m14s  30GB
Oct 04 15:04:56 Starting compiler/bootstrap/compilation/ag32/32
Oct 04 15:48:43 Finished compiler/bootstrap/compilation/ag32/32               43m45s 110GB
Oct 04 15:48:44 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 04 15:54:37 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m52s  32GB
Oct 04 15:54:38 SUCCESS