Job 2243

CakeML:a3cf8bbd5a03c4d19450fb325126bd37f2cfffe1
  Get a proof to build with an exclude_simps [Nov 29 19:13:45]
#975 (byte)
Merging into:8ac36a22c960a9f4aaae14aa89dabaf177cd63fa
  Merge pull request #974 from CakeML/dominance [Nov 15 15:00:12]
HOL:8f74c6afc449d7002c926d75228bd4ecb539d82f
  Allow type vars in cv_typesLib functions [Nov 19 10:16:00]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Nov 29 19:19:46 Claimed job
Nov 29 19:19:51 Reusing HOL
Nov 29 19:20:32 Starting developers
Nov 29 19:20:37 Finished developers                                               5s 122MB
Nov 29 19:20:37 Starting developers/bin
Nov 29 19:20:43 Finished developers/bin                                           5s   1GB
Nov 29 19:20:44 Starting compiler/proofs
Nov 29 21:11:25 Finished compiler/proofs                                    1h50m41s  19GB
Nov 29 21:11:26 Starting compiler/bootstrap/translation
Nov 30 05:26:20 Finished compiler/bootstrap/translation                     8h14m54s  51GB
Nov 30 05:26:20 Starting semantics/ffi
Nov 30 05:26:26 Finished semantics/ffi                                            5s 215MB
Nov 30 05:26:26 Starting semantics
Nov 30 05:26:28 Finished semantics                                                1s  17MB
Nov 30 05:26:28 Starting semantics/proofs
Nov 30 05:27:03 Finished semantics/proofs                                        35s 723MB
Nov 30 05:27:03 Starting semantics/alt_semantics
Nov 30 05:27:36 Finished semantics/alt_semantics                                 32s 879MB
Nov 30 05:27:36 Starting semantics/alt_semantics/proofs
Nov 30 05:39:26 Finished semantics/alt_semantics/proofs                       11m50s   1GB
Nov 30 05:39:26 Starting basis/pure
Nov 30 05:39:28 Finished basis/pure                                               1s  18MB
Nov 30 05:39:28 Starting translator
Nov 30 05:41:17 Finished translator                                            1m48s   1GB
Nov 30 05:41:17 Starting compiler/parsing
Nov 30 05:41:19 Finished compiler/parsing                                         1s  18MB
Nov 30 05:41:19 Starting characteristic
Nov 30 05:41:21 Finished characteristic                                           1s  27MB
Nov 30 05:41:21 Starting translator/monadic
Nov 30 05:41:23 Finished translator/monadic                                       2s  24MB
Nov 30 05:41:24 Starting basis
Nov 30 05:45:08 Finished basis                                                 3m44s   3GB
Nov 30 05:45:08 Starting compiler/inference
Nov 30 05:45:10 Finished compiler/inference                                       1s  21MB
Nov 30 05:45:10 Starting compiler/backend/reg_alloc
Nov 30 05:45:12 Finished compiler/backend/reg_alloc                               1s  25MB
Nov 30 05:45:12 Starting compiler/backend/gc
Nov 30 05:45:14 Finished compiler/backend/gc                                      2s  22MB
Nov 30 05:45:14 Starting compiler/backend
Nov 30 05:45:26 Finished compiler/backend                                        11s 741MB
Nov 30 05:45:27 Starting compiler/encoders/asm
Nov 30 05:45:28 Finished compiler/encoders/asm                                    1s  21MB
Nov 30 05:45:28 Starting compiler/encoders/x64
Nov 30 05:45:30 Finished compiler/encoders/x64                                    1s  24MB
Nov 30 05:45:30 Starting compiler/encoders/arm7
Nov 30 05:45:32 Finished compiler/encoders/arm7                                   1s  24MB
Nov 30 05:45:32 Starting compiler/encoders/arm8
Nov 30 05:45:34 Finished compiler/encoders/arm8                                   1s  24MB
Nov 30 05:45:34 Starting compiler/encoders/arm8_asl
Nov 30 05:48:46 Finished compiler/encoders/arm8_asl                            3m11s   1GB
Nov 30 05:48:46 Starting compiler/encoders/mips
Nov 30 05:48:48 Finished compiler/encoders/mips                                   1s  21MB
Nov 30 05:48:48 Starting compiler/encoders/riscv
Nov 30 05:48:50 Finished compiler/encoders/riscv                                  1s  24MB
Nov 30 05:48:50 Starting compiler/encoders/ag32
Nov 30 05:48:52 Finished compiler/encoders/ag32                                   1s  26MB
Nov 30 05:48:52 Starting compiler/backend/x64
Nov 30 05:48:54 Finished compiler/backend/x64                                     2s  24MB
Nov 30 05:48:54 Starting compiler/backend/arm7
Nov 30 05:48:57 Finished compiler/backend/arm7                                    2s  23MB
Nov 30 05:48:57 Starting compiler/backend/arm8
Nov 30 05:48:59 Finished compiler/backend/arm8                                    2s  22MB
Nov 30 05:48:59 Starting compiler/backend/mips
Nov 30 05:49:01 Finished compiler/backend/mips                                    2s  23MB
Nov 30 05:49:01 Starting compiler/backend/riscv
Nov 30 05:49:04 Finished compiler/backend/riscv                                   2s  30MB
Nov 30 05:49:04 Starting compiler/backend/ag32
Nov 30 05:50:28 Finished compiler/backend/ag32                                 1m24s   1GB
Nov 30 05:50:28 Starting compiler/parsing/proofs
Nov 30 05:50:30 Finished compiler/parsing/proofs                                  1s  19MB
Nov 30 05:50:30 Starting compiler/inference/proofs
Nov 30 05:50:32 Finished compiler/inference/proofs                                1s  22MB
Nov 30 05:50:32 Starting compiler/backend/semantics
Nov 30 05:51:47 Finished compiler/backend/semantics                            1m14s   1GB
Nov 30 05:51:47 Starting compiler/backend/reg_alloc/proofs
Nov 30 05:51:49 Finished compiler/backend/reg_alloc/proofs                        1s  26MB
Nov 30 05:51:49 Starting compiler/backend/proofs
Nov 30 05:52:48 Finished compiler/backend/proofs                                 59s   2GB
Nov 30 05:52:48 Starting compiler/backend/serialiser
Nov 30 05:52:51 Finished compiler/backend/serialiser                              2s  29MB
Nov 30 05:52:51 Starting compiler/encoders/x64/proofs
Nov 30 06:02:40 Finished compiler/encoders/x64/proofs                          9m49s   5GB
Nov 30 06:02:41 Starting compiler/encoders/arm7/proofs
Nov 30 06:16:31 Finished compiler/encoders/arm7/proofs                        13m50s   4GB
Nov 30 06:16:32 Starting compiler/encoders/arm8/proofs
Nov 30 06:23:30 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Nov 30 06:23:30 Starting compiler/encoders/arm8_asl/proofs
Nov 30 06:39:33 Finished compiler/encoders/arm8_asl/proofs                    16m02s   1GB
Nov 30 06:39:33 Starting compiler/encoders/mips/proofs
Nov 30 06:50:14 Finished compiler/encoders/mips/proofs                        10m40s   2GB
Nov 30 06:50:14 Starting compiler/encoders/riscv/proofs
Nov 30 06:59:16 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Nov 30 06:59:16 Starting compiler/encoders/ag32/proofs
Nov 30 07:01:46 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Nov 30 07:01:46 Starting compiler/backend/x64/proofs
Nov 30 07:02:15 Finished compiler/backend/x64/proofs                             29s   1GB
Nov 30 07:02:15 Starting compiler/backend/arm7/proofs
Nov 30 07:02:50 Finished compiler/backend/arm7/proofs                            34s   2GB
Nov 30 07:02:50 Starting compiler/backend/arm8/proofs
Nov 30 07:03:20 Finished compiler/backend/arm8/proofs                            29s   1GB
Nov 30 07:03:20 Starting compiler/backend/arm8_asl
Nov 30 07:03:45 Finished compiler/backend/arm8_asl                               24s   1GB
Nov 30 07:03:45 Starting compiler/backend/mips/proofs
Nov 30 07:04:16 Finished compiler/backend/mips/proofs                            31s   2GB
Nov 30 07:04:17 Starting compiler/backend/riscv/proofs
Nov 30 07:04:50 Finished compiler/backend/riscv/proofs                           33s   1GB
Nov 30 07:04:50 Starting compiler/backend/ag32/proofs
Nov 30 07:18:28 Finished compiler/backend/ag32/proofs                         13m37s   3GB
Nov 30 07:18:28 Starting candle/set-theory
Nov 30 07:19:08 Finished candle/set-theory                                       39s   1GB
Nov 30 07:19:08 Starting candle/syntax-lib
Nov 30 07:19:10 Finished candle/syntax-lib                                        1s  18MB
Nov 30 07:19:10 Starting candle/standard/syntax
Nov 30 07:19:20 Finished candle/standard/syntax                                  10s 547MB
Nov 30 07:19:20 Starting candle/standard/semantics
Nov 30 07:21:20 Finished candle/standard/semantics                             1m59s   1GB
Nov 30 07:21:20 Starting candle/standard/monadic
Nov 30 07:21:22 Finished candle/standard/monadic                                  1s  29MB
Nov 30 07:21:22 Starting candle/standard/ml_kernel
Nov 30 07:23:03 Finished candle/standard/ml_kernel                             1m41s   3GB
Nov 30 07:23:03 Starting candle/overloading/syntax
Nov 30 07:26:27 Finished candle/overloading/syntax                             3m23s   1GB
Nov 30 07:26:28 Starting candle/overloading/semantics
Nov 30 07:38:59 Finished candle/overloading/semantics                         12m31s   2GB
Nov 30 07:38:59 Starting candle/overloading/monadic
Nov 30 07:41:43 Finished candle/overloading/monadic                            2m43s   2GB
Nov 30 07:41:43 Starting candle/overloading/ml_kernel
Nov 30 07:49:42 Finished candle/overloading/ml_kernel                          7m58s   3GB
Nov 30 07:49:42 Starting candle/overloading/ml_checker
Nov 30 07:52:17 Finished candle/overloading/ml_checker                         2m34s   3GB
Nov 30 07:52:17 Starting candle/prover
Nov 30 08:02:27 Finished candle/prover                                        10m09s   3GB
Nov 30 08:02:27 Starting pancake
Nov 30 08:03:09 Finished pancake                                                 42s 872MB
Nov 30 08:03:09 Starting pancake/ffi
Nov 30 08:03:10 Finished pancake/ffi                                              0s  13MB
Nov 30 08:03:10 Starting pancake/semantics
Nov 30 08:05:36 Finished pancake/semantics                                     2m26s   1GB
Nov 30 08:05:36 Starting pancake/parser
Nov 30 08:05:59 Finished pancake/parser                                          22s 613MB
Nov 30 08:05:59 Starting pancake/proofs
Nov 30 08:39:33 Finished pancake/proofs                                       33m33s   5GB
Nov 30 08:39:33 Starting characteristic/examples
Nov 30 08:41:09 Finished characteristic/examples                               1m35s   3GB
Nov 30 08:41:09 Starting tutorial/solutions
Nov 30 08:56:28 Finished tutorial/solutions                                   15m18s   9GB
Nov 30 08:56:28 Starting translator/monadic/examples
Nov 30 09:00:28 Finished translator/monadic/examples                           4m00s   2GB
Nov 30 09:00:28 Starting examples
Nov 30 09:16:10 Finished examples                                             15m41s   4GB
Nov 30 09:16:10 Starting examples/compilation/x64
Nov 30 11:18:14 Finished examples/compilation/x64                           2h02m03s  17GB
Nov 30 11:18:14 Starting examples/compilation/x64/proofs
Nov 30 11:20:47 Finished examples/compilation/x64/proofs                       2m32s   4GB
Nov 30 11:20:47 Starting examples/compilation/ag32
Nov 30 11:51:12 Finished examples/compilation/ag32                            30m24s  10GB
Nov 30 11:51:12 Starting examples/compilation/ag32/proofs
Nov 30 11:52:15 Finished examples/compilation/ag32/proofs                      1m02s   5GB
Nov 30 11:52:15 Starting examples/compilation/to_word
Nov 30 11:55:49 Finished examples/compilation/to_word                          3m34s   7GB
Nov 30 11:55:50 Starting examples/lpr_checker
Nov 30 11:56:55 Finished examples/lpr_checker                                  1m05s   1GB
Nov 30 11:56:55 Starting examples/lpr_checker/array
Nov 30 12:27:59 Finished examples/lpr_checker/array                           31m03s   6GB
Nov 30 12:27:59 Starting examples/lpr_checker/array/compilation
Nov 30 13:20:16 Finished examples/lpr_checker/array/compilation               52m16s  23GB
Nov 30 13:20:16 Starting examples/lpr_checker/array/compilation/proofs
Nov 30 13:22:21 Finished examples/lpr_checker/array/compilation/proofs         2m05s   3GB
Nov 30 13:22:21 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 30 13:28:01 Finished examples/lpr_checker/array/compilation/proofsARM8     5m39s  19GB
Nov 30 13:28:01 Starting examples/pseudo_bool
Nov 30 13:29:50 Finished examples/pseudo_bool                                  1m48s   1GB
Nov 30 13:29:50 Starting examples/pseudo_bool/cnf_encoding
Nov 30 13:30:15 Finished examples/pseudo_bool/cnf_encoding                       24s 691MB
Nov 30 13:30:15 Starting examples/pseudo_bool/graph_encoding
Nov 30 13:30:58 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Nov 30 13:30:58 Starting examples/pseudo_bool/array
Nov 30 14:24:25 Finished examples/pseudo_bool/array                           53m27s   5GB
Nov 30 14:24:26 Starting examples/pseudo_bool/array/compilation
Nov 30 17:21:08 Finished examples/pseudo_bool/array/compilation             2h56m41s  31GB
Nov 30 17:21:08 Starting examples/pseudo_bool/array/compilation/proofs
Nov 30 17:23:52 Finished examples/pseudo_bool/array/compilation/proofs         2m44s   5GB
Nov 30 17:23:52 Starting examples/opentheory
Nov 30 17:34:57 Finished examples/opentheory                                  11m04s   3GB
Nov 30 17:34:57 Starting examples/opentheory
Nov 30 17:34:59 Finished examples/opentheory                                      1s  32MB
Nov 30 17:34:59 Starting examples/opentheory/compilation
Nov 30 18:12:17 Finished examples/opentheory/compilation                      37m17s  32GB
Nov 30 18:12:17 Starting examples/opentheory/compilation/proofs
Nov 30 18:13:21 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Nov 30 18:13:21 Starting examples/opentheory/compilation/ag32
Nov 30 18:47:28 Finished examples/opentheory/compilation/ag32                 34m07s  30GB
Nov 30 18:47:28 Starting examples/opentheory/compilation/ag32/proofs
Nov 30 18:49:25 Finished examples/opentheory/compilation/ag32/proofs           1m56s   4GB
Nov 30 18:49:25 Starting examples/sat_encodings
Nov 30 18:51:29 Finished examples/sat_encodings                                2m03s 923MB
Nov 30 18:51:29 Starting examples/sat_encodings/case_studies
Nov 30 18:53:13 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Nov 30 18:53:13 Starting examples/sat_encodings/translation
Nov 30 18:59:33 Finished examples/sat_encodings/translation                    6m19s   4GB
Nov 30 18:59:33 Starting examples/sat_encodings/translation/compilation
Nov 30 19:46:45 Finished examples/sat_encodings/translation/compilation       47m11s  21GB
Nov 30 19:46:45 Starting examples/deflate
Nov 30 19:47:46 Finished examples/deflate                                      1m01s 923MB
Nov 30 19:47:46 Starting examples/deflate/translation
Nov 30 19:49:29 Finished examples/deflate/translation                          1m42s   3GB
Nov 30 19:49:30 Starting examples/deflate/translation/compilation
Nov 30 20:10:15 Finished examples/deflate/translation/compilation             20m45s  13GB
Nov 30 20:10:15 Starting examples/vipr
Nov 30 20:14:26 Finished examples/vipr                                         4m10s   6GB
Nov 30 20:14:26 Starting examples/vipr/compilation
Nov 30 20:35:10 Finished examples/vipr/compilation                            20m43s  16GB
Nov 30 20:35:10 Starting translator/okasaki-examples
Nov 30 20:40:21 Finished translator/okasaki-examples                           5m10s   2GB
Nov 30 20:40:21 Starting translator/other-examples
Nov 30 20:41:16 Finished translator/other-examples                               54s   1GB
Nov 30 20:41:16 Starting compiler/parsing/tests
Nov 30 20:41:48 Finished compiler/parsing/tests                                  31s 749MB
Nov 30 20:41:48 Starting compiler/inference/tests
Nov 30 20:50:25 Finished compiler/inference/tests                              8m37s   5GB
Nov 30 20:50:25 Starting compiler/printing/test
Nov 30 20:54:20 Finished compiler/printing/test                                3m54s   3GB
Nov 30 20:54:20 Starting icing/flover
Nov 30 21:37:54 Finished icing/flover                                         43m33s   2GB
Nov 30 21:37:54 Starting icing/
Nov 30 22:32:02 Finished icing/                                               54m08s   7GB
Nov 30 22:32:02 Starting icing/examples
Nov 30 22:33:38 Finished icing/examples                                        1m35s   3GB
Nov 30 22:33:38 Starting compiler/repl
Nov 30 22:42:20 Finished compiler/repl                                         8m41s   5GB
Nov 30 22:42:20 Starting unverified/sexpr-bootstrap/x64/64
Nov 30 22:55:56 Finished unverified/sexpr-bootstrap/x64/64                    13m35s  17GB
Nov 30 22:55:56 Starting unverified/sexpr-bootstrap/x64/32
Nov 30 23:06:59 Finished unverified/sexpr-bootstrap/x64/32                    11m02s  14GB
Nov 30 23:06:59 Starting compiler/benchmarks
Nov 30 23:22:37 Finished compiler/benchmarks                                  15m38s   2GB
Nov 30 23:22:38 Starting compiler/bootstrap/compilation/x64/64
Dec 01 12:21:26 Finished compiler/bootstrap/compilation/x64/64             12h58m48s  64GB
Dec 01 12:21:26 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 01 12:42:13 Finished compiler/bootstrap/compilation/x64/64/proofs         20m46s  25GB
Dec 01 12:42:13 Starting compiler/bootstrap/compilation/x64/32
Dec 01 19:52:52 Finished compiler/bootstrap/compilation/x64/32              7h10m38s  64GB
Dec 01 19:52:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 01 19:55:56 Finished compiler/bootstrap/compilation/x64/32/proofs          3m03s  19GB
Dec 01 19:55:56 Starting compiler/bootstrap/compilation/ag32/32
Dec 02 03:14:51 Finished compiler/bootstrap/compilation/ag32/32             7h18m54s  64GB
Dec 02 03:14:51 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 02 03:21:45 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m54s  31GB
Dec 02 03:21:45 SUCCESS