Job 2772

CakeML:e0e8a40f04c4ebbce02bc7e9b654ca2c547f79ce
  Merge pull request #1129 from CakeML/remove_Misc_bool_case_eq [Feb 07 15:04:17]
HOL:8c4bb7e9ff0ffbaaa9058df6bf0322d96c3132dc
  Tweak drule_all* so negated conclusions are not seen as implications [Jan 30 22:45:48]
Machine:lammmington
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-arm8-64.tar.gz
cake-x64-32.tar.gz

Feb 07 15:10:13 Claimed job
Feb 07 15:10:17 Reusing HOL
Feb 07 15:10:28 Starting developers
Feb 07 15:10:32 Finished developers                                               3s 218MB
Feb 07 15:10:32 Starting developers/bin
Feb 07 15:10:39 Finished developers/bin                                           5s 746MB
Feb 07 15:10:40 Starting misc
Feb 07 15:11:23 Finished misc                                                    41s   1GB
Feb 07 15:11:23 Starting compiler/proofs
Feb 07 16:50:22 Finished compiler/proofs                                    1h38m57s  35GB
Feb 07 16:50:23 Starting compiler/bootstrap/translation
Feb 07 22:38:52 Finished compiler/bootstrap/translation                     5h48m28s  96GB
Feb 07 22:38:53 Starting semantics/ffi
Feb 07 22:39:03 Finished semantics/ffi                                            9s 587MB
Feb 07 22:39:04 Starting semantics
Feb 07 22:39:05 Finished semantics                                                0s  52MB
Feb 07 22:39:06 Starting semantics/proofs
Feb 07 22:39:29 Finished semantics/proofs                                        22s 711MB
Feb 07 22:39:30 Starting semantics/alt_semantics
Feb 07 22:39:51 Finished semantics/alt_semantics                                 19s 692MB
Feb 07 22:39:52 Starting semantics/alt_semantics/proofs
Feb 07 22:50:15 Finished semantics/alt_semantics/proofs                       10m22s   2GB
Feb 07 22:50:16 Starting basis/pure
Feb 07 22:50:17 Finished basis/pure                                               0s  63MB
Feb 07 22:50:18 Starting translator
Feb 07 22:51:55 Finished translator                                            1m35s   2GB
Feb 07 22:51:56 Starting compiler/parsing
Feb 07 22:51:57 Finished compiler/parsing                                         0s  57MB
Feb 07 22:51:58 Starting characteristic
Feb 07 22:52:00 Finished characteristic                                           0s  86MB
Feb 07 22:52:01 Starting translator/monadic
Feb 07 22:52:02 Finished translator/monadic                                       0s  86MB
Feb 07 22:52:03 Starting translator/monadic/monad_base
Feb 07 22:52:05 Finished translator/monadic/monad_base                            0s  55MB
Feb 07 22:52:05 Starting basis
Feb 07 22:54:27 Finished basis                                                 2m20s   3GB
Feb 07 22:54:28 Starting compiler
Feb 07 22:54:30 Finished compiler                                                 1s 189MB
Feb 07 22:54:31 Starting compiler/inference
Feb 07 22:54:33 Finished compiler/inference                                       0s  83MB
Feb 07 22:54:34 Starting compiler/backend/reg_alloc
Feb 07 22:54:35 Finished compiler/backend/reg_alloc                               0s  52MB
Feb 07 22:54:36 Starting compiler/backend/gc
Feb 07 22:54:38 Finished compiler/backend/gc                                      1s 131MB
Feb 07 22:54:39 Starting compiler/backend
Feb 07 22:54:44 Finished compiler/backend                                         4s 245MB
Feb 07 22:54:45 Starting compiler/encoders/asm
Feb 07 22:54:47 Finished compiler/encoders/asm                                    0s  83MB
Feb 07 22:54:48 Starting compiler/encoders/x64
Feb 07 22:54:49 Finished compiler/encoders/x64                                    0s  88MB
Feb 07 22:54:50 Starting compiler/encoders/arm7
Feb 07 22:54:52 Finished compiler/encoders/arm7                                   0s  90MB
Feb 07 22:54:53 Starting compiler/encoders/arm8
Feb 07 22:54:55 Finished compiler/encoders/arm8                                   0s  84MB
Feb 07 22:54:56 Starting compiler/encoders/arm8_asl
Feb 07 22:55:52 Finished compiler/encoders/arm8_asl                              55s  18GB
Feb 07 22:55:53 Starting compiler/encoders/mips
Feb 07 22:55:55 Finished compiler/encoders/mips                                   0s  86MB
Feb 07 22:55:56 Starting compiler/encoders/riscv
Feb 07 22:55:58 Finished compiler/encoders/riscv                                  0s  83MB
Feb 07 22:55:58 Starting compiler/encoders/ag32
Feb 07 22:56:00 Finished compiler/encoders/ag32                                   0s  88MB
Feb 07 22:56:01 Starting compiler/encoders/tests
Feb 07 22:56:03 Finished compiler/encoders/tests                                  0s 111MB
Feb 07 22:56:04 Starting compiler/encoders/monadic_enc
Feb 07 22:56:06 Finished compiler/encoders/monadic_enc                            1s 128MB
Feb 07 22:56:07 Starting compiler/backend/x64
Feb 07 22:56:09 Finished compiler/backend/x64                                     1s 133MB
Feb 07 22:56:10 Starting compiler/backend/arm7
Feb 07 22:56:12 Finished compiler/backend/arm7                                    1s 127MB
Feb 07 22:56:13 Starting compiler/backend/arm8
Feb 07 22:56:15 Finished compiler/backend/arm8                                    1s 127MB
Feb 07 22:56:16 Starting compiler/backend/mips
Feb 07 22:56:18 Finished compiler/backend/mips                                    1s 128MB
Feb 07 22:56:19 Starting compiler/backend/riscv
Feb 07 22:56:21 Finished compiler/backend/riscv                                   1s 127MB
Feb 07 22:56:22 Starting compiler/backend/ag32
Feb 07 22:57:28 Finished compiler/backend/ag32                                 1m05s   2GB
Feb 07 22:57:29 Starting compiler/backend/pattern_matching
Feb 07 22:57:30 Finished compiler/backend/pattern_matching                        0s  51MB
Feb 07 22:57:31 Starting compiler/parsing/ocaml
Feb 07 22:59:14 Finished compiler/parsing/ocaml                                1m42s   1GB
Feb 07 22:59:15 Starting compiler/printing
Feb 07 22:59:17 Finished compiler/printing                                        0s  87MB
Feb 07 22:59:18 Starting compiler/parsing/proofs
Feb 07 22:59:19 Finished compiler/parsing/proofs                                  0s  63MB
Feb 07 22:59:20 Starting compiler/inference/proofs
Feb 07 22:59:22 Finished compiler/inference/proofs                                0s  83MB
Feb 07 22:59:23 Starting compiler/backend/semantics
Feb 07 23:02:28 Finished compiler/backend/semantics                            3m04s   2GB
Feb 07 23:02:29 Starting compiler/backend/reg_alloc/proofs
Feb 07 23:02:31 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Feb 07 23:02:32 Starting compiler/backend/proofs
Feb 07 23:03:23 Finished compiler/backend/proofs                                 49s   3GB
Feb 07 23:03:23 Starting compiler/backend/serialiser
Feb 07 23:03:26 Finished compiler/backend/serialiser                              1s 130MB
Feb 07 23:03:26 Starting compiler/encoders/x64/proofs
Feb 07 23:13:40 Finished compiler/encoders/x64/proofs                         10m12s   4GB
Feb 07 23:13:41 Starting compiler/encoders/arm7/proofs
Feb 07 23:27:00 Finished compiler/encoders/arm7/proofs                        13m17s  11GB
Feb 07 23:27:01 Starting compiler/encoders/arm8/proofs
Feb 07 23:34:13 Finished compiler/encoders/arm8/proofs                         7m11s   4GB
Feb 07 23:34:14 Starting compiler/encoders/arm8_asl/proofs
Feb 07 23:49:51 Finished compiler/encoders/arm8_asl/proofs                    15m35s   3GB
Feb 07 23:49:51 Starting compiler/encoders/mips/proofs
Feb 07 23:59:56 Finished compiler/encoders/mips/proofs                        10m04s   4GB
Feb 07 23:59:57 Starting compiler/encoders/riscv/proofs
Feb 08 00:08:01 Finished compiler/encoders/riscv/proofs                        8m02s   4GB
Feb 08 00:08:02 Starting compiler/encoders/ag32/proofs
Feb 08 00:10:54 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Feb 08 00:10:55 Starting compiler/backend/x64/proofs
Feb 08 00:11:26 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 08 00:11:27 Starting compiler/backend/arm7/proofs
Feb 08 00:11:57 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 08 00:11:58 Starting compiler/backend/arm8/proofs
Feb 08 00:12:28 Finished compiler/backend/arm8/proofs                            29s   2GB
Feb 08 00:12:29 Starting compiler/backend/arm8_asl
Feb 08 00:12:51 Finished compiler/backend/arm8_asl                               20s   2GB
Feb 08 00:12:52 Starting compiler/backend/mips/proofs
Feb 08 00:13:22 Finished compiler/backend/mips/proofs                            29s   1GB
Feb 08 00:13:23 Starting compiler/backend/riscv/proofs
Feb 08 00:13:57 Finished compiler/backend/riscv/proofs                           32s   2GB
Feb 08 00:13:58 Starting compiler/backend/ag32/proofs
Feb 08 00:27:42 Finished compiler/backend/ag32/proofs                         13m43s   5GB
Feb 08 00:27:43 Starting compiler/backend/cv_compute
Feb 08 00:28:53 Finished compiler/backend/cv_compute                           1m08s   2GB
Feb 08 00:28:54 Starting cv_translator
Feb 08 00:49:54 Finished cv_translator                                        20m58s   8GB
Feb 08 00:49:55 Starting candle
Feb 08 00:49:56 Finished candle                                                   0s  11MB
Feb 08 00:49:56 Starting candle/set-theory
Feb 08 00:50:31 Finished candle/set-theory                                       33s   1GB
Feb 08 00:50:32 Starting candle/syntax-lib
Feb 08 00:50:33 Finished candle/syntax-lib                                        0s  61MB
Feb 08 00:50:34 Starting candle/standard
Feb 08 00:50:35 Finished candle/standard                                          0s  12MB
Feb 08 00:50:36 Starting candle/standard/syntax
Feb 08 00:50:48 Finished candle/standard/syntax                                  11s 795MB
Feb 08 00:50:49 Starting candle/standard/semantics
Feb 08 00:52:52 Finished candle/standard/semantics                             2m01s   2GB
Feb 08 00:52:53 Starting candle/standard/monadic
Feb 08 00:52:54 Finished candle/standard/monadic                                  0s  96MB
Feb 08 00:52:55 Starting candle/standard/ml_kernel
Feb 08 00:54:39 Finished candle/standard/ml_kernel                             1m42s   4GB
Feb 08 00:54:40 Starting candle/standard/ml_kernel/lisp
Feb 08 00:54:41 Finished candle/standard/ml_kernel/lisp                           0s  49MB
Feb 08 00:54:42 Starting candle/overloading
Feb 08 00:54:43 Finished candle/overloading                                       0s  11MB
Feb 08 00:54:44 Starting candle/overloading/syntax
Feb 08 00:57:56 Finished candle/overloading/syntax                             3m10s   1GB
Feb 08 00:57:56 Starting candle/overloading/semantics
Feb 08 01:09:00 Finished candle/overloading/semantics                         11m02s   5GB
Feb 08 01:09:01 Starting candle/overloading/monadic
Feb 08 01:11:19 Finished candle/overloading/monadic                            2m17s   2GB
Feb 08 01:11:20 Starting candle/overloading/ml_kernel
Feb 08 01:18:33 Finished candle/overloading/ml_kernel                          7m12s   5GB
Feb 08 01:18:34 Starting candle/overloading/ml_checker
Feb 08 01:20:41 Finished candle/overloading/ml_checker                         2m06s   6GB
Feb 08 01:20:41 Starting candle/prover
Feb 08 01:30:22 Finished candle/prover                                         9m39s   5GB
Feb 08 01:30:23 Starting candle/prover/compute
Feb 08 01:30:25 Finished candle/prover/compute                                    1s 111MB
Feb 08 01:30:26 Starting pancake
Feb 08 01:30:47 Finished pancake                                                 20s 637MB
Feb 08 01:30:48 Starting pancake/semantics
Feb 08 01:32:54 Finished pancake/semantics                                     2m04s   2GB
Feb 08 01:32:55 Starting pancake/parser
Feb 08 01:33:18 Finished pancake/parser                                          22s 460MB
Feb 08 01:33:19 Starting pancake/proofs
Feb 08 01:49:31 Finished pancake/proofs                                       16m11s   7GB
Feb 08 01:49:32 Starting pancake/ta_progs
Feb 08 01:49:33 Finished pancake/ta_progs                                         0s  10MB
Feb 08 01:49:34 Starting compiler/dafny
Feb 08 01:52:06 Finished compiler/dafny                                        2m31s  11GB
Feb 08 01:52:07 Starting compiler/dafny/translation
Feb 08 02:10:07 Finished compiler/dafny/translation                           17m58s  25GB
Feb 08 02:10:07 Starting compiler/dafny/compilation
Feb 08 02:12:41 Finished compiler/dafny/compilation                            2m32s   9GB
Feb 08 02:12:42 Starting compiler/dafny/semantics
Feb 08 02:13:18 Finished compiler/dafny/semantics                                34s   1GB
Feb 08 02:13:19 Starting characteristic/examples
Feb 08 02:14:44 Finished characteristic/examples                               1m24s   4GB
Feb 08 02:14:45 Starting tutorial/solutions
Feb 08 02:17:07 Finished tutorial/solutions                                    2m20s   3GB
Feb 08 02:17:08 Starting translator/monadic/examples
Feb 08 02:20:00 Finished translator/monadic/examples                           2m51s   3GB
Feb 08 02:20:00 Starting examples
Feb 08 02:25:56 Finished examples                                              5m54s   4GB
Feb 08 02:25:57 Starting examples/compilation
Feb 08 02:25:58 Finished examples/compilation                                     0s  11MB
Feb 08 02:25:59 Starting examples/compilation/x64
Feb 08 02:32:35 Finished examples/compilation/x64                              6m35s   3GB
Feb 08 02:32:36 Starting examples/compilation/x64/proofs
Feb 08 02:35:01 Finished examples/compilation/x64/proofs                       2m23s   4GB
Feb 08 02:35:02 Starting examples/compilation/ag32
Feb 08 02:36:47 Finished examples/compilation/ag32                             1m44s   3GB
Feb 08 02:36:48 Starting examples/compilation/ag32/proofs
Feb 08 02:37:48 Finished examples/compilation/ag32/proofs                        59s   5GB
Feb 08 02:37:49 Starting examples/lpr_checker
Feb 08 02:38:19 Finished examples/lpr_checker                                    28s   1GB
Feb 08 02:38:19 Starting examples/lpr_checker/array
Feb 08 03:04:35 Finished examples/lpr_checker/array                           26m14s  24GB
Feb 08 03:04:36 Starting examples/lpr_checker/array/compilation
Feb 08 03:12:55 Finished examples/lpr_checker/array/compilation                8m17s  38GB
Feb 08 03:12:56 Starting examples/lpr_checker/array/compilation/proofs
Feb 08 03:14:08 Finished examples/lpr_checker/array/compilation/proofs         1m10s   6GB
Feb 08 03:14:08 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 08 03:15:17 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Feb 08 03:15:18 Starting .
Feb 08 03:15:22 Finished .                                                        2s 279MB
Feb 08 03:15:23 Starting examples/xlrup_checker
Feb 08 03:15:57 Finished examples/xlrup_checker                                  33s   1GB
Feb 08 03:15:58 Starting examples/xlrup_checker/array
Feb 08 03:28:53 Finished examples/xlrup_checker/array                         12m54s   8GB
Feb 08 03:28:54 Starting examples/xlrup_checker/array/compilation
Feb 08 03:29:52 Finished examples/xlrup_checker/array/compilation                57s   4GB
Feb 08 03:29:53 Starting examples/xlrup_checker/array/compilation/proofs
Feb 08 03:30:56 Finished examples/xlrup_checker/array/compilation/proofs       1m02s   5GB
Feb 08 03:30:57 Starting examples/pseudo_bool
Feb 08 03:32:27 Finished examples/pseudo_bool                                  1m29s   2GB
Feb 08 03:32:28 Starting examples/pseudo_bool/cnf_encoding
Feb 08 03:32:57 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Feb 08 03:32:58 Starting examples/pseudo_bool/graph_encoding
Feb 08 03:33:43 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Feb 08 03:33:43 Starting examples/pseudo_bool/array
Feb 08 04:41:36 Finished examples/pseudo_bool/array                         1h07m51s  44GB
Feb 08 04:41:37 Starting examples/pseudo_bool/array/compilation
Feb 08 04:50:12 Finished examples/pseudo_bool/array/compilation                8m34s  15GB
Feb 08 04:50:13 Starting examples/pseudo_bool/array/compilation/proofs
Feb 08 04:52:49 Finished examples/pseudo_bool/array/compilation/proofs         2m34s   6GB
Feb 08 04:52:50 Starting examples/pseudo_bool/array/compilation/proofsARM8
Feb 08 04:54:02 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m10s   6GB
Feb 08 04:54:03 Starting examples/opentheory
Feb 08 05:02:29 Finished examples/opentheory                                   8m25s   6GB
Feb 08 05:02:30 Starting examples/opentheory/compilation
Feb 08 05:03:54 Finished examples/opentheory/compilation                       1m22s   5GB
Feb 08 05:03:55 Starting examples/opentheory/compilation/proofs
Feb 08 05:04:51 Finished examples/opentheory/compilation/proofs                  55s   4GB
Feb 08 05:04:52 Starting examples/opentheory/compilation/ag32
Feb 08 05:06:21 Finished examples/opentheory/compilation/ag32                  1m27s   6GB
Feb 08 05:06:22 Starting examples/opentheory/compilation/ag32/proofs
Feb 08 05:07:59 Finished examples/opentheory/compilation/ag32/proofs           1m36s   8GB
Feb 08 05:08:00 Starting examples/sat_encodings
Feb 08 05:09:00 Finished examples/sat_encodings                                  58s 762MB
Feb 08 05:09:01 Starting examples/sat_encodings/demo
Feb 08 05:09:02 Finished examples/sat_encodings/demo                              0s  11MB
Feb 08 05:09:03 Starting examples/sat_encodings/case_studies
Feb 08 05:10:49 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Feb 08 05:10:49 Starting examples/sat_encodings/translation
Feb 08 05:14:31 Finished examples/sat_encodings/translation                    3m40s   3GB
Feb 08 05:14:32 Starting examples/sat_encodings/translation/compilation
Feb 08 05:16:18 Finished examples/sat_encodings/translation/compilation        1m45s   4GB
Feb 08 05:16:19 Starting examples/deflate
Feb 08 05:16:47 Finished examples/deflate                                        27s 682MB
Feb 08 05:16:48 Starting examples/deflate/translation
Feb 08 05:17:53 Finished examples/deflate/translation                          1m04s   4GB
Feb 08 05:17:54 Starting examples/deflate/translation/compilation
Feb 08 05:18:41 Finished examples/deflate/translation/compilation                45s   3GB
Feb 08 05:18:41 Starting examples/vipr
Feb 08 05:22:19 Finished examples/vipr                                         3m36s   7GB
Feb 08 05:22:20 Starting examples/vipr/compilation
Feb 08 05:23:13 Finished examples/vipr/compilation                               52s   4GB
Feb 08 05:23:14 Starting translator/okasaki-examples
Feb 08 05:27:13 Finished translator/okasaki-examples                           3m58s   4GB
Feb 08 05:27:14 Starting translator/other-examples
Feb 08 05:28:07 Finished translator/other-examples                               51s   3GB
Feb 08 05:28:08 Starting translator/other-examples/auxiliary
Feb 08 05:28:09 Finished translator/other-examples/auxiliary                      0s  11MB
Feb 08 05:28:10 Starting compiler/parsing/tests
Feb 08 05:28:45 Finished compiler/parsing/tests                                  33s   1GB
Feb 08 05:28:46 Starting compiler/inference/tests
Feb 08 05:29:22 Finished compiler/inference/tests                                35s   2GB
Feb 08 05:29:23 Starting compiler/printing/test
Feb 08 05:30:37 Finished compiler/printing/test                                1m12s   5GB
Feb 08 05:30:38 Starting icing/flover
Feb 08 06:04:57 Finished icing/flover                                         34m18s   2GB
Feb 08 06:04:58 Starting icing/flover/Infra
Feb 08 06:04:59 Finished icing/flover/Infra                                       0s  11MB
Feb 08 06:05:00 Starting icing/flover/semantics
Feb 08 06:05:01 Finished icing/flover/semantics                                   0s  12MB
Feb 08 06:05:02 Starting icing/
Feb 08 06:32:30 Finished icing/                                               27m27s   7GB
Feb 08 06:32:31 Starting icing/examples
Feb 08 06:34:04 Finished icing/examples                                        1m32s   7GB
Feb 08 06:34:05 Starting compiler/repl
Feb 08 06:41:58 Finished compiler/repl                                         7m51s   7GB
Feb 08 06:41:59 Starting unverified/sexpr-bootstrap/x64/64
Feb 08 06:46:12 Finished unverified/sexpr-bootstrap/x64/64                     3m59s  15GB
Feb 08 06:46:13 Starting unverified/sexpr-bootstrap/x64/32
Feb 08 06:49:39 Finished unverified/sexpr-bootstrap/x64/32                     3m15s  15GB
Feb 08 06:49:40 Starting compiler/benchmarks
Feb 08 06:50:26 Finished compiler/benchmarks                                     44s 712MB
Feb 08 06:50:27 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 08 06:50:30 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 236MB
Feb 08 06:50:31 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 08 06:50:34 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 257MB
Feb 08 06:50:35 Starting compiler/bootstrap/compilation/x64/64
Feb 08 07:12:22 Finished compiler/bootstrap/compilation/x64/64                21m35s  52GB
Feb 08 07:12:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 08 07:36:06 Finished compiler/bootstrap/compilation/x64/64/proofs         23m42s  47GB
Feb 08 07:36:07 Starting compiler/bootstrap/compilation/x64/32
Feb 08 08:00:33 Finished compiler/bootstrap/compilation/x64/32                24m19s  64GB
Feb 08 08:00:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 08 08:05:01 Finished compiler/bootstrap/compilation/x64/32/proofs          4m26s  23GB
Feb 08 08:05:02 Starting compiler/bootstrap/compilation/arm8/64
Feb 08 08:41:41 Finished compiler/bootstrap/compilation/arm8/64               36m30s  88GB
Feb 08 08:41:42 Starting compiler/bootstrap/compilation/arm8/64/proofs
Feb 08 08:46:41 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m57s  29GB
Feb 08 08:46:42 Starting compiler/bootstrap/compilation/ag32/32
Feb 08 09:13:04 Finished compiler/bootstrap/compilation/ag32/32               26m21s  76GB
Feb 08 09:13:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 08 09:17:47 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m41s  30GB
Feb 08 09:17:48 SUCCESS