Job 2825

CakeML:2cb913bafb3f7b8bc061e5c7001747bf1c7f018e
  remove duplicate lemma [May 05 20:10:54]
#1165 (pancake_internal32bit)
Merging into:421f54d7feabd143e522e58d881f9e23c63bf934
  Merge pull request #1175 from CakeML/mcandidate-fix [May 10 11:20:24]
HOL:725300ce5d22e30174177682d5870306852113d5
  Apply a patch to lem_relation before Holmake runs [May 09 00:00:24]
Machine:pavlova

May 12 12:38:01 Claimed job
May 12 12:38:08 Reusing HOL
May 12 12:38:19 Starting developers
May 12 12:38:23 Finished developers                                               3s 163MB
May 12 12:38:24 Starting developers/bin
May 12 12:38:30 Finished developers/bin                                           4s 591MB
May 12 12:38:31 Starting misc
May 12 12:39:12 Finished misc                                                    40s   2GB
May 12 12:39:13 Starting compiler/proofs
May 12 14:17:06 Finished compiler/proofs                                    1h37m52s  37GB
May 12 14:17:07 Starting compiler/bootstrap/translation
May 12 19:56:42 Finished compiler/bootstrap/translation                     5h39m33s  87GB
May 12 19:56:43 Starting semantics/ffi
May 12 19:56:52 Finished semantics/ffi                                            8s 548MB
May 12 19:56:53 Starting semantics
May 12 19:56:54 Finished semantics                                                0s  54MB
May 12 19:56:55 Starting semantics/proofs
May 12 19:57:18 Finished semantics/proofs                                        22s 712MB
May 12 19:57:19 Starting semantics/alt_semantics
May 12 19:57:39 Finished semantics/alt_semantics                                 19s 670MB
May 12 19:57:40 Starting semantics/alt_semantics/proofs
May 12 20:07:58 Finished semantics/alt_semantics/proofs                       10m17s   2GB
May 12 20:07:59 Starting basis/pure
May 12 20:08:01 Finished basis/pure                                               0s  94MB
May 12 20:08:02 Starting translator
May 12 20:09:35 Finished translator                                            1m32s   2GB
May 12 20:09:36 Starting compiler/parsing
May 12 20:09:38 Finished compiler/parsing                                         0s  60MB
May 12 20:09:38 Starting characteristic
May 12 20:09:40 Finished characteristic                                           1s 123MB
May 12 20:09:41 Starting translator/monadic
May 12 20:09:43 Finished translator/monadic                                       1s 114MB
May 12 20:09:44 Starting translator/monadic/monad_base
May 12 20:09:46 Finished translator/monadic/monad_base                            0s  50MB
May 12 20:09:47 Starting basis
May 12 20:12:06 Finished basis                                                 2m18s   4GB
May 12 20:12:07 Starting compiler
May 12 20:12:09 Finished compiler                                                 1s 210MB
May 12 20:12:10 Starting compiler/inference
May 12 20:12:12 Finished compiler/inference                                       1s 115MB
May 12 20:12:13 Starting compiler/backend/reg_alloc
May 12 20:12:14 Finished compiler/backend/reg_alloc                               0s  55MB
May 12 20:12:15 Starting compiler/backend/gc
May 12 20:12:17 Finished compiler/backend/gc                                      1s 139MB
May 12 20:12:18 Starting compiler/backend
May 12 20:12:23 Finished compiler/backend                                         4s 250MB
May 12 20:12:24 Starting compiler/encoders/asm
May 12 20:12:26 Finished compiler/encoders/asm                                    0s  84MB
May 12 20:12:27 Starting compiler/encoders/x64
May 12 20:12:28 Finished compiler/encoders/x64                                    0s  89MB
May 12 20:12:29 Starting compiler/encoders/arm7
May 12 20:12:31 Finished compiler/encoders/arm7                                   0s  89MB
May 12 20:12:32 Starting compiler/encoders/arm8
May 12 20:12:33 Finished compiler/encoders/arm8                                   0s  82MB
May 12 20:12:34 Starting compiler/encoders/arm8_asl
May 12 22:12:54 Finished compiler/encoders/arm8_asl                         2h00m17s  29GB
May 12 22:12:55 Starting compiler/encoders/mips
May 12 22:12:56 Finished compiler/encoders/mips                                   0s  82MB
May 12 22:12:57 Starting compiler/encoders/riscv
May 12 22:12:59 Finished compiler/encoders/riscv                                  0s  88MB
May 12 22:13:00 Starting compiler/encoders/ag32
May 12 22:13:01 Finished compiler/encoders/ag32                                   0s  87MB
May 12 22:13:02 Starting compiler/encoders/tests
May 12 22:13:04 Finished compiler/encoders/tests                                  0s 112MB
May 12 22:13:05 Starting compiler/encoders/monadic_enc
May 12 22:13:07 Finished compiler/encoders/monadic_enc                            1s 127MB
May 12 22:13:08 Starting compiler/backend/x64
May 12 22:13:10 Finished compiler/backend/x64                                     1s 134MB
May 12 22:13:11 Starting compiler/backend/arm7
May 12 22:13:13 Finished compiler/backend/arm7                                    1s 135MB
May 12 22:13:14 Starting compiler/backend/arm8
May 12 22:13:16 Finished compiler/backend/arm8                                    1s 135MB
May 12 22:13:17 Starting compiler/backend/mips
May 12 22:13:19 Finished compiler/backend/mips                                    1s 128MB
May 12 22:13:20 Starting compiler/backend/riscv
May 12 22:13:22 Finished compiler/backend/riscv                                   1s 135MB
May 12 22:13:23 Starting compiler/backend/ag32
May 12 22:14:29 Finished compiler/backend/ag32                                 1m05s   3GB
May 12 22:14:30 Starting compiler/backend/pattern_matching
May 12 22:14:31 Finished compiler/backend/pattern_matching                        0s  54MB
May 12 22:14:32 Starting compiler/parsing/ocaml
May 12 22:16:13 Finished compiler/parsing/ocaml                                1m39s   1GB
May 12 22:16:14 Starting compiler/printing
May 12 22:16:16 Finished compiler/printing                                        1s 111MB
May 12 22:16:17 Starting compiler/parsing/proofs
May 12 22:16:18 Finished compiler/parsing/proofs                                  0s  61MB
May 12 22:16:19 Starting compiler/inference/proofs
May 12 22:16:21 Finished compiler/inference/proofs                                1s 115MB
May 12 22:16:22 Starting compiler/backend/semantics
May 12 22:19:25 Finished compiler/backend/semantics                            3m02s   3GB
May 12 22:19:26 Starting compiler/backend/reg_alloc/proofs
May 12 22:19:28 Finished compiler/backend/reg_alloc/proofs                        1s 115MB
May 12 22:19:29 Starting compiler/backend/proofs
May 12 22:20:13 Finished compiler/backend/proofs                                 43s   2GB
May 12 22:20:14 Starting compiler/backend/serialiser
May 12 22:20:16 Finished compiler/backend/serialiser                              1s 142MB
May 12 22:20:17 Starting compiler/encoders/x64/proofs
May 12 22:30:19 Finished compiler/encoders/x64/proofs                         10m01s   4GB
May 12 22:30:20 Starting compiler/encoders/arm7/proofs
May 12 22:43:14 Finished compiler/encoders/arm7/proofs                        12m51s   5GB
May 12 22:43:15 Starting compiler/encoders/arm8/proofs
May 12 22:50:14 Finished compiler/encoders/arm8/proofs                         6m57s   4GB
May 12 22:50:14 Starting compiler/encoders/arm8_asl/proofs
May 12 23:39:31 Finished compiler/encoders/arm8_asl/proofs                    49m15s  20GB
May 12 23:39:32 Starting compiler/encoders/mips/proofs
May 12 23:49:23 Finished compiler/encoders/mips/proofs                         9m50s   3GB
May 12 23:49:24 Starting compiler/encoders/riscv/proofs
May 12 23:57:44 Finished compiler/encoders/riscv/proofs                        8m18s   3GB
May 12 23:57:45 Starting compiler/encoders/ag32/proofs
May 13 00:00:35 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
May 13 00:00:36 Starting compiler/backend/x64/proofs
May 13 00:01:05 Finished compiler/backend/x64/proofs                             28s   2GB
May 13 00:01:06 Starting compiler/backend/arm7/proofs
May 13 00:01:35 Finished compiler/backend/arm7/proofs                            27s   1GB
May 13 00:01:36 Starting compiler/backend/arm8/proofs
May 13 00:02:07 Finished compiler/backend/arm8/proofs                            29s   2GB
May 13 00:02:08 Starting compiler/backend/arm8_asl
May 13 00:02:30 Finished compiler/backend/arm8_asl                               21s   1GB
May 13 00:02:31 Starting compiler/backend/mips/proofs
May 13 00:03:00 Finished compiler/backend/mips/proofs                            28s   1GB
May 13 00:03:01 Starting compiler/backend/riscv/proofs
May 13 00:03:31 Finished compiler/backend/riscv/proofs                           29s   2GB
May 13 00:03:32 Starting compiler/backend/ag32/proofs
May 13 00:17:08 Finished compiler/backend/ag32/proofs                         13m35s   5GB
May 13 00:17:09 Starting compiler/backend/cv_compute
May 13 00:18:16 Finished compiler/backend/cv_compute                           1m06s   2GB
May 13 00:18:17 Starting cv_translator
May 13 00:38:24 Finished cv_translator                                        20m05s   8GB
May 13 00:38:25 Starting candle
May 13 00:38:26 Finished candle                                                   0s  11MB
May 13 00:38:27 Starting candle/set-theory
May 13 00:38:59 Finished candle/set-theory                                       31s   1GB
May 13 00:39:00 Starting candle/syntax-lib
May 13 00:39:02 Finished candle/syntax-lib                                        0s  94MB
May 13 00:39:03 Starting candle/standard
May 13 00:39:03 Finished candle/standard                                          0s  12MB
May 13 00:39:05 Starting candle/standard/syntax
May 13 00:39:16 Finished candle/standard/syntax                                  10s 746MB
May 13 00:39:17 Starting candle/standard/semantics
May 13 00:41:16 Finished candle/standard/semantics                             1m57s   2GB
May 13 00:41:17 Starting candle/standard/monadic
May 13 00:41:19 Finished candle/standard/monadic                                  1s 121MB
May 13 00:41:20 Starting candle/standard/ml_kernel
May 13 00:43:03 Finished candle/standard/ml_kernel                             1m42s   4GB
May 13 00:43:04 Starting candle/standard/ml_kernel/lisp
May 13 00:43:05 Finished candle/standard/ml_kernel/lisp                           0s  47MB
May 13 00:43:06 Starting candle/overloading
May 13 00:43:07 Finished candle/overloading                                       0s  12MB
May 13 00:43:08 Starting candle/overloading/syntax
May 13 00:46:14 Finished candle/overloading/syntax                             3m04s   1GB
May 13 00:46:15 Starting candle/overloading/semantics
May 13 00:57:03 Finished candle/overloading/semantics                         10m47s   3GB
May 13 00:57:04 Starting candle/overloading/monadic
May 13 00:59:16 Finished candle/overloading/monadic                            2m10s   2GB
May 13 00:59:16 Starting candle/overloading/ml_kernel
May 13 01:06:21 Finished candle/overloading/ml_kernel                          7m03s   5GB
May 13 01:06:22 Starting candle/overloading/ml_checker
May 13 01:08:34 Finished candle/overloading/ml_checker                         2m11s   6GB
May 13 01:08:35 Starting candle/prover
May 13 01:18:05 Finished candle/prover                                         9m28s   5GB
May 13 01:18:06 Starting candle/prover/compute
May 13 01:18:08 Finished candle/prover/compute                                    1s 152MB
May 13 01:18:09 Starting pancake
May 13 01:18:11 Finished pancake                                                  1s 131MB
May 13 01:18:12 Starting pancake/semantics
May 13 01:20:18 Finished pancake/semantics                                     2m05s   1GB
May 13 01:20:19 Starting pancake/parser
May 13 01:20:43 Finished pancake/parser                                          23s 479MB
May 13 01:20:44 Starting pancake/static_checker
May 13 01:21:21 Finished pancake/static_checker                                  35s   1GB
May 13 01:21:22 Starting pancake/proofs
May 13 01:37:29 Finished pancake/proofs                                       16m06s   5GB
May 13 01:37:30 Starting compiler/dafny
May 13 01:40:21 Finished compiler/dafny                                        2m49s  10GB
May 13 01:40:22 Starting compiler/dafny/translation
May 13 02:00:03 Finished compiler/dafny/translation                           19m40s  26GB
May 13 02:00:04 Starting compiler/dafny/compilation
May 13 02:03:03 Finished compiler/dafny/compilation                            2m57s   9GB
May 13 02:03:03 Starting compiler/dafny/semantics
May 13 02:03:41 Finished compiler/dafny/semantics                                36s   1GB
May 13 02:03:42 Starting characteristic/examples
May 13 02:05:09 Finished characteristic/examples                               1m25s   4GB
May 13 02:05:09 Starting tutorial/solutions
May 13 02:07:32 Finished tutorial/solutions                                    2m21s   3GB
May 13 02:07:33 Starting translator/monadic/examples
May 13 02:10:25 Finished translator/monadic/examples                           2m50s   3GB
May 13 02:10:26 Starting examples
May 13 02:16:25 Finished examples                                              5m58s   5GB
May 13 02:16:26 Starting examples/compilation
May 13 02:16:27 Finished examples/compilation                                     0s  11MB
May 13 02:16:28 Starting examples/compilation/x64
May 13 02:23:27 Finished examples/compilation/x64                              6m58s   4GB
May 13 02:23:28 Starting examples/compilation/x64/proofs
May 13 02:25:47 Finished examples/compilation/x64/proofs                       2m17s   4GB
May 13 02:25:48 Starting examples/compilation/ag32
May 13 02:27:44 Finished examples/compilation/ag32                             1m54s   3GB
May 13 02:27:45 Starting examples/compilation/ag32/proofs
May 13 02:28:45 Finished examples/compilation/ag32/proofs                        59s   4GB
May 13 02:28:46 Starting examples/lpr_checker
May 13 02:29:16 Finished examples/lpr_checker                                    29s   1GB
May 13 02:29:17 Starting examples/lpr_checker/array
May 13 02:55:11 Finished examples/lpr_checker/array                           25m52s  18GB
May 13 02:55:12 Starting examples/lpr_checker/array/compilation
May 13 02:57:36 Finished examples/lpr_checker/array/compilation                2m23s   7GB
May 13 02:57:37 Starting examples/lpr_checker/array/compilation/proofs
May 13 02:58:46 Finished examples/lpr_checker/array/compilation/proofs         1m08s   5GB
May 13 02:58:47 Starting examples/lpr_checker/array/compilation/proofsARM8
May 13 02:59:55 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
May 13 02:59:56 Starting .
May 13 03:00:00 Finished .                                                        2s 319MB
May 13 03:00:01 Starting examples/xlrup_checker
May 13 03:00:35 Finished examples/xlrup_checker                                  33s   1GB
May 13 03:00:36 Starting examples/xlrup_checker/array
May 13 03:13:35 Finished examples/xlrup_checker/array                         12m57s   8GB
May 13 03:13:36 Starting examples/xlrup_checker/array/compilation
May 13 03:14:39 Finished examples/xlrup_checker/array/compilation              1m00s   4GB
May 13 03:14:39 Starting examples/xlrup_checker/array/compilation/proofs
May 13 03:15:41 Finished examples/xlrup_checker/array/compilation/proofs       1m00s   5GB
May 13 03:15:42 Starting examples/pseudo_bool
May 13 03:17:13 Finished examples/pseudo_bool                                  1m30s   2GB
May 13 03:17:14 Starting examples/pseudo_bool/cnf_encoding
May 13 03:17:42 Finished examples/pseudo_bool/cnf_encoding                       26s   1GB
May 13 03:17:43 Starting examples/pseudo_bool/graph_encoding
May 13 03:18:25 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
May 13 03:18:26 Starting examples/pseudo_bool/array
May 13 04:26:53 Finished examples/pseudo_bool/array                         1h08m25s  26GB
May 13 04:26:54 Starting examples/pseudo_bool/array/compilation
May 13 04:36:48 Finished examples/pseudo_bool/array/compilation                9m52s  19GB
May 13 04:36:49 Starting examples/pseudo_bool/array/compilation/proofs
May 13 04:39:23 Finished examples/pseudo_bool/array/compilation/proofs         2m32s   6GB
May 13 04:39:24 Starting examples/pseudo_bool/array/compilation/proofsARM8
May 13 04:40:37 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m12s   6GB
May 13 04:40:38 Starting examples/opentheory
May 13 04:49:18 Finished examples/opentheory                                   8m38s   7GB
May 13 04:49:19 Starting examples/opentheory/compilation
May 13 04:50:53 Finished examples/opentheory/compilation                       1m33s   7GB
May 13 04:50:54 Starting examples/opentheory/compilation/proofs
May 13 04:51:54 Finished examples/opentheory/compilation/proofs                  59s   4GB
May 13 04:51:55 Starting examples/opentheory/compilation/ag32
May 13 04:53:31 Finished examples/opentheory/compilation/ag32                  1m35s   7GB
May 13 04:53:32 Starting examples/opentheory/compilation/ag32/proofs
May 13 04:55:11 Finished examples/opentheory/compilation/ag32/proofs           1m37s   8GB
May 13 04:55:12 Starting examples/sat_encodings
May 13 04:56:12 Finished examples/sat_encodings                                  59s 929MB
May 13 04:56:13 Starting examples/sat_encodings/demo
May 13 04:56:14 Finished examples/sat_encodings/demo                              0s  11MB
May 13 04:56:15 Starting examples/sat_encodings/case_studies
May 13 04:57:57 Finished examples/sat_encodings/case_studies                   1m41s   1GB
May 13 04:57:58 Starting examples/sat_encodings/translation
May 13 05:01:30 Finished examples/sat_encodings/translation                    3m31s   2GB
May 13 05:01:31 Starting examples/sat_encodings/translation/compilation
May 13 05:03:27 Finished examples/sat_encodings/translation/compilation        1m55s   4GB
May 13 05:03:28 Starting examples/deflate
May 13 05:03:56 Finished examples/deflate                                        26s 682MB
May 13 05:03:57 Starting examples/deflate/translation
May 13 05:05:01 Finished examples/deflate/translation                          1m03s   4GB
May 13 05:05:02 Starting examples/deflate/translation/compilation
May 13 05:05:53 Finished examples/deflate/translation/compilation                49s   3GB
May 13 05:05:54 Starting examples/vipr
May 13 05:09:04 Finished examples/vipr                                         3m09s   4GB
May 13 05:09:05 Starting examples/vipr/compilation
May 13 05:10:01 Finished examples/vipr/compilation                               55s   4GB
May 13 05:10:02 Starting translator/okasaki-examples
May 13 05:14:04 Finished translator/okasaki-examples                           4m01s   3GB
May 13 05:14:05 Starting translator/other-examples
May 13 05:16:24 Finished translator/other-examples                             2m17s   1GB
May 13 05:16:24 Starting translator/other-examples/auxiliary
May 13 05:16:25 Finished translator/other-examples/auxiliary                      0s  14MB
May 13 05:16:26 Starting compiler/parsing/tests
May 13 05:17:01 Finished compiler/parsing/tests                                  33s   1GB
May 13 05:17:02 Starting compiler/inference/tests
May 13 05:17:37 Finished compiler/inference/tests                                33s   2GB
May 13 05:17:38 Starting compiler/printing/test
May 13 05:18:48 Finished compiler/printing/test                                1m09s   5GB
May 13 05:18:49 Starting icing/flover
May 13 05:51:16 Finished icing/flover                                         32m24s   2GB
May 13 05:51:17 Starting icing/flover/Infra
May 13 05:51:18 Finished icing/flover/Infra                                       0s  13MB
May 13 05:51:19 Starting icing/flover/semantics
May 13 05:51:20 Finished icing/flover/semantics                                   0s  14MB
May 13 05:51:21 Starting icing/
May 13 06:17:36 Finished icing/                                               26m12s   4GB
May 13 06:17:37 Starting icing/examples
May 13 06:19:02 Finished icing/examples                                        1m23s   7GB
May 13 06:19:03 Starting compiler/repl
May 13 06:26:56 Finished compiler/repl                                         7m52s   8GB
May 13 06:26:56 Starting unverified/sexpr-bootstrap/x64/64
May 13 06:30:46 Finished unverified/sexpr-bootstrap/x64/64                     3m48s  15GB
May 13 06:30:47 Starting unverified/sexpr-bootstrap/x64/32
May 13 06:33:57 Finished unverified/sexpr-bootstrap/x64/32                     3m08s  14GB
May 13 06:33:58 Starting compiler/benchmarks
May 13 06:34:44 Finished compiler/benchmarks                                     44s 712MB
May 13 06:34:45 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
May 13 06:34:48 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 262MB
May 13 06:34:49 Starting compiler/benchmarks/mlton_benchmarks/cakeml
May 13 06:34:52 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 252MB
May 13 06:34:53 Starting compiler/bootstrap/compilation/x64/64
May 13 07:03:50 Finished compiler/bootstrap/compilation/x64/64                28m54s 114GB
May 13 07:03:51 Starting compiler/bootstrap/compilation/x64/64/proofs
May 13 07:27:54 Finished compiler/bootstrap/compilation/x64/64/proofs         24m02s  55GB
May 13 07:27:55 Starting compiler/bootstrap/compilation/x64/32
May 13 07:58:26 Finished compiler/bootstrap/compilation/x64/32                30m29s  71GB
May 13 07:58:27 Starting compiler/bootstrap/compilation/x64/32/proofs
May 13 08:02:33 Finished compiler/bootstrap/compilation/x64/32/proofs          4m05s  24GB
May 13 08:02:34 Starting compiler/bootstrap/compilation/arm8/64
May 13 08:44:18 Finished compiler/bootstrap/compilation/arm8/64               41m41s 113GB
May 13 08:44:19 Starting compiler/bootstrap/compilation/arm8/64/proofs
May 13 08:50:04 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m44s  30GB
May 13 08:50:05 Starting compiler/bootstrap/compilation/ag32/32
May 13 09:19:40 Finished compiler/bootstrap/compilation/ag32/32               29m33s  86GB
May 13 09:19:41 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 13 09:24:29 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m47s  29GB
May 13 09:24:30 SUCCESS