Job 2781

CakeML:0b9973c32c95da84ab748acbd4589a8caf74bc28
  Fix translator issues [Mar 06 04:34:30]
#1138 (halogentlepersuasion:pan_static)
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:lammmington

Mar 06 07:35:13 Claimed job
Mar 06 07:35:20 Building HOL
Mar 06 07:46:12 Starting developers
Mar 06 07:46:16 Finished developers                                               3s 208MB
Mar 06 07:46:17 Starting developers/bin
Mar 06 07:46:23 Finished developers/bin                                           5s 746MB
Mar 06 07:46:24 Starting misc
Mar 06 07:47:22 Finished misc                                                    57s   1GB
Mar 06 07:47:23 Starting compiler/proofs
Mar 06 09:28:40 Finished compiler/proofs                                    1h41m16s  26GB
Mar 06 09:28:41 Starting compiler/bootstrap/translation
Mar 06 15:16:30 Finished compiler/bootstrap/translation                     5h47m47s  88GB
Mar 06 15:16:30 Starting semantics/ffi
Mar 06 15:16:41 Finished semantics/ffi                                            9s 595MB
Mar 06 15:16:41 Starting semantics
Mar 06 15:16:43 Finished semantics                                                0s  52MB
Mar 06 15:16:44 Starting semantics/proofs
Mar 06 15:17:07 Finished semantics/proofs                                        21s 886MB
Mar 06 15:17:07 Starting semantics/alt_semantics
Mar 06 15:17:28 Finished semantics/alt_semantics                                 20s 890MB
Mar 06 15:17:29 Starting semantics/alt_semantics/proofs
Mar 06 15:27:49 Finished semantics/alt_semantics/proofs                       10m18s   2GB
Mar 06 15:27:50 Starting basis/pure
Mar 06 15:27:51 Finished basis/pure                                               0s  94MB
Mar 06 15:27:52 Starting translator
Mar 06 15:29:24 Finished translator                                            1m30s   3GB
Mar 06 15:29:25 Starting compiler/parsing
Mar 06 15:29:26 Finished compiler/parsing                                         0s  55MB
Mar 06 15:29:27 Starting characteristic
Mar 06 15:29:29 Finished characteristic                                           1s 121MB
Mar 06 15:29:30 Starting translator/monadic
Mar 06 15:29:32 Finished translator/monadic                                       1s 123MB
Mar 06 15:29:33 Starting translator/monadic/monad_base
Mar 06 15:29:34 Finished translator/monadic/monad_base                            0s  51MB
Mar 06 15:29:35 Starting basis
Mar 06 15:32:00 Finished basis                                                 2m23s   4GB
Mar 06 15:32:01 Starting compiler
Mar 06 15:32:04 Finished compiler                                                 1s 197MB
Mar 06 15:32:04 Starting compiler/inference
Mar 06 15:32:06 Finished compiler/inference                                       1s 107MB
Mar 06 15:32:07 Starting compiler/backend/reg_alloc
Mar 06 15:32:09 Finished compiler/backend/reg_alloc                               0s  57MB
Mar 06 15:32:10 Starting compiler/backend/gc
Mar 06 15:32:12 Finished compiler/backend/gc                                      1s 145MB
Mar 06 15:32:13 Starting compiler/backend
Mar 06 15:32:18 Finished compiler/backend                                         4s 259MB
Mar 06 15:32:19 Starting compiler/encoders/asm
Mar 06 15:32:20 Finished compiler/encoders/asm                                    0s  86MB
Mar 06 15:32:21 Starting compiler/encoders/x64
Mar 06 15:32:23 Finished compiler/encoders/x64                                    0s  87MB
Mar 06 15:32:24 Starting compiler/encoders/arm7
Mar 06 15:32:25 Finished compiler/encoders/arm7                                   0s  92MB
Mar 06 15:32:26 Starting compiler/encoders/arm8
Mar 06 15:32:28 Finished compiler/encoders/arm8                                   0s  90MB
Mar 06 15:32:29 Starting compiler/encoders/arm8_asl
Mar 06 17:33:38 Finished compiler/encoders/arm8_asl                         2h01m08s  28GB
Mar 06 17:33:39 Starting compiler/encoders/mips
Mar 06 17:33:41 Finished compiler/encoders/mips                                   0s  88MB
Mar 06 17:33:42 Starting compiler/encoders/riscv
Mar 06 17:33:43 Finished compiler/encoders/riscv                                  0s  86MB
Mar 06 17:33:44 Starting compiler/encoders/ag32
Mar 06 17:33:46 Finished compiler/encoders/ag32                                   0s  84MB
Mar 06 17:33:47 Starting compiler/encoders/tests
Mar 06 17:33:49 Finished compiler/encoders/tests                                  1s 114MB
Mar 06 17:33:50 Starting compiler/encoders/monadic_enc
Mar 06 17:33:52 Finished compiler/encoders/monadic_enc                            1s 135MB
Mar 06 17:33:53 Starting compiler/backend/x64
Mar 06 17:33:55 Finished compiler/backend/x64                                     1s 136MB
Mar 06 17:33:56 Starting compiler/backend/arm7
Mar 06 17:33:58 Finished compiler/backend/arm7                                    1s 138MB
Mar 06 17:33:59 Starting compiler/backend/arm8
Mar 06 17:34:01 Finished compiler/backend/arm8                                    1s 137MB
Mar 06 17:34:02 Starting compiler/backend/mips
Mar 06 17:34:04 Finished compiler/backend/mips                                    1s 137MB
Mar 06 17:34:05 Starting compiler/backend/riscv
Mar 06 17:34:07 Finished compiler/backend/riscv                                   1s 137MB
Mar 06 17:34:08 Starting compiler/backend/ag32
Mar 06 17:35:15 Finished compiler/backend/ag32                                 1m06s   1GB
Mar 06 17:35:16 Starting compiler/backend/pattern_matching
Mar 06 17:35:18 Finished compiler/backend/pattern_matching                        0s  54MB
Mar 06 17:35:19 Starting compiler/parsing/ocaml
Mar 06 17:37:00 Finished compiler/parsing/ocaml                                1m40s   1GB
Mar 06 17:37:01 Starting compiler/printing
Mar 06 17:37:03 Finished compiler/printing                                        1s 122MB
Mar 06 17:37:04 Starting compiler/parsing/proofs
Mar 06 17:37:05 Finished compiler/parsing/proofs                                  0s  65MB
Mar 06 17:37:06 Starting compiler/inference/proofs
Mar 06 17:37:08 Finished compiler/inference/proofs                                1s 121MB
Mar 06 17:37:09 Starting compiler/backend/semantics
Mar 06 17:40:18 Finished compiler/backend/semantics                            3m07s   2GB
Mar 06 17:40:18 Starting compiler/backend/reg_alloc/proofs
Mar 06 17:40:20 Finished compiler/backend/reg_alloc/proofs                        1s 118MB
Mar 06 17:40:21 Starting compiler/backend/proofs
Mar 06 17:41:14 Finished compiler/backend/proofs                                 51s   4GB
Mar 06 17:41:15 Starting compiler/backend/serialiser
Mar 06 17:41:17 Finished compiler/backend/serialiser                              1s 140MB
Mar 06 17:41:18 Starting compiler/encoders/x64/proofs
Mar 06 17:51:30 Finished compiler/encoders/x64/proofs                         10m11s   5GB
Mar 06 17:51:31 Starting compiler/encoders/arm7/proofs
Mar 06 18:04:28 Finished compiler/encoders/arm7/proofs                        12m56s   6GB
Mar 06 18:04:29 Starting compiler/encoders/arm8/proofs
Mar 06 18:11:40 Finished compiler/encoders/arm8/proofs                         7m10s   4GB
Mar 06 18:11:41 Starting compiler/encoders/arm8_asl/proofs
Mar 06 19:00:57 Finished compiler/encoders/arm8_asl/proofs                    49m14s  20GB
Mar 06 19:00:58 Starting compiler/encoders/mips/proofs
Mar 06 19:10:55 Finished compiler/encoders/mips/proofs                         9m56s   4GB
Mar 06 19:10:56 Starting compiler/encoders/riscv/proofs
Mar 06 19:19:04 Finished compiler/encoders/riscv/proofs                        8m07s   4GB
Mar 06 19:19:05 Starting compiler/encoders/ag32/proofs
Mar 06 19:21:56 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Mar 06 19:21:56 Starting compiler/backend/x64/proofs
Mar 06 19:22:28 Finished compiler/backend/x64/proofs                             30s   2GB
Mar 06 19:22:29 Starting compiler/backend/arm7/proofs
Mar 06 19:23:03 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 06 19:23:04 Starting compiler/backend/arm8/proofs
Mar 06 19:23:37 Finished compiler/backend/arm8/proofs                            31s   2GB
Mar 06 19:23:38 Starting compiler/backend/arm8_asl
Mar 06 19:23:59 Finished compiler/backend/arm8_asl                               20s   1GB
Mar 06 19:24:00 Starting compiler/backend/mips/proofs
Mar 06 19:24:32 Finished compiler/backend/mips/proofs                            31s   2GB
Mar 06 19:24:33 Starting compiler/backend/riscv/proofs
Mar 06 19:25:07 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 06 19:25:08 Starting compiler/backend/ag32/proofs
Mar 06 19:38:50 Finished compiler/backend/ag32/proofs                         13m41s   5GB
Mar 06 19:38:52 Starting compiler/backend/cv_compute
Mar 06 19:40:02 Finished compiler/backend/cv_compute                           1m09s   2GB
Mar 06 19:40:03 Starting cv_translator
Mar 06 20:00:51 Finished cv_translator                                        20m46s   7GB
Mar 06 20:00:52 Starting candle
Mar 06 20:00:53 Finished candle                                                   0s  11MB
Mar 06 20:00:54 Starting candle/set-theory
Mar 06 20:01:30 Finished candle/set-theory                                       35s   1GB
Mar 06 20:01:31 Starting candle/syntax-lib
Mar 06 20:01:32 Finished candle/syntax-lib                                        0s  95MB
Mar 06 20:01:33 Starting candle/standard
Mar 06 20:01:34 Finished candle/standard                                          0s  10MB
Mar 06 20:01:35 Starting candle/standard/syntax
Mar 06 20:01:47 Finished candle/standard/syntax                                  11s 797MB
Mar 06 20:01:48 Starting candle/standard/semantics
Mar 06 20:03:54 Finished candle/standard/semantics                             2m05s   2GB
Mar 06 20:03:55 Starting candle/standard/monadic
Mar 06 20:03:57 Finished candle/standard/monadic                                  1s 123MB
Mar 06 20:03:58 Starting candle/standard/ml_kernel
Mar 06 20:05:41 Finished candle/standard/ml_kernel                             1m41s   4GB
Mar 06 20:05:41 Starting candle/standard/ml_kernel/lisp
Mar 06 20:05:43 Finished candle/standard/ml_kernel/lisp                           0s  47MB
Mar 06 20:05:44 Starting candle/overloading
Mar 06 20:05:45 Finished candle/overloading                                       0s  12MB
Mar 06 20:05:45 Starting candle/overloading/syntax
Mar 06 20:08:54 Finished candle/overloading/syntax                             3m07s   2GB
Mar 06 20:08:55 Starting candle/overloading/semantics
Mar 06 20:19:53 Finished candle/overloading/semantics                         10m56s   3GB
Mar 06 20:19:54 Starting candle/overloading/monadic
Mar 06 20:22:10 Finished candle/overloading/monadic                            2m15s   2GB
Mar 06 20:22:11 Starting candle/overloading/ml_kernel
Mar 06 20:29:22 Finished candle/overloading/ml_kernel                          7m09s   5GB
Mar 06 20:29:23 Starting candle/overloading/ml_checker
Mar 06 20:31:34 Finished candle/overloading/ml_checker                         2m10s   6GB
Mar 06 20:31:34 Starting candle/prover
Mar 06 20:41:13 Finished candle/prover                                         9m37s   5GB
Mar 06 20:41:13 Starting candle/prover/compute
Mar 06 20:41:16 Finished candle/prover/compute                                    1s 152MB
Mar 06 20:41:17 Starting pancake
Mar 06 20:41:38 Finished pancake                                                 20s 726MB
Mar 06 20:41:39 Starting pancake/semantics
Mar 06 20:43:46 Finished pancake/semantics                                     2m06s   2GB
Mar 06 20:43:47 Starting pancake/parser
Mar 06 20:44:11 Finished pancake/parser                                          22s 443MB
Mar 06 20:44:12 Starting pancake/static_checker
Mar 06 20:44:50 Finished pancake/static_checker                                  36s   1GB
Mar 06 20:44:51 Starting pancake/proofs
Mar 06 21:00:54 Finished pancake/proofs                                       16m02s   7GB
Mar 06 21:00:55 Starting pancake/ta_progs
Mar 06 21:00:56 Finished pancake/ta_progs                                         0s  11MB
Mar 06 21:00:57 Starting compiler/dafny
Mar 06 21:03:38 Finished compiler/dafny                                        2m40s  12GB
Mar 06 21:03:39 Starting compiler/dafny/translation
Mar 06 21:21:54 Finished compiler/dafny/translation                           18m13s  21GB
Mar 06 21:21:55 Starting compiler/dafny/compilation
Mar 06 21:24:43 Finished compiler/dafny/compilation                            2m47s  10GB
Mar 06 21:24:44 Starting compiler/dafny/semantics
Mar 06 21:25:20 Finished compiler/dafny/semantics                                35s   1GB
Mar 06 21:25:21 Starting characteristic/examples
Mar 06 21:26:44 Finished characteristic/examples                               1m22s   4GB
Mar 06 21:26:45 Starting tutorial/solutions
Mar 06 21:29:08 Finished tutorial/solutions                                    2m22s   3GB
Mar 06 21:29:09 Starting translator/monadic/examples
Mar 06 21:32:02 Finished translator/monadic/examples                           2m51s   4GB
Mar 06 21:32:03 Starting examples
Mar 06 21:38:06 Finished examples                                              6m01s   4GB
Mar 06 21:38:06 Starting examples/compilation
Mar 06 21:38:07 Finished examples/compilation                                     0s  11MB
Mar 06 21:38:08 Starting examples/compilation/x64
Mar 06 21:45:02 Finished examples/compilation/x64                              6m53s   4GB
Mar 06 21:45:03 Starting examples/compilation/x64/proofs
Mar 06 21:47:27 Finished examples/compilation/x64/proofs                       2m21s   4GB
Mar 06 21:47:27 Starting examples/compilation/ag32
Mar 06 21:49:21 Finished examples/compilation/ag32                             1m52s   3GB
Mar 06 21:49:22 Starting examples/compilation/ag32/proofs
Mar 06 21:50:21 Finished examples/compilation/ag32/proofs                        57s   5GB
Mar 06 21:50:21 Starting examples/lpr_checker
Mar 06 21:50:51 Finished examples/lpr_checker                                    29s   1GB
Mar 06 21:50:52 Starting examples/lpr_checker/array
Mar 06 22:16:56 Finished examples/lpr_checker/array                           26m02s  24GB
Mar 06 22:16:56 Starting examples/lpr_checker/array/compilation
Mar 06 23:25:57 Finished examples/lpr_checker/array/compilation             1h08m59s 249GB
Mar 06 23:25:58 Starting examples/lpr_checker/array/compilation/proofs
Mar 06 23:27:08 Finished examples/lpr_checker/array/compilation/proofs         1m09s   6GB
Mar 06 23:27:09 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 06 23:28:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Mar 06 23:28:19 Starting .
Mar 06 23:28:22 Finished .                                                        2s 295MB
Mar 06 23:28:23 Starting examples/xlrup_checker
Mar 06 23:28:58 Finished examples/xlrup_checker                                  34s   1GB
Mar 06 23:28:59 Starting examples/xlrup_checker/array
Mar 06 23:41:51 Finished examples/xlrup_checker/array                         12m50s  11GB
Mar 06 23:41:52 Starting examples/xlrup_checker/array/compilation
Mar 06 23:42:54 Finished examples/xlrup_checker/array/compilation              1m01s   5GB
Mar 06 23:42:55 Starting examples/xlrup_checker/array/compilation/proofs
Mar 06 23:43:57 Finished examples/xlrup_checker/array/compilation/proofs       1m00s   5GB
Mar 06 23:43:58 Starting examples/pseudo_bool
Mar 06 23:45:27 Finished examples/pseudo_bool                                  1m28s   2GB
Mar 06 23:45:28 Starting examples/pseudo_bool/cnf_encoding
Mar 06 23:45:58 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Mar 06 23:45:59 Starting examples/pseudo_bool/graph_encoding
Mar 06 23:46:43 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Mar 06 23:46:44 Starting examples/pseudo_bool/array
Mar 07 00:54:07 Finished examples/pseudo_bool/array                         1h07m22s  33GB
Mar 07 00:54:08 Starting examples/pseudo_bool/array/compilation
Mar 07 01:04:03 Finished examples/pseudo_bool/array/compilation                9m54s  18GB
Mar 07 01:04:04 Starting examples/pseudo_bool/array/compilation/proofs
Mar 07 01:06:35 Finished examples/pseudo_bool/array/compilation/proofs         2m30s   6GB
Mar 07 01:06:36 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 07 01:07:46 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m08s   7GB
Mar 07 01:07:47 Starting examples/opentheory
Mar 07 01:16:18 Finished examples/opentheory                                   8m30s   6GB
Mar 07 01:16:19 Starting examples/opentheory/compilation
Mar 07 01:17:53 Finished examples/opentheory/compilation                       1m33s   6GB
Mar 07 01:17:54 Starting examples/opentheory/compilation/proofs
Mar 07 01:18:52 Finished examples/opentheory/compilation/proofs                  57s   5GB
Mar 07 01:18:53 Starting examples/opentheory/compilation/ag32
Mar 07 01:20:31 Finished examples/opentheory/compilation/ag32                  1m37s   7GB
Mar 07 01:20:32 Starting examples/opentheory/compilation/ag32/proofs
Mar 07 01:22:10 Finished examples/opentheory/compilation/ag32/proofs           1m37s   8GB
Mar 07 01:22:11 Starting examples/sat_encodings
Mar 07 01:23:12 Finished examples/sat_encodings                                1m00s 848MB
Mar 07 01:23:13 Starting examples/sat_encodings/demo
Mar 07 01:23:14 Finished examples/sat_encodings/demo                              0s  11MB
Mar 07 01:23:15 Starting examples/sat_encodings/case_studies
Mar 07 01:24:59 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Mar 07 01:25:00 Starting examples/sat_encodings/translation
Mar 07 01:28:32 Finished examples/sat_encodings/translation                    3m31s   3GB
Mar 07 01:28:33 Starting examples/sat_encodings/translation/compilation
Mar 07 01:30:30 Finished examples/sat_encodings/translation/compilation        1m55s   4GB
Mar 07 01:30:31 Starting examples/deflate
Mar 07 01:30:59 Finished examples/deflate                                        27s 717MB
Mar 07 01:31:00 Starting examples/deflate/translation
Mar 07 01:32:05 Finished examples/deflate/translation                          1m04s   4GB
Mar 07 01:32:06 Starting examples/deflate/translation/compilation
Mar 07 01:32:59 Finished examples/deflate/translation/compilation                51s   3GB
Mar 07 01:32:59 Starting examples/vipr
Mar 07 01:36:31 Finished examples/vipr                                         3m30s   7GB
Mar 07 01:36:31 Starting examples/vipr/compilation
Mar 07 01:37:28 Finished examples/vipr/compilation                               55s   4GB
Mar 07 01:37:29 Starting translator/okasaki-examples
Mar 07 01:41:29 Finished translator/okasaki-examples                           3m59s   3GB
Mar 07 01:41:30 Starting translator/other-examples
Mar 07 01:44:30 Finished translator/other-examples                             2m59s   3GB
Mar 07 01:44:31 Starting translator/other-examples/auxiliary
Mar 07 01:44:32 Finished translator/other-examples/auxiliary                      0s  11MB
Mar 07 01:44:33 Starting compiler/parsing/tests
Mar 07 01:45:08 Finished compiler/parsing/tests                                  34s   1GB
Mar 07 01:45:09 Starting compiler/inference/tests
Mar 07 01:45:45 Finished compiler/inference/tests                                35s   2GB
Mar 07 01:45:46 Starting compiler/printing/test
Mar 07 01:46:59 Finished compiler/printing/test                                1m11s   6GB
Mar 07 01:47:00 Starting icing/flover
Mar 07 02:20:56 Finished icing/flover                                         33m54s   1GB
Mar 07 02:20:57 Starting icing/flover/Infra
Mar 07 02:20:58 Finished icing/flover/Infra                                       0s  11MB
Mar 07 02:20:59 Starting icing/flover/semantics
Mar 07 02:21:00 Finished icing/flover/semantics                                   0s  12MB
Mar 07 02:21:00 Starting icing/
Mar 07 02:48:03 Finished icing/                                               27m01s   7GB
Mar 07 02:48:04 Starting icing/examples
Mar 07 02:49:37 Finished icing/examples                                        1m32s   8GB
Mar 07 02:49:38 Starting compiler/repl
Mar 07 02:57:34 Finished compiler/repl                                         7m54s   7GB
Mar 07 02:57:35 Starting unverified/sexpr-bootstrap/x64/64
Mar 07 03:01:27 Finished unverified/sexpr-bootstrap/x64/64                     3m51s  16GB
Mar 07 03:01:29 Starting unverified/sexpr-bootstrap/x64/32
Mar 07 03:05:27 Finished unverified/sexpr-bootstrap/x64/32                     3m57s  12GB
Mar 07 03:05:28 Starting compiler/benchmarks
Mar 07 03:06:14 Finished compiler/benchmarks                                     44s 711MB
Mar 07 03:06:15 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 07 03:06:18 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 249MB
Mar 07 03:06:19 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 07 03:06:23 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 271MB
Mar 07 03:06:24 Starting compiler/bootstrap/compilation/x64/64
Mar 07 03:34:28 Finished compiler/bootstrap/compilation/x64/64                28m03s  94GB
Mar 07 03:34:29 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 07 03:58:06 Finished compiler/bootstrap/compilation/x64/64/proofs         23m35s  44GB
Mar 07 03:58:07 Starting compiler/bootstrap/compilation/x64/32
Mar 07 04:26:54 Finished compiler/bootstrap/compilation/x64/32                28m46s  75GB
Mar 07 04:26:55 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 07 04:31:08 Finished compiler/bootstrap/compilation/x64/32/proofs          4m11s  23GB
Mar 07 04:31:08 Starting compiler/bootstrap/compilation/arm8/64
Mar 07 05:12:29 Finished compiler/bootstrap/compilation/arm8/64               41m19s 116GB
Mar 07 05:12:30 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 07 05:17:14 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m43s  30GB
Mar 07 05:17:15 Starting compiler/bootstrap/compilation/ag32/32
Mar 07 05:47:44 Finished compiler/bootstrap/compilation/ag32/32               30m27s  82GB
Mar 07 05:47:45 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 07 05:52:26 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m40s  29GB
Mar 07 05:52:27 SUCCESS