Job 2653

CakeML:5c7a0c29a09cbcc3bbae63316a68df949b73f518
  Remove val foo = Q.prove(..) automatically [Oct 13 08:15:21]
#1069 (remove-simple-qprove)
Merging into:b9843ac59b40ad1a8adc0dfdfcd5e0656f44ab6e
  Merge pull request #1064 from CakeML/remove-define [Oct 10 11:32:18]
HOL:4d1b16443810923d9832780d757d1b868bc9eef4
  cv translator: allow known fun types in ctors [Oct 09 12:54:25]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Oct 14 21:21:01 Claimed job
Oct 14 21:21:06 Reusing HOL
Oct 14 21:21:51 Starting developers
Oct 14 21:21:57 Finished developers                                               6s 111MB
Oct 14 21:21:57 Starting developers/bin
Oct 14 21:22:04 Finished developers/bin                                           6s   1GB
Oct 14 21:22:04 Starting compiler/proofs
Oct 14 23:17:19 Finished compiler/proofs                                    1h55m14s  20GB
Oct 14 23:17:19 Starting compiler/bootstrap/translation
Oct 15 08:15:01 Finished compiler/bootstrap/translation                     8h57m42s  53GB
Oct 15 08:15:01 Starting semantics/ffi
Oct 15 08:15:07 Finished semantics/ffi                                            5s 410MB
Oct 15 08:15:07 Starting semantics
Oct 15 08:15:09 Finished semantics                                                1s  19MB
Oct 15 08:15:09 Starting semantics/proofs
Oct 15 08:15:35 Finished semantics/proofs                                        25s 415MB
Oct 15 08:15:35 Starting semantics/alt_semantics
Oct 15 08:15:58 Finished semantics/alt_semantics                                 23s 524MB
Oct 15 08:15:58 Starting semantics/alt_semantics/proofs
Oct 15 08:27:37 Finished semantics/alt_semantics/proofs                       11m38s   1GB
Oct 15 08:27:37 Starting basis/pure
Oct 15 08:27:38 Finished basis/pure                                               1s  19MB
Oct 15 08:27:38 Starting translator
Oct 15 08:29:20 Finished translator                                            1m41s   1GB
Oct 15 08:29:20 Starting compiler/parsing
Oct 15 08:29:22 Finished compiler/parsing                                         1s  17MB
Oct 15 08:29:22 Starting characteristic
Oct 15 08:29:24 Finished characteristic                                           1s  21MB
Oct 15 08:29:24 Starting translator/monadic
Oct 15 08:29:26 Finished translator/monadic                                       1s  26MB
Oct 15 08:29:26 Starting basis
Oct 15 08:32:02 Finished basis                                                 2m35s   2GB
Oct 15 08:32:02 Starting compiler/inference
Oct 15 08:32:04 Finished compiler/inference                                       1s  21MB
Oct 15 08:32:04 Starting compiler/backend/reg_alloc
Oct 15 08:32:05 Finished compiler/backend/reg_alloc                               1s  17MB
Oct 15 08:32:05 Starting compiler/backend/gc
Oct 15 08:32:08 Finished compiler/backend/gc                                      2s  26MB
Oct 15 08:32:08 Starting compiler/backend
Oct 15 08:32:13 Finished compiler/backend                                         5s 271MB
Oct 15 08:32:13 Starting compiler/encoders/asm
Oct 15 08:32:15 Finished compiler/encoders/asm                                    1s  22MB
Oct 15 08:32:15 Starting compiler/encoders/x64
Oct 15 08:32:17 Finished compiler/encoders/x64                                    1s  21MB
Oct 15 08:32:17 Starting compiler/encoders/arm7
Oct 15 08:32:19 Finished compiler/encoders/arm7                                   1s  28MB
Oct 15 08:32:19 Starting compiler/encoders/arm8
Oct 15 08:32:21 Finished compiler/encoders/arm8                                   1s  20MB
Oct 15 08:32:21 Starting compiler/encoders/arm8_asl
Oct 15 08:35:26 Finished compiler/encoders/arm8_asl                            3m04s   1GB
Oct 15 08:35:26 Starting compiler/encoders/mips
Oct 15 08:35:28 Finished compiler/encoders/mips                                   1s  22MB
Oct 15 08:35:28 Starting compiler/encoders/riscv
Oct 15 08:35:30 Finished compiler/encoders/riscv                                  1s  25MB
Oct 15 08:35:30 Starting compiler/encoders/ag32
Oct 15 08:35:32 Finished compiler/encoders/ag32                                   1s  23MB
Oct 15 08:35:32 Starting compiler/backend/x64
Oct 15 08:35:34 Finished compiler/backend/x64                                     2s  25MB
Oct 15 08:35:34 Starting compiler/backend/arm7
Oct 15 08:35:37 Finished compiler/backend/arm7                                    2s  29MB
Oct 15 08:35:37 Starting compiler/backend/arm8
Oct 15 08:35:39 Finished compiler/backend/arm8                                    2s  29MB
Oct 15 08:35:39 Starting compiler/backend/mips
Oct 15 08:35:41 Finished compiler/backend/mips                                    2s  23MB
Oct 15 08:35:41 Starting compiler/backend/riscv
Oct 15 08:35:44 Finished compiler/backend/riscv                                   2s  22MB
Oct 15 08:35:44 Starting compiler/backend/ag32
Oct 15 08:36:56 Finished compiler/backend/ag32                                 1m12s   1GB
Oct 15 08:36:57 Starting compiler/parsing/proofs
Oct 15 08:36:58 Finished compiler/parsing/proofs                                  1s  17MB
Oct 15 08:36:58 Starting compiler/inference/proofs
Oct 15 08:37:00 Finished compiler/inference/proofs                                1s  20MB
Oct 15 08:37:00 Starting compiler/backend/semantics
Oct 15 08:40:32 Finished compiler/backend/semantics                            3m32s   1GB
Oct 15 08:40:33 Starting compiler/backend/reg_alloc/proofs
Oct 15 08:40:35 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Oct 15 08:40:35 Starting compiler/backend/proofs
Oct 15 08:41:28 Finished compiler/backend/proofs                                 53s   2GB
Oct 15 08:41:28 Starting compiler/backend/serialiser
Oct 15 08:41:31 Finished compiler/backend/serialiser                              2s  23MB
Oct 15 08:41:31 Starting compiler/encoders/x64/proofs
Oct 15 08:52:16 Finished compiler/encoders/x64/proofs                         10m45s   4GB
Oct 15 08:52:17 Starting compiler/encoders/arm7/proofs
Oct 15 13:54:34 Resuming compiler/encoders/arm7/proofs
Oct 16 04:37:18 Finished compiler/encoders/arm7/proofs                     14h42m44s   7GB
Oct 16 04:37:19 Starting compiler/encoders/arm8/proofs
Oct 16 04:44:58 Finished compiler/encoders/arm8/proofs                         7m39s   1GB
Oct 16 04:44:58 Starting compiler/encoders/arm8_asl/proofs
Oct 16 05:02:21 Finished compiler/encoders/arm8_asl/proofs                    17m23s   2GB
Oct 16 05:02:21 Starting compiler/encoders/mips/proofs
Oct 16 05:13:04 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Oct 16 05:13:04 Starting compiler/encoders/riscv/proofs
Oct 16 05:22:04 Finished compiler/encoders/riscv/proofs                        8m59s   2GB
Oct 16 05:22:04 Starting compiler/encoders/ag32/proofs
Oct 16 05:25:23 Finished compiler/encoders/ag32/proofs                         3m19s   1GB
Oct 16 05:25:23 Starting compiler/backend/x64/proofs
Oct 16 05:25:57 Finished compiler/backend/x64/proofs                             33s   2GB
Oct 16 05:25:57 Starting compiler/backend/arm7/proofs
Oct 16 05:26:32 Finished compiler/backend/arm7/proofs                            34s   1GB
Oct 16 05:26:32 Starting compiler/backend/arm8/proofs
Oct 16 05:27:04 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 16 05:27:05 Starting compiler/backend/arm8_asl
Oct 16 05:27:29 Finished compiler/backend/arm8_asl                               24s   2GB
Oct 16 05:27:29 Starting compiler/backend/mips/proofs
Oct 16 05:28:03 Finished compiler/backend/mips/proofs                            34s   2GB
Oct 16 05:28:03 Starting compiler/backend/riscv/proofs
Oct 16 05:28:39 Finished compiler/backend/riscv/proofs                           35s   2GB
Oct 16 05:28:39 Starting compiler/backend/ag32/proofs
Oct 16 05:43:38 Finished compiler/backend/ag32/proofs                         14m58s   3GB
Oct 16 05:43:38 Starting compiler/backend/cv_compute
Oct 16 05:44:55 Finished compiler/backend/cv_compute                           1m17s   1GB
Oct 16 05:44:56 Starting cv_translator
Oct 16 06:05:51 Finished cv_translator                                        20m55s   6GB
Oct 16 06:05:51 Starting candle/set-theory
Oct 16 06:06:29 Finished candle/set-theory                                       37s   1GB
Oct 16 06:06:29 Starting candle/syntax-lib
Oct 16 06:06:30 Finished candle/syntax-lib                                        1s  22MB
Oct 16 06:06:31 Starting candle/standard/syntax
Oct 16 06:06:44 Finished candle/standard/syntax                                  13s 838MB
Oct 16 06:06:44 Starting candle/standard/semantics
Oct 16 06:08:56 Finished candle/standard/semantics                             2m12s   1GB
Oct 16 06:08:56 Starting candle/standard/monadic
Oct 16 06:08:58 Finished candle/standard/monadic                                  1s  22MB
Oct 16 06:08:58 Starting candle/standard/ml_kernel
Oct 16 06:10:46 Finished candle/standard/ml_kernel                             1m47s   3GB
Oct 16 06:10:46 Starting candle/overloading/syntax
Oct 16 06:14:15 Finished candle/overloading/syntax                             3m29s   1GB
Oct 16 06:14:16 Starting candle/overloading/semantics
Oct 16 06:26:52 Finished candle/overloading/semantics                         12m35s   2GB
Oct 16 06:26:52 Starting candle/overloading/monadic
Oct 16 06:29:21 Finished candle/overloading/monadic                            2m29s   1GB
Oct 16 06:29:21 Starting candle/overloading/ml_kernel
Oct 16 06:37:42 Finished candle/overloading/ml_kernel                          8m21s   3GB
Oct 16 06:37:42 Starting candle/overloading/ml_checker
Oct 16 06:40:44 Finished candle/overloading/ml_checker                         3m01s   2GB
Oct 16 06:40:44 Starting candle/prover
Oct 16 06:51:09 Finished candle/prover                                        10m24s   3GB
Oct 16 06:51:09 Starting pancake
Oct 16 06:51:35 Finished pancake                                                 25s 834MB
Oct 16 06:51:35 Starting pancake/ffi
Oct 16 06:51:35 Finished pancake/ffi                                              0s  13MB
Oct 16 06:51:35 Starting pancake/semantics
Oct 16 06:54:00 Finished pancake/semantics                                     2m24s   1GB
Oct 16 06:54:01 Starting pancake/parser
Oct 16 06:54:27 Finished pancake/parser                                          26s 419MB
Oct 16 06:54:27 Starting pancake/proofs
Oct 16 07:12:47 Finished pancake/proofs                                       18m20s   3GB
Oct 16 07:12:47 Starting compiler/dafny
Oct 16 07:15:13 Finished compiler/dafny                                        2m25s   8GB
Oct 16 07:15:13 Starting compiler/dafny/translation
Oct 16 07:45:21 Finished compiler/dafny/translation                           30m08s  16GB
Oct 16 07:45:21 Starting compiler/dafny/compilation
Oct 16 07:48:45 Finished compiler/dafny/compilation                            3m24s  11GB
Oct 16 07:48:45 Starting compiler/dafny/semantics
Oct 16 07:49:23 Finished compiler/dafny/semantics                                37s 824MB
Oct 16 07:49:23 Starting characteristic/examples
Oct 16 07:50:54 Finished characteristic/examples                               1m31s   2GB
Oct 16 07:50:54 Starting tutorial/solutions
Oct 16 07:53:42 Finished tutorial/solutions                                    2m47s   3GB
Oct 16 07:53:42 Starting translator/monadic/examples
Oct 16 07:57:19 Finished translator/monadic/examples                           3m37s   3GB
Oct 16 07:57:19 Starting examples
Oct 16 08:11:55 Finished examples                                             14m36s   3GB
Oct 16 08:11:55 Starting examples/compilation/x64
Oct 16 08:21:06 Finished examples/compilation/x64                              9m10s   5GB
Oct 16 08:21:06 Starting examples/compilation/x64/proofs
Oct 16 08:24:05 Finished examples/compilation/x64/proofs                       2m59s   4GB
Oct 16 08:24:06 Starting examples/compilation/ag32
Oct 16 08:26:21 Finished examples/compilation/ag32                             2m15s   3GB
Oct 16 08:26:21 Starting examples/compilation/ag32/proofs
Oct 16 08:27:36 Finished examples/compilation/ag32/proofs                      1m14s   5GB
Oct 16 08:27:36 Starting examples/compilation/to_word
Oct 16 08:31:15 Finished examples/compilation/to_word                          3m38s   5GB
Oct 16 08:31:15 Starting examples/lpr_checker
Oct 16 08:31:48 Finished examples/lpr_checker                                    32s 556MB
Oct 16 08:31:48 Starting examples/lpr_checker/array
Oct 16 09:01:37 Finished examples/lpr_checker/array                           29m48s   4GB
Oct 16 09:01:37 Starting examples/lpr_checker/array/compilation
Oct 16 09:04:36 Finished examples/lpr_checker/array/compilation                2m59s   8GB
Oct 16 09:04:36 Starting examples/lpr_checker/array/compilation/proofs
Oct 16 09:06:02 Finished examples/lpr_checker/array/compilation/proofs         1m25s   6GB
Oct 16 09:06:02 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 16 09:07:21 Finished examples/lpr_checker/array/compilation/proofsARM8     1m18s   7GB
Oct 16 09:07:21 Starting examples/xlrup_checker
Oct 16 09:07:59 Finished examples/xlrup_checker                                  37s 813MB
Oct 16 09:07:59 Starting examples/xlrup_checker/array
Oct 16 09:23:02 Finished examples/xlrup_checker/array                         15m03s   2GB
Oct 16 09:23:02 Starting examples/xlrup_checker/array/compilation
Oct 16 09:24:27 Finished examples/xlrup_checker/array/compilation              1m24s   5GB
Oct 16 09:24:27 Starting examples/xlrup_checker/array/compilation/proofs
Oct 16 09:25:34 Finished examples/xlrup_checker/array/compilation/proofs       1m07s   5GB
Oct 16 09:25:34 Starting examples/pseudo_bool
Oct 16 09:27:14 Finished examples/pseudo_bool                                  1m39s   1GB
Oct 16 09:27:14 Starting examples/pseudo_bool/cnf_encoding
Oct 16 09:27:44 Finished examples/pseudo_bool/cnf_encoding                       30s 945MB
Oct 16 09:27:44 Starting examples/pseudo_bool/graph_encoding
Oct 16 09:28:31 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Oct 16 09:28:31 Starting examples/pseudo_bool/array
Oct 16 10:46:39 Finished examples/pseudo_bool/array                         1h18m07s   6GB
Oct 16 10:46:39 Starting examples/pseudo_bool/array/compilation
Oct 16 11:06:12 Finished examples/pseudo_bool/array/compilation               19m32s  24GB
Oct 16 11:06:12 Starting examples/pseudo_bool/array/compilation/proofs
Oct 16 11:09:36 Finished examples/pseudo_bool/array/compilation/proofs         3m23s   7GB
Oct 16 11:09:36 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 16 11:10:59 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m23s   7GB
Oct 16 11:10:59 Starting examples/opentheory
Oct 16 11:20:39 Finished examples/opentheory                                   9m39s   2GB
Oct 16 11:20:39 Starting examples/opentheory
Oct 16 11:20:41 Finished examples/opentheory                                      1s  25MB
Oct 16 11:20:41 Starting examples/opentheory/compilation
Oct 16 11:22:49 Finished examples/opentheory/compilation                       2m08s   5GB
Oct 16 11:22:49 Starting examples/opentheory/compilation/proofs
Oct 16 11:23:58 Finished examples/opentheory/compilation/proofs                1m08s   4GB
Oct 16 11:23:58 Starting examples/opentheory/compilation/ag32
Oct 16 11:26:07 Finished examples/opentheory/compilation/ag32                  2m09s   5GB
Oct 16 11:26:07 Starting examples/opentheory/compilation/ag32/proofs
Oct 16 11:27:56 Finished examples/opentheory/compilation/ag32/proofs           1m48s   7GB
Oct 16 11:27:56 Starting examples/sat_encodings
Oct 16 11:29:07 Finished examples/sat_encodings                                1m10s 448MB
Oct 16 11:29:07 Starting examples/sat_encodings/case_studies
Oct 16 11:31:10 Finished examples/sat_encodings/case_studies                   2m02s   1GB
Oct 16 11:31:10 Starting examples/sat_encodings/translation
Oct 16 11:35:32 Finished examples/sat_encodings/translation                    4m21s   1GB
Oct 16 11:35:32 Starting examples/sat_encodings/translation/compilation
Oct 16 11:38:05 Finished examples/sat_encodings/translation/compilation        2m33s   5GB
Oct 16 11:38:05 Starting examples/deflate
Oct 16 11:38:38 Finished examples/deflate                                        32s 518MB
Oct 16 11:38:38 Starting examples/deflate/translation
Oct 16 11:39:52 Finished examples/deflate/translation                          1m13s   1GB
Oct 16 11:39:52 Starting examples/deflate/translation/compilation
Oct 16 11:41:07 Finished examples/deflate/translation/compilation              1m15s   4GB
Oct 16 11:41:07 Starting examples/vipr
Oct 16 11:45:10 Finished examples/vipr                                         4m02s   4GB
Oct 16 11:45:10 Starting examples/vipr/compilation
Oct 16 11:46:26 Finished examples/vipr/compilation                             1m15s   4GB
Oct 16 11:46:26 Starting translator/okasaki-examples
Oct 16 11:52:04 Finished translator/okasaki-examples                           5m37s   2GB
Oct 16 11:52:04 Starting translator/other-examples
Oct 16 11:57:08 Finished translator/other-examples                             5m03s   1GB
Oct 16 11:57:08 Starting compiler/parsing/tests
Oct 16 11:57:49 Finished compiler/parsing/tests                                  41s 879MB
Oct 16 11:57:49 Starting compiler/inference/tests
Oct 16 11:58:23 Finished compiler/inference/tests                                34s   2GB
Oct 16 11:58:24 Starting compiler/printing/test
Oct 16 12:00:02 Finished compiler/printing/test                                1m38s   2GB
Oct 16 12:00:02 Starting icing/flover
Oct 16 12:48:03 Finished icing/flover                                         48m00s   2GB
Oct 16 12:48:03 Starting icing/
Oct 16 13:18:16 Finished icing/                                               30m13s   4GB
Oct 16 13:18:16 Starting icing/examples
Oct 16 13:19:59 Finished icing/examples                                        1m42s   5GB
Oct 16 13:20:00 Starting compiler/repl
Oct 16 13:29:15 Finished compiler/repl                                         9m14s   8GB
Oct 16 13:29:15 Starting unverified/sexpr-bootstrap/x64/64
Oct 16 13:45:53 Finished unverified/sexpr-bootstrap/x64/64                    16m38s  16GB
Oct 16 13:45:54 Starting unverified/sexpr-bootstrap/x64/32
Oct 16 13:58:51 Finished unverified/sexpr-bootstrap/x64/32                    12m57s  13GB
Oct 16 13:58:51 Starting compiler/benchmarks
Oct 16 14:14:34 Finished compiler/benchmarks                                  15m43s   2GB
Oct 16 14:14:35 Starting compiler/bootstrap/compilation/x64/64
Oct 16 14:55:20 Finished compiler/bootstrap/compilation/x64/64                40m45s  63GB
Oct 16 14:55:20 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 16 15:20:06 Finished compiler/bootstrap/compilation/x64/64/proofs         24m45s  53GB
Oct 16 15:20:06 Starting compiler/bootstrap/compilation/x64/32
Oct 16 15:55:45 Finished compiler/bootstrap/compilation/x64/32                35m39s  63GB
Oct 16 15:55:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 16 16:02:01 Finished compiler/bootstrap/compilation/x64/32/proofs          6m15s  19GB
Oct 16 16:02:01 Starting compiler/bootstrap/compilation/arm8/64
Oct 16 17:00:01 Finished compiler/bootstrap/compilation/arm8/64               57m59s  64GB
Oct 16 17:00:01 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 16 17:07:26 Finished compiler/bootstrap/compilation/arm8/64/proofs         7m24s  25GB
Oct 16 17:07:26 Starting compiler/bootstrap/compilation/ag32/32
Oct 16 17:51:01 Finished compiler/bootstrap/compilation/ag32/32               43m34s  64GB
Oct 16 17:51:01 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 16 17:57:54 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m53s  21GB
Oct 16 17:57:55 SUCCESS