Job 2775

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:65933ef783406de318821e34715c171c761cf3dc
  [probability] indep_functions_of_four_vars [Feb 21 09:48:55]
Machine:pavlova

Mar 04 07:56:11 Claimed job
Mar 04 07:56:20 Building HOL
Mar 04 08:07:08 Starting developers
Mar 04 08:07:12 Finished developers                                               3s 205MB
Mar 04 08:07:13 Starting developers/bin
Mar 04 08:07:20 Finished developers/bin                                           5s 746MB
Mar 04 08:07:21 Starting misc
Mar 04 08:08:19 Finished misc                                                    57s   2GB
Mar 04 08:08:20 Starting compiler/proofs
Mar 04 09:47:30 Finished compiler/proofs                                    1h39m07s  49GB
Mar 04 09:47:31 Starting compiler/bootstrap/translation
Mar 04 15:32:44 Finished compiler/bootstrap/translation                     5h45m11s  58GB
Mar 04 15:32:45 Starting semantics/ffi
Mar 04 15:32:55 Finished semantics/ffi                                            8s 603MB
Mar 04 15:32:56 Starting semantics
Mar 04 15:32:57 Finished semantics                                                0s  54MB
Mar 04 15:32:58 Starting semantics/proofs
Mar 04 15:33:21 Finished semantics/proofs                                        21s 855MB
Mar 04 15:33:22 Starting semantics/alt_semantics
Mar 04 15:33:42 Finished semantics/alt_semantics                                 19s 904MB
Mar 04 15:33:43 Starting semantics/alt_semantics/proofs
Mar 04 15:43:59 Finished semantics/alt_semantics/proofs                       10m14s   2GB
Mar 04 15:44:00 Starting basis/pure
Mar 04 15:44:01 Finished basis/pure                                               0s  94MB
Mar 04 15:44:02 Starting translator
Mar 04 15:45:38 Finished translator                                            1m34s   2GB
Mar 04 15:45:39 Starting compiler/parsing
Mar 04 15:45:40 Finished compiler/parsing                                         0s  57MB
Mar 04 15:45:41 Starting characteristic
Mar 04 15:45:43 Finished characteristic                                           1s 120MB
Mar 04 15:45:44 Starting translator/monadic
Mar 04 15:45:46 Finished translator/monadic                                       1s 115MB
Mar 04 15:45:47 Starting translator/monadic/monad_base
Mar 04 15:45:48 Finished translator/monadic/monad_base                            0s  51MB
Mar 04 15:45:49 Starting basis
Mar 04 15:48:10 Finished basis                                                 2m19s   3GB
Mar 04 15:48:11 Starting compiler
Mar 04 15:48:13 Finished compiler                                                 1s 206MB
Mar 04 15:48:14 Starting compiler/inference
Mar 04 15:48:16 Finished compiler/inference                                       1s 107MB
Mar 04 15:48:17 Starting compiler/backend/reg_alloc
Mar 04 15:48:19 Finished compiler/backend/reg_alloc                               0s  57MB
Mar 04 15:48:20 Starting compiler/backend/gc
Mar 04 15:48:22 Finished compiler/backend/gc                                      1s 147MB
Mar 04 15:48:23 Starting compiler/backend
Mar 04 15:48:28 Finished compiler/backend                                         4s 257MB
Mar 04 15:48:29 Starting compiler/encoders/asm
Mar 04 15:48:30 Finished compiler/encoders/asm                                    0s  86MB
Mar 04 15:48:31 Starting compiler/encoders/x64
Mar 04 15:48:33 Finished compiler/encoders/x64                                    0s  86MB
Mar 04 15:48:34 Starting compiler/encoders/arm7
Mar 04 15:48:35 Finished compiler/encoders/arm7                                   0s  90MB
Mar 04 15:48:36 Starting compiler/encoders/arm8
Mar 04 15:48:38 Finished compiler/encoders/arm8                                   0s  84MB
Mar 04 15:48:39 Starting compiler/encoders/arm8_asl
Mar 04 17:46:46 Finished compiler/encoders/arm8_asl                         1h58m05s  39GB
Mar 04 17:46:47 Starting compiler/encoders/mips
Mar 04 17:46:49 Finished compiler/encoders/mips                                   0s  87MB
Mar 04 17:46:50 Starting compiler/encoders/riscv
Mar 04 17:46:51 Finished compiler/encoders/riscv                                  0s  84MB
Mar 04 17:46:52 Starting compiler/encoders/ag32
Mar 04 17:46:54 Finished compiler/encoders/ag32                                   0s  80MB
Mar 04 17:46:55 Starting compiler/encoders/tests
Mar 04 17:46:57 Finished compiler/encoders/tests                                  1s 111MB
Mar 04 17:46:58 Starting compiler/encoders/monadic_enc
Mar 04 17:47:00 Finished compiler/encoders/monadic_enc                            1s 136MB
Mar 04 17:47:01 Starting compiler/backend/x64
Mar 04 17:47:03 Finished compiler/backend/x64                                     1s 137MB
Mar 04 17:47:04 Starting compiler/backend/arm7
Mar 04 17:47:06 Finished compiler/backend/arm7                                    1s 137MB
Mar 04 17:47:07 Starting compiler/backend/arm8
Mar 04 17:47:09 Finished compiler/backend/arm8                                    1s 137MB
Mar 04 17:47:10 Starting compiler/backend/mips
Mar 04 17:47:12 Finished compiler/backend/mips                                    1s 137MB
Mar 04 17:47:13 Starting compiler/backend/riscv
Mar 04 17:47:15 Finished compiler/backend/riscv                                   1s 137MB
Mar 04 17:47:16 Starting compiler/backend/ag32
Mar 04 17:48:21 Finished compiler/backend/ag32                                 1m04s   2GB
Mar 04 17:48:22 Starting compiler/backend/pattern_matching
Mar 04 17:48:23 Finished compiler/backend/pattern_matching                        0s  52MB
Mar 04 17:48:24 Starting compiler/parsing/ocaml
Mar 04 17:50:06 Finished compiler/parsing/ocaml                                1m40s   1GB
Mar 04 17:50:07 Starting compiler/printing
Mar 04 17:50:09 Finished compiler/printing                                        1s 109MB
Mar 04 17:50:10 Starting compiler/parsing/proofs
Mar 04 17:50:11 Finished compiler/parsing/proofs                                  0s  60MB
Mar 04 17:50:12 Starting compiler/inference/proofs
Mar 04 17:50:14 Finished compiler/inference/proofs                                1s 115MB
Mar 04 17:50:15 Starting compiler/backend/semantics
Mar 04 17:53:18 Finished compiler/backend/semantics                            3m01s   3GB
Mar 04 17:53:19 Starting compiler/backend/reg_alloc/proofs
Mar 04 17:53:21 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Mar 04 17:53:22 Starting compiler/backend/proofs
Mar 04 17:54:08 Finished compiler/backend/proofs                                 45s   2GB
Mar 04 17:54:09 Starting compiler/backend/serialiser
Mar 04 17:54:12 Finished compiler/backend/serialiser                              1s 143MB
Mar 04 17:54:12 Starting compiler/encoders/x64/proofs
Mar 04 18:04:25 Finished compiler/encoders/x64/proofs                         10m11s   4GB
Mar 04 18:04:26 Starting compiler/encoders/arm7/proofs
Mar 04 18:17:30 Finished compiler/encoders/arm7/proofs                        13m02s   8GB
Mar 04 18:17:30 Starting compiler/encoders/arm8/proofs
Mar 04 18:24:08 Finished compiler/encoders/arm8/proofs                         6m36s   3GB
Mar 04 18:24:09 Starting compiler/encoders/arm8_asl/proofs
Mar 04 19:13:19 Finished compiler/encoders/arm8_asl/proofs                    49m08s  18GB
Mar 04 19:13:20 Starting compiler/encoders/mips/proofs
Mar 04 19:23:23 Finished compiler/encoders/mips/proofs                        10m01s   5GB
Mar 04 19:23:24 Starting compiler/encoders/riscv/proofs
Mar 04 19:31:27 Finished compiler/encoders/riscv/proofs                        8m02s   3GB
Mar 04 19:31:28 Starting compiler/encoders/ag32/proofs
Mar 04 19:34:19 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Mar 04 19:34:20 Starting compiler/backend/x64/proofs
Mar 04 19:34:51 Finished compiler/backend/x64/proofs                             30s   2GB
Mar 04 19:34:52 Starting compiler/backend/arm7/proofs
Mar 04 19:35:23 Finished compiler/backend/arm7/proofs                            30s   2GB
Mar 04 19:35:24 Starting compiler/backend/arm8/proofs
Mar 04 19:35:56 Finished compiler/backend/arm8/proofs                            31s   2GB
Mar 04 19:35:57 Starting compiler/backend/arm8_asl
Mar 04 19:36:17 Finished compiler/backend/arm8_asl                               19s   1GB
Mar 04 19:36:18 Starting compiler/backend/mips/proofs
Mar 04 19:36:49 Finished compiler/backend/mips/proofs                            30s   2GB
Mar 04 19:36:50 Starting compiler/backend/riscv/proofs
Mar 04 19:37:24 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 04 19:37:25 Starting compiler/backend/ag32/proofs
Mar 04 19:51:22 Finished compiler/backend/ag32/proofs                         13m56s   5GB
Mar 04 19:51:23 Starting compiler/backend/cv_compute
Mar 04 19:52:34 Finished compiler/backend/cv_compute                           1m09s   2GB
Mar 04 19:52:35 Starting cv_translator
Mar 04 20:13:30 Finished cv_translator                                        20m53s   7GB
Mar 04 20:13:31 Starting candle
Mar 04 20:13:32 Finished candle                                                   0s  11MB
Mar 04 20:13:33 Starting candle/set-theory
Mar 04 20:14:08 Finished candle/set-theory                                       35s   1GB
Mar 04 20:14:09 Starting candle/syntax-lib
Mar 04 20:14:11 Finished candle/syntax-lib                                        0s  91MB
Mar 04 20:14:12 Starting candle/standard
Mar 04 20:14:13 Finished candle/standard                                          0s  12MB
Mar 04 20:14:14 Starting candle/standard/syntax
Mar 04 20:14:26 Finished candle/standard/syntax                                  11s 781MB
Mar 04 20:14:27 Starting candle/standard/semantics
Mar 04 20:16:27 Finished candle/standard/semantics                             1m59s   2GB
Mar 04 20:16:28 Starting candle/standard/monadic
Mar 04 20:16:30 Finished candle/standard/monadic                                  1s 123MB
Mar 04 20:16:31 Starting candle/standard/ml_kernel
Mar 04 20:18:16 Finished candle/standard/ml_kernel                             1m43s   4GB
Mar 04 20:18:16 Starting candle/standard/ml_kernel/lisp
Mar 04 20:18:18 Finished candle/standard/ml_kernel/lisp                           0s  47MB
Mar 04 20:18:19 Starting candle/overloading
Mar 04 20:18:20 Finished candle/overloading                                       0s  11MB
Mar 04 20:18:20 Starting candle/overloading/syntax
Mar 04 20:21:28 Finished candle/overloading/syntax                             3m06s   2GB
Mar 04 20:21:28 Starting candle/overloading/semantics
Mar 04 20:32:41 Finished candle/overloading/semantics                         11m11s   2GB
Mar 04 20:32:42 Starting candle/overloading/monadic
Mar 04 20:34:58 Finished candle/overloading/monadic                            2m15s   2GB
Mar 04 20:34:59 Starting candle/overloading/ml_kernel
Mar 04 20:42:08 Finished candle/overloading/ml_kernel                          7m07s   5GB
Mar 04 20:42:09 Starting candle/overloading/ml_checker
Mar 04 20:44:17 Finished candle/overloading/ml_checker                         2m06s   6GB
Mar 04 20:44:17 Starting candle/prover
Mar 04 20:53:53 Finished candle/prover                                         9m34s   5GB
Mar 04 20:53:53 Starting candle/prover/compute
Mar 04 20:53:56 Finished candle/prover/compute                                    1s 152MB
Mar 04 20:53:57 Starting pancake
Mar 04 20:54:18 Finished pancake                                                 19s 728MB
Mar 04 20:54:18 Starting pancake/semantics
Mar 04 20:56:27 Finished pancake/semantics                                     2m07s   1GB
Mar 04 20:56:27 Starting pancake/parser
Mar 04 20:56:51 Finished pancake/parser                                          22s 446MB
Mar 04 20:56:52 Starting pancake/proofs
Mar 04 21:12:47 Finished pancake/proofs                                       15m53s   7GB
Mar 04 21:12:48 Starting pancake/ta_progs
Mar 04 21:12:49 Finished pancake/ta_progs                                         0s  11MB
Mar 04 21:12:50 Starting compiler/dafny
Mar 04 21:15:47 Finished compiler/dafny                                        2m55s  10GB
Mar 04 21:15:48 Starting compiler/dafny/translation
Mar 04 21:35:03 Finished compiler/dafny/translation                           19m14s  20GB
Mar 04 21:35:04 Starting compiler/dafny/compilation
Mar 04 21:37:36 Finished compiler/dafny/compilation                            2m31s   7GB
Mar 04 21:37:37 Starting compiler/dafny/semantics
Mar 04 21:38:13 Finished compiler/dafny/semantics                                35s   1GB
Mar 04 21:38:14 Starting characteristic/examples
Mar 04 21:39:38 Finished characteristic/examples                               1m23s   4GB
Mar 04 21:39:39 Starting tutorial/solutions
Mar 04 21:42:12 Finished tutorial/solutions                                    2m31s   6GB
Mar 04 21:42:13 Starting translator/monadic/examples
Mar 04 21:45:05 Finished translator/monadic/examples                           2m51s   3GB
Mar 04 21:45:06 Starting examples
Mar 04 21:51:10 Finished examples                                              6m03s   5GB
Mar 04 21:51:11 Starting examples/compilation
Mar 04 21:51:12 Finished examples/compilation                                     0s  11MB
Mar 04 21:51:13 Starting examples/compilation/x64
Mar 04 21:57:40 Finished examples/compilation/x64                              6m26s   3GB
Mar 04 21:57:41 Starting examples/compilation/x64/proofs
Mar 04 22:00:04 Finished examples/compilation/x64/proofs                       2m22s   4GB
Mar 04 22:00:05 Starting examples/compilation/ag32
Mar 04 22:01:53 Finished examples/compilation/ag32                             1m46s   3GB
Mar 04 22:01:54 Starting examples/compilation/ag32/proofs
Mar 04 22:02:55 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Mar 04 22:02:56 Starting examples/lpr_checker
Mar 04 22:03:25 Finished examples/lpr_checker                                    28s   1GB
Mar 04 22:03:26 Starting examples/lpr_checker/array
Mar 04 22:29:45 Finished examples/lpr_checker/array                           26m16s  29GB
Mar 04 22:29:46 Starting examples/lpr_checker/array/compilation
Mar 04 22:37:51 Finished examples/lpr_checker/array/compilation                8m03s  36GB
Mar 04 22:37:51 Starting examples/lpr_checker/array/compilation/proofs
Mar 04 22:39:02 Finished examples/lpr_checker/array/compilation/proofs         1m09s   6GB
Mar 04 22:39:03 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 04 22:40:11 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Mar 04 22:40:12 Starting .
Mar 04 22:40:16 Finished .                                                        2s 301MB
Mar 04 22:40:17 Starting examples/xlrup_checker
Mar 04 22:40:51 Finished examples/xlrup_checker                                  33s   1GB
Mar 04 22:40:52 Starting examples/xlrup_checker/array
Mar 04 22:53:57 Finished examples/xlrup_checker/array                         13m03s  10GB
Mar 04 22:53:57 Starting examples/xlrup_checker/array/compilation
Mar 04 22:54:57 Finished examples/xlrup_checker/array/compilation                58s   4GB
Mar 04 22:54:58 Starting examples/xlrup_checker/array/compilation/proofs
Mar 04 22:55:56 Finished examples/xlrup_checker/array/compilation/proofs         57s   4GB
Mar 04 22:55:57 Starting examples/pseudo_bool
Mar 04 22:57:27 Finished examples/pseudo_bool                                  1m29s   2GB
Mar 04 22:57:28 Starting examples/pseudo_bool/cnf_encoding
Mar 04 22:57:58 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Mar 04 22:57:59 Starting examples/pseudo_bool/graph_encoding
Mar 04 22:58:42 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Mar 04 22:58:43 Starting examples/pseudo_bool/array
Mar 05 00:07:08 Finished examples/pseudo_bool/array                         1h08m23s  39GB
Mar 05 00:07:09 Starting examples/pseudo_bool/array/compilation
Mar 05 00:15:45 Finished examples/pseudo_bool/array/compilation                8m34s  16GB
Mar 05 00:15:46 Starting examples/pseudo_bool/array/compilation/proofs
Mar 05 00:18:20 Finished examples/pseudo_bool/array/compilation/proofs         2m33s   7GB
Mar 05 00:18:21 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 05 00:19:32 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m09s   6GB
Mar 05 00:19:32 Starting examples/opentheory
Mar 05 00:28:03 Finished examples/opentheory                                   8m29s   3GB
Mar 05 00:28:03 Starting examples/opentheory/compilation
Mar 05 00:29:31 Finished examples/opentheory/compilation                       1m26s   6GB
Mar 05 00:29:32 Starting examples/opentheory/compilation/proofs
Mar 05 00:30:33 Finished examples/opentheory/compilation/proofs                1m00s   4GB
Mar 05 00:30:34 Starting examples/opentheory/compilation/ag32
Mar 05 00:32:02 Finished examples/opentheory/compilation/ag32                  1m27s   6GB
Mar 05 00:32:03 Starting examples/opentheory/compilation/ag32/proofs
Mar 05 00:33:43 Finished examples/opentheory/compilation/ag32/proofs           1m38s   8GB
Mar 05 00:33:44 Starting examples/sat_encodings
Mar 05 00:34:45 Finished examples/sat_encodings                                  59s 896MB
Mar 05 00:34:45 Starting examples/sat_encodings/demo
Mar 05 00:34:46 Finished examples/sat_encodings/demo                              0s  11MB
Mar 05 00:34:47 Starting examples/sat_encodings/case_studies
Mar 05 00:36:34 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Mar 05 00:36:35 Starting examples/sat_encodings/translation
Mar 05 00:40:10 Finished examples/sat_encodings/translation                    3m34s   4GB
Mar 05 00:40:11 Starting examples/sat_encodings/translation/compilation
Mar 05 00:41:55 Finished examples/sat_encodings/translation/compilation        1m43s   4GB
Mar 05 00:41:56 Starting examples/deflate
Mar 05 00:42:24 Finished examples/deflate                                        26s 714MB
Mar 05 00:42:25 Starting examples/deflate/translation
Mar 05 00:43:31 Finished examples/deflate/translation                          1m05s   4GB
Mar 05 00:43:32 Starting examples/deflate/translation/compilation
Mar 05 00:44:20 Finished examples/deflate/translation/compilation                47s   3GB
Mar 05 00:44:21 Starting examples/vipr
Mar 05 00:47:59 Finished examples/vipr                                         3m36s   8GB
Mar 05 00:48:00 Starting examples/vipr/compilation
Mar 05 00:48:54 Finished examples/vipr/compilation                               52s   3GB
Mar 05 00:48:55 Starting translator/okasaki-examples
Mar 05 00:52:55 Finished translator/okasaki-examples                           3m59s   4GB
Mar 05 00:52:55 Starting translator/other-examples
Mar 05 00:55:52 Finished translator/other-examples                             2m56s   3GB
Mar 05 00:55:53 Starting translator/other-examples/auxiliary
Mar 05 00:55:54 Finished translator/other-examples/auxiliary                      0s  11MB
Mar 05 00:55:55 Starting compiler/parsing/tests
Mar 05 00:56:30 Finished compiler/parsing/tests                                  34s   1GB
Mar 05 00:56:31 Starting compiler/inference/tests
Mar 05 00:57:07 Finished compiler/inference/tests                                34s   2GB
Mar 05 00:57:08 Starting compiler/printing/test
Mar 05 00:58:19 Finished compiler/printing/test                                1m10s   6GB
Mar 05 00:58:20 Starting icing/flover
Mar 05 01:31:54 Finished icing/flover                                         33m30s   2GB
Mar 05 01:31:55 Starting icing/flover/Infra
Mar 05 01:31:56 Finished icing/flover/Infra                                       0s  11MB
Mar 05 01:31:56 Starting icing/flover/semantics
Mar 05 01:31:57 Finished icing/flover/semantics                                   0s  12MB
Mar 05 01:31:58 Starting icing/
Mar 05 01:59:06 Finished icing/                                               27m06s   5GB
Mar 05 01:59:07 Starting icing/examples
Mar 05 02:00:38 Finished icing/examples                                        1m30s   7GB
Mar 05 02:00:39 Starting compiler/repl
Mar 05 02:08:43 Finished compiler/repl                                         8m02s   7GB
Mar 05 02:08:44 Starting unverified/sexpr-bootstrap/x64/64
Mar 05 02:12:45 Finished unverified/sexpr-bootstrap/x64/64                     4m00s  17GB
Mar 05 02:12:46 Starting unverified/sexpr-bootstrap/x64/32
Mar 05 02:16:08 Finished unverified/sexpr-bootstrap/x64/32                     3m21s  13GB
Mar 05 02:16:09 Starting compiler/benchmarks
Mar 05 02:16:55 Finished compiler/benchmarks                                     44s 711MB
Mar 05 02:16:56 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 05 02:16:59 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 249MB
Mar 05 02:17:00 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 05 02:17:03 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 266MB
Mar 05 02:17:04 Starting compiler/bootstrap/compilation/x64/64
Mar 05 02:41:00 Finished compiler/bootstrap/compilation/x64/64                23m55s  82GB
Mar 05 02:41:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 05 03:05:01 Finished compiler/bootstrap/compilation/x64/64/proofs         23m59s  54GB
Mar 05 03:05:02 Starting compiler/bootstrap/compilation/x64/32
Mar 05 03:29:24 Finished compiler/bootstrap/compilation/x64/32                24m21s  62GB
Mar 05 03:29:25 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 05 03:33:27 Finished compiler/bootstrap/compilation/x64/32/proofs          4m01s  22GB
Mar 05 03:33:28 Starting compiler/bootstrap/compilation/arm8/64
Mar 05 04:10:08 Finished compiler/bootstrap/compilation/arm8/64               36m38s  75GB
Mar 05 04:10:09 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 05 04:15:48 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m38s  28GB
Mar 05 04:15:49 Starting compiler/bootstrap/compilation/ag32/32
Mar 05 04:41:04 Finished compiler/bootstrap/compilation/ag32/32               25m14s  48GB
Mar 05 04:41:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 05 04:46:14 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m08s  29GB
Mar 05 04:46:15 SUCCESS