Job 1772

CakeML:67b312862a2b9919d20a41b16a6599ef4a7635fe
  Merge pull request #855 from CakeML/minor-reheapification [Feb 14 13:06:51]
HOL:7d8123fd0cb1e8c2b7e3fffb337516da7cb7c9df
  Reinstate sptreeTheory.lrnext_def, which 8247e5e3a465 had deleted [Feb 10 23:16:16]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 14 23:07:30 Claimed job
Feb 14 23:07:32 Reusing HOL
Feb 14 23:07:44 Starting developers
Feb 14 23:07:49 Finished developers                                               4s 115MB
Feb 14 23:07:49 Starting developers/bin
Feb 14 23:07:53 Finished developers/bin                                           4s 675MB
Feb 14 23:07:53 Starting semantics/ffi
Feb 14 23:08:02 Finished semantics/ffi                                            8s 234MB
Feb 14 23:08:02 Starting semantics
Feb 14 23:09:42 Finished semantics                                             1m39s   1GB
Feb 14 23:09:42 Starting semantics/proofs
Feb 14 23:13:16 Finished semantics/proofs                                      3m33s 923MB
Feb 14 23:13:16 Starting semantics/alt_semantics
Feb 14 23:13:29 Finished semantics/alt_semantics                                 13s 449MB
Feb 14 23:13:29 Starting semantics/alt_semantics/proofs
Feb 14 23:15:58 Finished semantics/alt_semantics/proofs                        2m28s 851MB
Feb 14 23:15:58 Starting basis/pure
Feb 14 23:16:50 Finished basis/pure                                              51s 698MB
Feb 14 23:16:50 Starting translator
Feb 14 23:19:44 Finished translator                                            2m53s   1GB
Feb 14 23:19:44 Starting compiler/parsing
Feb 14 23:20:58 Finished compiler/parsing                                      1m13s   2GB
Feb 14 23:20:58 Starting characteristic
Feb 14 23:26:53 Finished characteristic                                        5m54s   1GB
Feb 14 23:26:53 Starting translator/monadic
Feb 14 23:28:38 Finished translator/monadic                                    1m45s   1GB
Feb 14 23:28:38 Starting basis
Feb 15 00:14:12 Finished basis                                                45m30s  14GB
Feb 15 00:14:13 Starting compiler/inference
Feb 15 00:15:23 Finished compiler/inference                                    1m10s   1GB
Feb 15 00:15:23 Starting compiler/backend/reg_alloc
Feb 15 00:16:29 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 15 00:16:29 Starting compiler/backend/gc
Feb 15 00:19:59 Finished compiler/backend/gc                                   3m29s   1GB
Feb 15 00:19:59 Starting compiler/backend
Feb 15 00:25:06 Finished compiler/backend                                      5m06s   2GB
Feb 15 00:25:06 Starting compiler/encoders/asm
Feb 15 00:25:30 Finished compiler/encoders/asm                                   23s 701MB
Feb 15 00:25:30 Starting compiler/encoders/x64
Feb 15 00:25:57 Finished compiler/encoders/x64                                   26s 790MB
Feb 15 00:25:57 Starting compiler/encoders/arm7
Feb 15 00:26:48 Finished compiler/encoders/arm7                                  51s   1GB
Feb 15 00:26:49 Starting compiler/encoders/arm8
Feb 15 00:27:03 Finished compiler/encoders/arm8                                  13s 907MB
Feb 15 00:27:03 Starting compiler/encoders/arm8_asl
Feb 15 00:29:34 Finished compiler/encoders/arm8_asl                            2m31s 970MB
Feb 15 00:29:34 Starting compiler/encoders/mips
Feb 15 00:29:53 Finished compiler/encoders/mips                                  18s   1GB
Feb 15 00:29:53 Starting compiler/encoders/riscv
Feb 15 00:30:09 Finished compiler/encoders/riscv                                 15s 809MB
Feb 15 00:30:09 Starting compiler/encoders/ag32
Feb 15 00:30:29 Finished compiler/encoders/ag32                                  19s 755MB
Feb 15 00:30:29 Starting compiler/backend/x64
Feb 15 00:30:50 Finished compiler/backend/x64                                    20s   1GB
Feb 15 00:30:50 Starting compiler/backend/arm7
Feb 15 00:31:13 Finished compiler/backend/arm7                                   23s   1GB
Feb 15 00:31:13 Starting compiler/backend/arm8
Feb 15 00:31:35 Finished compiler/backend/arm8                                   21s   1GB
Feb 15 00:31:35 Starting compiler/backend/mips
Feb 15 00:31:57 Finished compiler/backend/mips                                   21s   1GB
Feb 15 00:31:57 Starting compiler/backend/riscv
Feb 15 00:32:19 Finished compiler/backend/riscv                                  21s   1GB
Feb 15 00:32:19 Starting compiler/backend/ag32
Feb 15 00:33:28 Finished compiler/backend/ag32                                 1m09s   1GB
Feb 15 00:33:28 Starting compiler/parsing/proofs
Feb 15 00:37:12 Finished compiler/parsing/proofs                               3m43s   1GB
Feb 15 00:37:13 Starting compiler/inference/proofs
Feb 15 00:39:40 Finished compiler/inference/proofs                             2m27s 952MB
Feb 15 00:39:40 Starting compiler/backend/semantics
Feb 15 01:08:12 Finished compiler/backend/semantics                           28m31s   2GB
Feb 15 01:08:13 Starting compiler/backend/reg_alloc/proofs
Feb 15 01:11:46 Finished compiler/backend/reg_alloc/proofs                     3m33s 780MB
Feb 15 01:11:46 Starting compiler/backend/proofs
Feb 15 02:03:34 Finished compiler/backend/proofs                              51m47s  17GB
Feb 15 02:03:35 Starting compiler/backend/serialiser
Feb 15 02:05:03 Finished compiler/backend/serialiser                           1m28s   2GB
Feb 15 02:05:03 Starting compiler/encoders/x64/proofs
Feb 15 02:14:36 Finished compiler/encoders/x64/proofs                          9m33s   5GB
Feb 15 02:14:36 Starting compiler/encoders/arm7/proofs
Feb 15 02:27:45 Finished compiler/encoders/arm7/proofs                        13m08s   6GB
Feb 15 02:27:45 Starting compiler/encoders/arm8/proofs
Feb 15 02:34:36 Finished compiler/encoders/arm8/proofs                         6m50s   1GB
Feb 15 02:34:36 Starting compiler/encoders/arm8_asl/proofs
Feb 15 02:49:49 Finished compiler/encoders/arm8_asl/proofs                    15m13s   2GB
Feb 15 02:49:50 Starting compiler/encoders/mips/proofs
Feb 15 02:59:40 Finished compiler/encoders/mips/proofs                         9m49s   3GB
Feb 15 02:59:40 Starting compiler/encoders/riscv/proofs
Feb 15 03:08:34 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Feb 15 03:08:35 Starting compiler/encoders/ag32/proofs
Feb 15 03:11:15 Finished compiler/encoders/ag32/proofs                         2m39s 674MB
Feb 15 03:11:15 Starting compiler/backend/x64/proofs
Feb 15 03:11:41 Finished compiler/backend/x64/proofs                             26s   1GB
Feb 15 03:11:41 Starting compiler/backend/arm7/proofs
Feb 15 03:12:09 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 15 03:12:10 Starting compiler/backend/arm8/proofs
Feb 15 03:12:37 Finished compiler/backend/arm8/proofs                            26s   1GB
Feb 15 03:12:37 Starting compiler/backend/arm8_asl
Feb 15 03:12:59 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 15 03:12:59 Starting compiler/backend/mips/proofs
Feb 15 03:13:26 Finished compiler/backend/mips/proofs                            26s   1GB
Feb 15 03:13:26 Starting compiler/backend/riscv/proofs
Feb 15 03:13:53 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 15 03:13:53 Starting compiler/backend/ag32/proofs
Feb 15 03:26:41 Finished compiler/backend/ag32/proofs                         12m47s   2GB
Feb 15 03:26:42 Starting compiler/proofs
Feb 15 03:28:41 Finished compiler/proofs                                       1m59s   4GB
Feb 15 03:28:41 Starting candle/set-theory
Feb 15 03:29:10 Finished candle/set-theory                                       28s 848MB
Feb 15 03:29:10 Starting candle/syntax-lib
Feb 15 03:29:21 Finished candle/syntax-lib                                       11s 723MB
Feb 15 03:29:21 Starting candle/standard/syntax
Feb 15 03:31:12 Finished candle/standard/syntax                                1m50s 934MB
Feb 15 03:31:12 Starting candle/standard/semantics
Feb 15 03:33:00 Finished candle/standard/semantics                             1m47s   1GB
Feb 15 03:33:00 Starting candle/standard/monadic
Feb 15 03:34:36 Finished candle/standard/monadic                               1m36s   1GB
Feb 15 03:34:36 Starting candle/standard/ml_kernel
Feb 15 03:41:20 Finished candle/standard/ml_kernel                             6m43s   4GB
Feb 15 03:41:20 Starting candle/overloading/syntax
Feb 15 03:44:28 Finished candle/overloading/syntax                             3m07s   1GB
Feb 15 03:44:28 Starting candle/overloading/semantics
Feb 15 03:56:11 Finished candle/overloading/semantics                         11m42s   2GB
Feb 15 03:56:11 Starting candle/overloading/monadic
Feb 15 03:58:26 Finished candle/overloading/monadic                            2m15s   1GB
Feb 15 03:58:26 Starting candle/overloading/ml_kernel
Feb 15 04:06:02 Finished candle/overloading/ml_kernel                          7m35s   3GB
Feb 15 04:06:02 Starting candle/overloading/ml_checker
Feb 15 04:08:31 Finished candle/overloading/ml_checker                         2m29s   3GB
Feb 15 04:08:31 Starting candle/prover
Feb 15 04:16:12 Finished candle/prover                                         7m39s   3GB
Feb 15 04:16:12 Starting pancake
Feb 15 04:18:52 Finished pancake                                               2m40s   2GB
Feb 15 04:18:53 Starting pancake/ffi
Feb 15 04:18:53 Finished pancake/ffi                                              0s  35MB
Feb 15 04:18:53 Starting pancake/semantics
Feb 15 04:21:21 Finished pancake/semantics                                     2m28s   1GB
Feb 15 04:21:21 Starting pancake/proofs
Feb 15 04:33:26 Finished pancake/proofs                                       12m04s   5GB
Feb 15 04:33:26 Starting characteristic/examples
Feb 15 04:35:00 Finished characteristic/examples                               1m33s   2GB
Feb 15 04:35:00 Starting tutorial/solutions
Feb 15 04:51:10 Finished tutorial/solutions                                   16m10s   9GB
Feb 15 04:51:10 Starting translator/monadic/examples
Feb 15 04:54:28 Finished translator/monadic/examples                           3m17s   2GB
Feb 15 04:54:28 Starting examples
Feb 15 05:03:41 Finished examples                                              9m13s   4GB
Feb 15 05:03:41 Starting examples/compilation/x64
Feb 15 07:32:58 Finished examples/compilation/x64                           2h29m12s  18GB
Feb 15 07:32:58 Starting examples/compilation/x64/proofs
Feb 15 07:35:31 Finished examples/compilation/x64/proofs                       2m32s   3GB
Feb 15 07:35:31 Starting examples/compilation/ag32
Feb 15 08:10:16 Finished examples/compilation/ag32                            34m45s   9GB
Feb 15 08:10:16 Starting examples/compilation/ag32/proofs
Feb 15 08:11:10 Finished examples/compilation/ag32/proofs                        53s   2GB
Feb 15 08:11:11 Starting examples/cost
Feb 15 09:06:25 Finished examples/cost                                        55m13s  10GB
Feb 15 09:06:25 Starting examples/lpr_checker
Feb 15 09:07:20 Finished examples/lpr_checker                                    54s 756MB
Feb 15 09:07:20 Starting examples/lpr_checker/array
Feb 15 09:35:45 Finished examples/lpr_checker/array                           28m25s   7GB
Feb 15 09:35:45 Starting examples/lpr_checker/array/compilation
Feb 15 10:58:58 Finished examples/lpr_checker/array/compilation             1h23m11s  27GB
Feb 15 10:58:58 Starting examples/lpr_checker/array/compilation/proofs
Feb 15 11:00:24 Finished examples/lpr_checker/array/compilation/proofs         1m25s   6GB
Feb 15 11:00:24 Starting examples/opentheory
Feb 15 11:10:08 Finished examples/opentheory                                   9m44s   4GB
Feb 15 11:10:08 Starting examples/opentheory
Feb 15 11:10:09 Finished examples/opentheory                                      1s 130MB
Feb 15 11:10:10 Starting examples/opentheory/compilation
Feb 15 11:49:14 Finished examples/opentheory/compilation                      39m04s  27GB
Feb 15 11:49:14 Starting examples/opentheory/compilation/proofs
Feb 15 11:50:10 Finished examples/opentheory/compilation/proofs                  55s   4GB
Feb 15 11:50:10 Starting examples/opentheory/compilation/ag32
Feb 15 12:28:17 Finished examples/opentheory/compilation/ag32                 38m04s  30GB
Feb 15 12:28:19 Starting examples/opentheory/compilation/ag32/proofs
Feb 15 12:30:07 Finished examples/opentheory/compilation/ag32/proofs           1m47s   6GB
Feb 15 12:30:07 Starting examples/sat_encodings
Feb 15 12:32:07 Finished examples/sat_encodings                                2m00s 847MB
Feb 15 12:32:07 Starting examples/sat_encodings/case_studies
Feb 15 12:33:49 Finished examples/sat_encodings/case_studies                   1m41s 827MB
Feb 15 12:33:49 Starting examples/sat_encodings/translation
Feb 15 12:39:30 Finished examples/sat_encodings/translation                    5m40s   5GB
Feb 15 12:39:30 Starting examples/sat_encodings/translation/compilation
Feb 15 13:30:06 Finished examples/sat_encodings/translation/compilation       50m35s  24GB
Feb 15 13:30:06 Starting translator/okasaki-examples
Feb 15 13:34:41 Finished translator/okasaki-examples                           4m34s   2GB
Feb 15 13:34:41 Starting translator/other-examples
Feb 15 13:35:30 Finished translator/other-examples                               49s   1GB
Feb 15 13:35:30 Starting compiler/parsing/tests
Feb 15 13:36:00 Finished compiler/parsing/tests                                  29s 618MB
Feb 15 13:36:00 Starting compiler/inference/tests
Feb 15 13:44:17 Finished compiler/inference/tests                              8m16s   5GB
Feb 15 13:44:17 Starting compiler/bootstrap/translation
Feb 15 16:20:47 Finished compiler/bootstrap/translation                     2h36m27s  24GB
Feb 15 16:20:47 Starting unverified/sexpr-bootstrap/x64/64
Feb 15 16:31:10 Finished unverified/sexpr-bootstrap/x64/64                    10m21s   8GB
Feb 15 16:31:10 Starting unverified/sexpr-bootstrap/x64/32
Feb 15 16:39:59 Finished unverified/sexpr-bootstrap/x64/32                     8m48s   8GB
Feb 15 16:40:00 Starting compiler/benchmarks
Feb 15 16:40:56 Finished compiler/benchmarks                                     56s 673MB
Feb 15 16:40:56 Starting compiler/bootstrap/compilation/x64/64
Feb 16 05:51:40 Finished compiler/bootstrap/compilation/x64/64             13h10m39s  64GB
Feb 16 05:51:40 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 16 05:54:50 Finished compiler/bootstrap/compilation/x64/64/proofs          3m10s  18GB
Feb 16 05:54:51 Starting compiler/bootstrap/compilation/x64/32
Feb 16 17:00:57 Finished compiler/bootstrap/compilation/x64/32             11h06m04s  64GB
Feb 16 17:00:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 16 17:04:31 Finished compiler/bootstrap/compilation/x64/32/proofs          3m33s  13GB
Feb 16 17:04:31 Starting compiler/bootstrap/compilation/ag32/32
Feb 17 04:24:03 Finished compiler/bootstrap/compilation/ag32/32            11h19m31s  64GB
Feb 17 04:24:03 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 17 04:37:37 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m33s  26GB
Feb 17 04:37:37 SUCCESS