Job 2780

CakeML:5e6f98b3390abfaeecc7cd0fbe2e1e50da3842fe
  Update to account for changed Dafny IR [Mar 01 17:06:39]
#1137 (dafny-ast-update)
Merging into:e0e8a40f04c4ebbce02bc7e9b654ca2c547f79ce
  Merge pull request #1129 from CakeML/remove_Misc_bool_case_eq [Feb 07 15:04:17]
HOL:79c5bf49ec3e47d70f7fb818d4a20de1baac3b3a
  Remove cv_rep_add and use [cv_rep] annotation instead [Mar 04 23:35:28]
Machine:pavlova

Mar 06 07:35:02 Claimed job
Mar 06 07:35:09 Reusing HOL
Mar 06 07:35:20 Starting developers
Mar 06 07:35:24 Finished developers                                               3s 198MB
Mar 06 07:35:25 Starting developers/bin
Mar 06 07:35:31 Finished developers/bin                                           5s 746MB
Mar 06 07:35:32 Starting misc
Mar 06 07:36:16 Finished misc                                                    42s   2GB
Mar 06 07:36:16 Starting compiler/proofs
Mar 06 09:15:40 Finished compiler/proofs                                    1h39m22s  34GB
Mar 06 09:15:41 Starting compiler/bootstrap/translation
Mar 06 15:01:16 Finished compiler/bootstrap/translation                     5h45m33s  91GB
Mar 06 15:01:17 Starting semantics/ffi
Mar 06 15:01:27 Finished semantics/ffi                                            9s 590MB
Mar 06 15:01:28 Starting semantics
Mar 06 15:01:29 Finished semantics                                                0s  54MB
Mar 06 15:01:30 Starting semantics/proofs
Mar 06 15:01:53 Finished semantics/proofs                                        21s 861MB
Mar 06 15:01:53 Starting semantics/alt_semantics
Mar 06 15:02:14 Finished semantics/alt_semantics                                 20s 895MB
Mar 06 15:02:15 Starting semantics/alt_semantics/proofs
Mar 06 15:12:28 Finished semantics/alt_semantics/proofs                       10m12s   3GB
Mar 06 15:12:29 Starting basis/pure
Mar 06 15:12:31 Finished basis/pure                                               0s  94MB
Mar 06 15:12:32 Starting translator
Mar 06 15:14:02 Finished translator                                            1m29s   3GB
Mar 06 15:14:03 Starting compiler/parsing
Mar 06 15:14:05 Finished compiler/parsing                                         0s  57MB
Mar 06 15:14:06 Starting characteristic
Mar 06 15:14:08 Finished characteristic                                           1s 120MB
Mar 06 15:14:09 Starting translator/monadic
Mar 06 15:14:11 Finished translator/monadic                                       1s 115MB
Mar 06 15:14:12 Starting translator/monadic/monad_base
Mar 06 15:14:13 Finished translator/monadic/monad_base                            0s  51MB
Mar 06 15:14:14 Starting basis
Mar 06 15:16:33 Finished basis                                                 2m18s   3GB
Mar 06 15:16:34 Starting compiler
Mar 06 15:16:37 Finished compiler                                                 1s 208MB
Mar 06 15:16:38 Starting compiler/inference
Mar 06 15:16:40 Finished compiler/inference                                       1s 114MB
Mar 06 15:16:41 Starting compiler/backend/reg_alloc
Mar 06 15:16:42 Finished compiler/backend/reg_alloc                               0s  57MB
Mar 06 15:16:43 Starting compiler/backend/gc
Mar 06 15:16:45 Finished compiler/backend/gc                                      1s 147MB
Mar 06 15:16:46 Starting compiler/backend
Mar 06 15:16:51 Finished compiler/backend                                         4s 239MB
Mar 06 15:16:52 Starting compiler/encoders/asm
Mar 06 15:16:54 Finished compiler/encoders/asm                                    0s  86MB
Mar 06 15:16:55 Starting compiler/encoders/x64
Mar 06 15:16:56 Finished compiler/encoders/x64                                    0s  86MB
Mar 06 15:16:57 Starting compiler/encoders/arm7
Mar 06 15:16:59 Finished compiler/encoders/arm7                                   0s  90MB
Mar 06 15:17:00 Starting compiler/encoders/arm8
Mar 06 15:17:01 Finished compiler/encoders/arm8                                   0s  89MB
Mar 06 15:17:02 Starting compiler/encoders/arm8_asl
Mar 06 17:18:37 Finished compiler/encoders/arm8_asl                         2h01m33s  43GB
Mar 06 17:18:38 Starting compiler/encoders/mips
Mar 06 17:18:40 Finished compiler/encoders/mips                                   0s  88MB
Mar 06 17:18:41 Starting compiler/encoders/riscv
Mar 06 17:18:42 Finished compiler/encoders/riscv                                  0s  84MB
Mar 06 17:18:43 Starting compiler/encoders/ag32
Mar 06 17:18:45 Finished compiler/encoders/ag32                                   0s  87MB
Mar 06 17:18:46 Starting compiler/encoders/tests
Mar 06 17:18:48 Finished compiler/encoders/tests                                  1s 112MB
Mar 06 17:18:49 Starting compiler/encoders/monadic_enc
Mar 06 17:18:51 Finished compiler/encoders/monadic_enc                            1s 140MB
Mar 06 17:18:52 Starting compiler/backend/x64
Mar 06 17:18:54 Finished compiler/backend/x64                                     1s 137MB
Mar 06 17:18:55 Starting compiler/backend/arm7
Mar 06 17:18:57 Finished compiler/backend/arm7                                    1s 137MB
Mar 06 17:18:58 Starting compiler/backend/arm8
Mar 06 17:19:00 Finished compiler/backend/arm8                                    1s 137MB
Mar 06 17:19:01 Starting compiler/backend/mips
Mar 06 17:19:03 Finished compiler/backend/mips                                    1s 136MB
Mar 06 17:19:04 Starting compiler/backend/riscv
Mar 06 17:19:06 Finished compiler/backend/riscv                                   1s 137MB
Mar 06 17:19:07 Starting compiler/backend/ag32
Mar 06 17:20:11 Finished compiler/backend/ag32                                 1m03s   1GB
Mar 06 17:20:12 Starting compiler/backend/pattern_matching
Mar 06 17:20:13 Finished compiler/backend/pattern_matching                        0s  53MB
Mar 06 17:20:14 Starting compiler/parsing/ocaml
Mar 06 17:21:55 Finished compiler/parsing/ocaml                                1m39s   1GB
Mar 06 17:21:56 Starting compiler/printing
Mar 06 17:21:58 Finished compiler/printing                                        1s 117MB
Mar 06 17:21:58 Starting compiler/parsing/proofs
Mar 06 17:22:00 Finished compiler/parsing/proofs                                  0s  65MB
Mar 06 17:22:01 Starting compiler/inference/proofs
Mar 06 17:22:03 Finished compiler/inference/proofs                                1s 113MB
Mar 06 17:22:04 Starting compiler/backend/semantics
Mar 06 17:25:08 Finished compiler/backend/semantics                            3m02s   2GB
Mar 06 17:25:09 Starting compiler/backend/reg_alloc/proofs
Mar 06 17:25:11 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Mar 06 17:25:11 Starting compiler/backend/proofs
Mar 06 17:25:57 Finished compiler/backend/proofs                                 44s   2GB
Mar 06 17:25:58 Starting compiler/backend/serialiser
Mar 06 17:26:00 Finished compiler/backend/serialiser                              1s 151MB
Mar 06 17:26:01 Starting compiler/encoders/x64/proofs
Mar 06 17:36:12 Finished compiler/encoders/x64/proofs                         10m09s   4GB
Mar 06 17:36:12 Starting compiler/encoders/arm7/proofs
Mar 06 17:49:07 Finished compiler/encoders/arm7/proofs                        12m53s   5GB
Mar 06 17:49:08 Starting compiler/encoders/arm8/proofs
Mar 06 17:56:06 Finished compiler/encoders/arm8/proofs                         6m57s   4GB
Mar 06 17:56:07 Starting compiler/encoders/arm8_asl/proofs
Mar 06 18:45:02 Finished compiler/encoders/arm8_asl/proofs                    48m53s  18GB
Mar 06 18:45:02 Starting compiler/encoders/mips/proofs
Mar 06 18:55:19 Finished compiler/encoders/mips/proofs                        10m15s   8GB
Mar 06 18:55:20 Starting compiler/encoders/riscv/proofs
Mar 06 19:03:26 Finished compiler/encoders/riscv/proofs                        8m05s   4GB
Mar 06 19:03:27 Starting compiler/encoders/ag32/proofs
Mar 06 19:06:18 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Mar 06 19:06:19 Starting compiler/backend/x64/proofs
Mar 06 19:06:53 Finished compiler/backend/x64/proofs                             32s   2GB
Mar 06 19:06:54 Starting compiler/backend/arm7/proofs
Mar 06 19:07:27 Finished compiler/backend/arm7/proofs                            32s   2GB
Mar 06 19:07:28 Starting compiler/backend/arm8/proofs
Mar 06 19:07:58 Finished compiler/backend/arm8/proofs                            29s   2GB
Mar 06 19:07:59 Starting compiler/backend/arm8_asl
Mar 06 19:08:22 Finished compiler/backend/arm8_asl                               21s   2GB
Mar 06 19:08:23 Starting compiler/backend/mips/proofs
Mar 06 19:08:55 Finished compiler/backend/mips/proofs                            31s   2GB
Mar 06 19:08:56 Starting compiler/backend/riscv/proofs
Mar 06 19:09:28 Finished compiler/backend/riscv/proofs                           31s   2GB
Mar 06 19:09:29 Starting compiler/backend/ag32/proofs
Mar 06 19:23:09 Finished compiler/backend/ag32/proofs                         13m39s   5GB
Mar 06 19:23:10 Starting compiler/backend/cv_compute
Mar 06 19:24:20 Finished compiler/backend/cv_compute                           1m08s   2GB
Mar 06 19:24:20 Starting cv_translator
Mar 06 19:45:15 Finished cv_translator                                        20m52s  12GB
Mar 06 19:45:15 Starting candle
Mar 06 19:45:16 Finished candle                                                   0s  11MB
Mar 06 19:45:17 Starting candle/set-theory
Mar 06 19:45:52 Finished candle/set-theory                                       34s   1GB
Mar 06 19:45:53 Starting candle/syntax-lib
Mar 06 19:45:55 Finished candle/syntax-lib                                        0s  95MB
Mar 06 19:45:56 Starting candle/standard
Mar 06 19:45:57 Finished candle/standard                                          0s  12MB
Mar 06 19:45:58 Starting candle/standard/syntax
Mar 06 19:46:11 Finished candle/standard/syntax                                  11s 807MB
Mar 06 19:46:12 Starting candle/standard/semantics
Mar 06 19:48:10 Finished candle/standard/semantics                             1m57s   2GB
Mar 06 19:48:11 Starting candle/standard/monadic
Mar 06 19:48:13 Finished candle/standard/monadic                                  1s 120MB
Mar 06 19:48:14 Starting candle/standard/ml_kernel
Mar 06 19:49:59 Finished candle/standard/ml_kernel                             1m44s   4GB
Mar 06 19:50:00 Starting candle/standard/ml_kernel/lisp
Mar 06 19:50:01 Finished candle/standard/ml_kernel/lisp                           0s  47MB
Mar 06 19:50:02 Starting candle/overloading
Mar 06 19:50:03 Finished candle/overloading                                       0s  12MB
Mar 06 19:50:04 Starting candle/overloading/syntax
Mar 06 19:53:11 Finished candle/overloading/syntax                             3m06s   2GB
Mar 06 19:53:12 Starting candle/overloading/semantics
Mar 06 20:04:08 Finished candle/overloading/semantics                         10m54s   4GB
Mar 06 20:04:09 Starting candle/overloading/monadic
Mar 06 20:06:28 Finished candle/overloading/monadic                            2m18s   2GB
Mar 06 20:06:29 Starting candle/overloading/ml_kernel
Mar 06 20:13:35 Finished candle/overloading/ml_kernel                          7m05s   5GB
Mar 06 20:13:36 Starting candle/overloading/ml_checker
Mar 06 20:15:44 Finished candle/overloading/ml_checker                         2m06s   6GB
Mar 06 20:15:45 Starting candle/prover
Mar 06 20:25:17 Finished candle/prover                                         9m31s   5GB
Mar 06 20:25:18 Starting candle/prover/compute
Mar 06 20:25:20 Finished candle/prover/compute                                    1s 153MB
Mar 06 20:25:21 Starting pancake
Mar 06 20:25:43 Finished pancake                                                 21s 845MB
Mar 06 20:25:44 Starting pancake/semantics
Mar 06 20:27:53 Finished pancake/semantics                                     2m07s   2GB
Mar 06 20:27:54 Starting pancake/parser
Mar 06 20:28:17 Finished pancake/parser                                          22s 476MB
Mar 06 20:28:18 Starting pancake/proofs
Mar 06 20:44:15 Finished pancake/proofs                                       15m56s   6GB
Mar 06 20:44:16 Starting pancake/ta_progs
Mar 06 20:44:17 Finished pancake/ta_progs                                         0s  11MB
Mar 06 20:44:18 Starting compiler/dafny
Mar 06 20:47:11 Finished compiler/dafny                                        2m51s  11GB
Mar 06 20:47:12 Starting compiler/dafny/translation
Mar 06 21:06:26 Finished compiler/dafny/translation                           19m12s  20GB
Mar 06 21:06:27 Starting compiler/dafny/compilation
Mar 06 21:09:22 Finished compiler/dafny/compilation                            2m54s  11GB
Mar 06 21:09:23 Starting compiler/dafny/semantics
Mar 06 21:09:59 Finished compiler/dafny/semantics                                35s   1GB
Mar 06 21:10:00 Starting characteristic/examples
Mar 06 21:11:25 Finished characteristic/examples                               1m24s   4GB
Mar 06 21:11:26 Starting tutorial/solutions
Mar 06 21:13:52 Finished tutorial/solutions                                    2m25s   4GB
Mar 06 21:13:53 Starting translator/monadic/examples
Mar 06 21:16:44 Finished translator/monadic/examples                           2m50s   3GB
Mar 06 21:16:45 Starting examples
Mar 06 21:22:48 Finished examples                                              6m01s   5GB
Mar 06 21:22:49 Starting examples/compilation
Mar 06 21:22:50 Finished examples/compilation                                     0s  11MB
Mar 06 21:22:51 Starting examples/compilation/x64
Mar 06 21:29:45 Finished examples/compilation/x64                              6m52s   4GB
Mar 06 21:29:45 Starting examples/compilation/x64/proofs
Mar 06 21:32:11 Finished examples/compilation/x64/proofs                       2m24s   4GB
Mar 06 21:32:12 Starting examples/compilation/ag32
Mar 06 21:34:06 Finished examples/compilation/ag32                             1m53s   3GB
Mar 06 21:34:07 Starting examples/compilation/ag32/proofs
Mar 06 21:35:08 Finished examples/compilation/ag32/proofs                        59s   5GB
Mar 06 21:35:09 Starting examples/lpr_checker
Mar 06 21:35:39 Finished examples/lpr_checker                                    29s   1GB
Mar 06 21:35:40 Starting examples/lpr_checker/array
Mar 06 22:01:40 Finished examples/lpr_checker/array                           25m59s  28GB
Mar 06 22:01:41 Starting examples/lpr_checker/array/compilation
Mar 06 23:06:38 Finished examples/lpr_checker/array/compilation             1h04m55s 253GB
Mar 06 23:06:39 Starting examples/lpr_checker/array/compilation/proofs
Mar 06 23:08:11 Finished examples/lpr_checker/array/compilation/proofs         1m30s   6GB
Mar 06 23:08:12 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 06 23:09:20 Finished examples/lpr_checker/array/compilation/proofsARM8     1m06s   6GB
Mar 06 23:09:21 Starting .
Mar 06 23:09:24 Finished .                                                        2s 296MB
Mar 06 23:09:25 Starting examples/xlrup_checker
Mar 06 23:10:00 Finished examples/xlrup_checker                                  33s   1GB
Mar 06 23:10:01 Starting examples/xlrup_checker/array
Mar 06 23:22:47 Finished examples/xlrup_checker/array                         12m45s   7GB
Mar 06 23:22:48 Starting examples/xlrup_checker/array/compilation
Mar 06 23:23:57 Finished examples/xlrup_checker/array/compilation              1m08s   3GB
Mar 06 23:23:58 Starting examples/xlrup_checker/array/compilation/proofs
Mar 06 23:24:56 Finished examples/xlrup_checker/array/compilation/proofs         57s   5GB
Mar 06 23:24:57 Starting examples/pseudo_bool
Mar 06 23:26:28 Finished examples/pseudo_bool                                  1m29s   2GB
Mar 06 23:26:29 Starting examples/pseudo_bool/cnf_encoding
Mar 06 23:26:58 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Mar 06 23:26:59 Starting examples/pseudo_bool/graph_encoding
Mar 06 23:27:45 Finished examples/pseudo_bool/graph_encoding                     44s   2GB
Mar 06 23:27:46 Starting examples/pseudo_bool/array
Mar 07 00:35:10 Finished examples/pseudo_bool/array                         1h07m22s  39GB
Mar 07 00:35:10 Starting examples/pseudo_bool/array/compilation
Mar 07 00:44:41 Finished examples/pseudo_bool/array/compilation                9m29s  18GB
Mar 07 00:44:42 Starting examples/pseudo_bool/array/compilation/proofs
Mar 07 00:47:16 Finished examples/pseudo_bool/array/compilation/proofs         2m33s   7GB
Mar 07 00:47:17 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 07 00:48:29 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m11s   6GB
Mar 07 00:48:30 Starting examples/opentheory
Mar 07 00:57:06 Finished examples/opentheory                                   8m35s   5GB
Mar 07 00:57:07 Starting examples/opentheory/compilation
Mar 07 00:58:42 Finished examples/opentheory/compilation                       1m33s   6GB
Mar 07 00:58:42 Starting examples/opentheory/compilation/proofs
Mar 07 00:59:42 Finished examples/opentheory/compilation/proofs                  58s   5GB
Mar 07 00:59:43 Starting examples/opentheory/compilation/ag32
Mar 07 01:01:21 Finished examples/opentheory/compilation/ag32                  1m36s   7GB
Mar 07 01:01:22 Starting examples/opentheory/compilation/ag32/proofs
Mar 07 01:03:01 Finished examples/opentheory/compilation/ag32/proofs           1m37s   7GB
Mar 07 01:03:02 Starting examples/sat_encodings
Mar 07 01:04:00 Finished examples/sat_encodings                                  57s 826MB
Mar 07 01:04:01 Starting examples/sat_encodings/demo
Mar 07 01:04:02 Finished examples/sat_encodings/demo                              0s  10MB
Mar 07 01:04:03 Starting examples/sat_encodings/case_studies
Mar 07 01:05:48 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Mar 07 01:05:49 Starting examples/sat_encodings/translation
Mar 07 01:09:27 Finished examples/sat_encodings/translation                    3m37s   2GB
Mar 07 01:09:28 Starting examples/sat_encodings/translation/compilation
Mar 07 01:11:23 Finished examples/sat_encodings/translation/compilation        1m54s   4GB
Mar 07 01:11:24 Starting examples/deflate
Mar 07 01:11:52 Finished examples/deflate                                        26s 752MB
Mar 07 01:11:53 Starting examples/deflate/translation
Mar 07 01:12:59 Finished examples/deflate/translation                          1m05s   4GB
Mar 07 01:13:00 Starting examples/deflate/translation/compilation
Mar 07 01:13:52 Finished examples/deflate/translation/compilation                50s   3GB
Mar 07 01:13:54 Starting examples/vipr
Mar 07 01:17:28 Finished examples/vipr                                         3m31s   7GB
Mar 07 01:17:29 Starting examples/vipr/compilation
Mar 07 01:18:27 Finished examples/vipr/compilation                               56s   4GB
Mar 07 01:18:28 Starting translator/okasaki-examples
Mar 07 01:22:29 Finished translator/okasaki-examples                           3m59s   3GB
Mar 07 01:22:30 Starting translator/other-examples
Mar 07 01:25:33 Finished translator/other-examples                             3m02s   2GB
Mar 07 01:25:33 Starting translator/other-examples/auxiliary
Mar 07 01:25:34 Finished translator/other-examples/auxiliary                      0s  12MB
Mar 07 01:25:35 Starting compiler/parsing/tests
Mar 07 01:26:10 Finished compiler/parsing/tests                                  34s   1GB
Mar 07 01:26:11 Starting compiler/inference/tests
Mar 07 01:26:47 Finished compiler/inference/tests                                35s   2GB
Mar 07 01:26:48 Starting compiler/printing/test
Mar 07 01:27:57 Finished compiler/printing/test                                1m08s   3GB
Mar 07 01:27:58 Starting icing/flover
Mar 07 02:02:33 Finished icing/flover                                         34m34s   2GB
Mar 07 02:02:34 Starting icing/flover/Infra
Mar 07 02:02:35 Finished icing/flover/Infra                                       0s  11MB
Mar 07 02:02:36 Starting icing/flover/semantics
Mar 07 02:02:37 Finished icing/flover/semantics                                   0s  12MB
Mar 07 02:02:38 Starting icing/
Mar 07 02:29:30 Finished icing/                                               26m51s   4GB
Mar 07 02:29:31 Starting icing/examples
Mar 07 02:31:02 Finished icing/examples                                        1m29s   8GB
Mar 07 02:31:02 Starting compiler/repl
Mar 07 02:38:55 Finished compiler/repl                                         7m51s   6GB
Mar 07 02:38:56 Starting unverified/sexpr-bootstrap/x64/64
Mar 07 02:43:01 Finished unverified/sexpr-bootstrap/x64/64                     4m04s  15GB
Mar 07 02:43:02 Starting unverified/sexpr-bootstrap/x64/32
Mar 07 02:46:18 Finished unverified/sexpr-bootstrap/x64/32                     3m14s  14GB
Mar 07 02:46:19 Starting compiler/benchmarks
Mar 07 02:47:05 Finished compiler/benchmarks                                     45s 712MB
Mar 07 02:47:06 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 07 02:47:09 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 271MB
Mar 07 02:47:10 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 07 02:47:14 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 253MB
Mar 07 02:47:15 Starting compiler/bootstrap/compilation/x64/64
Mar 07 03:15:18 Finished compiler/bootstrap/compilation/x64/64                28m01s  93GB
Mar 07 03:15:18 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 07 03:38:53 Finished compiler/bootstrap/compilation/x64/64/proofs         23m33s  43GB
Mar 07 03:38:53 Starting compiler/bootstrap/compilation/x64/32
Mar 07 04:05:57 Finished compiler/bootstrap/compilation/x64/32                27m02s  75GB
Mar 07 04:05:58 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 07 04:10:11 Finished compiler/bootstrap/compilation/x64/32/proofs          4m11s  23GB
Mar 07 04:10:11 Starting compiler/bootstrap/compilation/arm8/64
Mar 07 04:50:16 Finished compiler/bootstrap/compilation/arm8/64               40m03s 109GB
Mar 07 04:50:17 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 07 04:55:32 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m14s  29GB
Mar 07 04:55:33 Starting compiler/bootstrap/compilation/ag32/32
Mar 07 05:25:56 Finished compiler/bootstrap/compilation/ag32/32               30m22s  83GB
Mar 07 05:25:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 07 05:30:38 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m39s  30GB
Mar 07 05:30:39 SUCCESS