Job 1770

CakeML:b6ce1417ef4a3913736824d1853fa54db032c681
  Merge branch 'master' into minor-reheapification [Jan 21 05:38:01]
#855 (minor-reheapification)
Merging into:2c76fd761b008577d98a968b7bbfee6e8c803477
  Fix a strange failure in translation [Feb 12 15:34:49]
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

Feb 12 15:45:30 Claimed job
Feb 12 15:45:31 Reusing HOL
Feb 12 15:45:45 Starting developers
Feb 12 15:45:49 Finished developers                                               4s 173MB
Feb 12 15:45:49 Starting developers/bin
Feb 12 15:45:53 Finished developers/bin                                           4s 674MB
Feb 12 15:45:54 Starting semantics/ffi
Feb 12 15:46:03 Finished semantics/ffi                                            9s 251MB
Feb 12 15:46:03 Starting semantics
Feb 12 15:47:43 Finished semantics                                             1m40s 912MB
Feb 12 15:47:44 Starting semantics/proofs
Feb 12 15:51:19 Finished semantics/proofs                                      3m35s   1GB
Feb 12 15:51:19 Starting semantics/alt_semantics
Feb 12 15:51:33 Finished semantics/alt_semantics                                 13s 391MB
Feb 12 15:51:33 Starting semantics/alt_semantics/proofs
Feb 12 15:54:01 Finished semantics/alt_semantics/proofs                        2m28s   1GB
Feb 12 15:54:01 Starting basis/pure
Feb 12 15:54:53 Finished basis/pure                                              51s 645MB
Feb 12 15:54:53 Starting translator
Feb 12 15:57:47 Finished translator                                            2m53s   1GB
Feb 12 15:57:47 Starting compiler/parsing
Feb 12 15:59:02 Finished compiler/parsing                                      1m14s   2GB
Feb 12 15:59:02 Starting characteristic
Feb 12 16:04:54 Finished characteristic                                        5m51s   1GB
Feb 12 16:04:54 Starting translator/monadic
Feb 12 16:06:38 Finished translator/monadic                                    1m44s   1GB
Feb 12 16:06:38 Starting basis
Feb 12 16:52:36 Finished basis                                                45m57s  16GB
Feb 12 16:52:36 Starting compiler/inference
Feb 12 16:53:45 Finished compiler/inference                                    1m08s   1GB
Feb 12 16:53:45 Starting compiler/backend/reg_alloc
Feb 12 16:54:53 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 12 16:54:53 Starting compiler/backend/gc
Feb 12 16:58:22 Finished compiler/backend/gc                                   3m28s   2GB
Feb 12 16:58:22 Starting compiler/backend
Feb 12 17:03:26 Finished compiler/backend                                      5m03s   2GB
Feb 12 17:03:26 Starting compiler/encoders/asm
Feb 12 17:03:50 Finished compiler/encoders/asm                                   23s 701MB
Feb 12 17:03:50 Starting compiler/encoders/x64
Feb 12 17:04:17 Finished compiler/encoders/x64                                   27s 791MB
Feb 12 17:04:17 Starting compiler/encoders/arm7
Feb 12 17:05:09 Finished compiler/encoders/arm7                                  51s 802MB
Feb 12 17:05:09 Starting compiler/encoders/arm8
Feb 12 17:05:23 Finished compiler/encoders/arm8                                  13s 942MB
Feb 12 17:05:23 Starting compiler/encoders/arm8_asl
Feb 12 17:07:56 Finished compiler/encoders/arm8_asl                            2m32s   1GB
Feb 12 17:07:56 Starting compiler/encoders/mips
Feb 12 17:08:14 Finished compiler/encoders/mips                                  18s   1GB
Feb 12 17:08:14 Starting compiler/encoders/riscv
Feb 12 17:08:30 Finished compiler/encoders/riscv                                 15s 753MB
Feb 12 17:08:30 Starting compiler/encoders/ag32
Feb 12 17:08:50 Finished compiler/encoders/ag32                                  19s 626MB
Feb 12 17:08:50 Starting compiler/backend/x64
Feb 12 17:09:11 Finished compiler/backend/x64                                    21s   1GB
Feb 12 17:09:11 Starting compiler/backend/arm7
Feb 12 17:09:34 Finished compiler/backend/arm7                                   23s   1GB
Feb 12 17:09:34 Starting compiler/backend/arm8
Feb 12 17:09:57 Finished compiler/backend/arm8                                   22s   1GB
Feb 12 17:09:57 Starting compiler/backend/mips
Feb 12 17:10:18 Finished compiler/backend/mips                                   21s   1GB
Feb 12 17:10:18 Starting compiler/backend/riscv
Feb 12 17:10:40 Finished compiler/backend/riscv                                  21s   1GB
Feb 12 17:10:40 Starting compiler/backend/ag32
Feb 12 17:11:49 Finished compiler/backend/ag32                                 1m09s   1GB
Feb 12 17:11:50 Starting compiler/parsing/proofs
Feb 12 17:15:34 Finished compiler/parsing/proofs                               3m44s   1GB
Feb 12 17:15:34 Starting compiler/inference/proofs
Feb 12 17:18:02 Finished compiler/inference/proofs                             2m27s 882MB
Feb 12 17:18:02 Starting compiler/backend/semantics
Feb 12 17:46:39 Finished compiler/backend/semantics                           28m36s   1GB
Feb 12 17:46:39 Starting compiler/backend/reg_alloc/proofs
Feb 12 17:50:06 Finished compiler/backend/reg_alloc/proofs                     3m27s 705MB
Feb 12 17:50:07 Starting compiler/backend/proofs
Feb 12 18:42:17 Finished compiler/backend/proofs                              52m07s  23GB
Feb 12 18:42:18 Starting compiler/backend/serialiser
Feb 12 18:43:44 Finished compiler/backend/serialiser                           1m26s   1GB
Feb 12 18:43:44 Starting compiler/encoders/x64/proofs
Feb 12 18:53:23 Finished compiler/encoders/x64/proofs                          9m38s   3GB
Feb 12 18:53:23 Starting compiler/encoders/arm7/proofs
Feb 12 19:06:34 Finished compiler/encoders/arm7/proofs                        13m11s   3GB
Feb 12 19:06:34 Starting compiler/encoders/arm8/proofs
Feb 12 19:13:16 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Feb 12 19:13:16 Starting compiler/encoders/arm8_asl/proofs
Feb 12 19:29:12 Finished compiler/encoders/arm8_asl/proofs                    15m56s   1GB
Feb 12 19:29:12 Starting compiler/encoders/mips/proofs
Feb 12 19:39:19 Finished compiler/encoders/mips/proofs                        10m07s   2GB
Feb 12 19:39:19 Starting compiler/encoders/riscv/proofs
Feb 12 19:48:08 Finished compiler/encoders/riscv/proofs                        8m46s   1GB
Feb 12 19:48:08 Starting compiler/encoders/ag32/proofs
Feb 12 19:50:41 Finished compiler/encoders/ag32/proofs                         2m33s 757MB
Feb 12 19:50:42 Starting compiler/backend/x64/proofs
Feb 12 19:51:08 Finished compiler/backend/x64/proofs                             26s   1GB
Feb 12 19:51:08 Starting compiler/backend/arm7/proofs
Feb 12 19:51:35 Finished compiler/backend/arm7/proofs                            27s   1GB
Feb 12 19:51:36 Starting compiler/backend/arm8/proofs
Feb 12 19:52:02 Finished compiler/backend/arm8/proofs                            26s   1GB
Feb 12 19:52:02 Starting compiler/backend/arm8_asl
Feb 12 19:52:24 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 12 19:52:25 Starting compiler/backend/mips/proofs
Feb 12 19:52:52 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 12 19:52:52 Starting compiler/backend/riscv/proofs
Feb 12 19:53:19 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 12 19:53:20 Starting compiler/backend/ag32/proofs
Feb 12 20:06:03 Finished compiler/backend/ag32/proofs                         12m43s   2GB
Feb 12 20:06:03 Starting compiler/proofs
Feb 12 20:07:57 Finished compiler/proofs                                       1m53s   3GB
Feb 12 20:07:57 Starting candle/set-theory
Feb 12 20:08:26 Finished candle/set-theory                                       28s 702MB
Feb 12 20:08:26 Starting candle/syntax-lib
Feb 12 20:08:37 Finished candle/syntax-lib                                       11s 483MB
Feb 12 20:08:37 Starting candle/standard/syntax
Feb 12 20:10:27 Finished candle/standard/syntax                                1m49s   1GB
Feb 12 20:10:27 Starting candle/standard/semantics
Feb 12 20:12:13 Finished candle/standard/semantics                             1m46s   1GB
Feb 12 20:12:13 Starting candle/standard/monadic
Feb 12 20:13:52 Finished candle/standard/monadic                               1m38s   1GB
Feb 12 20:13:52 Starting candle/standard/ml_kernel
Feb 12 20:20:42 Finished candle/standard/ml_kernel                             6m48s   3GB
Feb 12 20:20:42 Starting candle/overloading/syntax
Feb 12 20:23:50 Finished candle/overloading/syntax                             3m08s   1GB
Feb 12 20:23:50 Starting candle/overloading/semantics
Feb 12 20:35:41 Finished candle/overloading/semantics                         11m50s   2GB
Feb 12 20:35:41 Starting candle/overloading/monadic
Feb 12 20:37:57 Finished candle/overloading/monadic                            2m16s   1GB
Feb 12 20:37:57 Starting candle/overloading/ml_kernel
Feb 12 20:45:28 Finished candle/overloading/ml_kernel                          7m30s   4GB
Feb 12 20:45:28 Starting candle/overloading/ml_checker
Feb 12 20:47:51 Finished candle/overloading/ml_checker                         2m23s   3GB
Feb 12 20:47:52 Starting candle/prover
Feb 12 20:55:25 Finished candle/prover                                         7m32s   3GB
Feb 12 20:55:25 Starting pancake
Feb 12 20:58:08 Finished pancake                                               2m43s   2GB
Feb 12 20:58:08 Starting pancake/ffi
Feb 12 20:58:09 Finished pancake/ffi                                              0s  35MB
Feb 12 20:58:09 Starting pancake/semantics
Feb 12 21:00:37 Finished pancake/semantics                                     2m28s   1GB
Feb 12 21:00:37 Starting pancake/proofs
Feb 12 21:12:45 Finished pancake/proofs                                       12m07s   7GB
Feb 12 21:12:45 Starting characteristic/examples
Feb 12 21:14:09 Finished characteristic/examples                               1m23s   3GB
Feb 12 21:14:09 Starting tutorial/solutions
Feb 12 21:31:02 Finished tutorial/solutions                                   16m52s   9GB
Feb 12 21:31:02 Starting translator/monadic/examples
Feb 12 21:34:25 Finished translator/monadic/examples                           3m22s   2GB
Feb 12 21:34:25 Starting examples
Feb 12 21:43:32 Finished examples                                              9m07s   3GB
Feb 12 21:43:33 Starting examples/compilation/x64
Feb 13 00:11:32 Finished examples/compilation/x64                           2h27m58s  20GB
Feb 13 00:11:32 Starting examples/compilation/x64/proofs
Feb 13 00:13:45 Finished examples/compilation/x64/proofs                       2m12s   3GB
Feb 13 00:13:45 Starting examples/compilation/ag32
Feb 13 00:48:25 Finished examples/compilation/ag32                            34m39s   8GB
Feb 13 00:48:25 Starting examples/compilation/ag32/proofs
Feb 13 00:49:19 Finished examples/compilation/ag32/proofs                        53s   3GB
Feb 13 00:49:19 Starting examples/cost
Feb 13 01:44:57 Finished examples/cost                                        55m34s  10GB
Feb 13 01:44:57 Starting examples/lpr_checker
Feb 13 01:45:49 Finished examples/lpr_checker                                    52s 641MB
Feb 13 01:45:49 Starting examples/lpr_checker/array
Feb 13 02:13:57 Finished examples/lpr_checker/array                           28m07s   8GB
Feb 13 02:13:57 Starting examples/lpr_checker/array/compilation
Feb 13 03:40:10 Finished examples/lpr_checker/array/compilation             1h26m10s  34GB
Feb 13 03:40:10 Starting examples/lpr_checker/array/compilation/proofs
Feb 13 03:41:33 Finished examples/lpr_checker/array/compilation/proofs         1m22s   6GB
Feb 13 03:41:33 Starting examples/opentheory
Feb 13 03:51:15 Finished examples/opentheory                                   9m42s   3GB
Feb 13 03:51:16 Starting examples/opentheory
Feb 13 03:51:17 Finished examples/opentheory                                      1s 130MB
Feb 13 03:51:17 Starting examples/opentheory/compilation
Feb 13 04:30:35 Finished examples/opentheory/compilation                      39m18s  30GB
Feb 13 04:30:35 Starting examples/opentheory/compilation/proofs
Feb 13 04:31:38 Finished examples/opentheory/compilation/proofs                1m02s   3GB
Feb 13 04:31:38 Starting examples/opentheory/compilation/ag32
Feb 13 05:10:15 Finished examples/opentheory/compilation/ag32                 38m35s  30GB
Feb 13 05:10:15 Starting examples/opentheory/compilation/ag32/proofs
Feb 13 05:12:01 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
Feb 13 05:12:01 Starting examples/sat_encodings
Feb 13 05:14:02 Finished examples/sat_encodings                                2m00s 990MB
Feb 13 05:14:02 Starting examples/sat_encodings/case_studies
Feb 13 05:15:45 Finished examples/sat_encodings/case_studies                   1m42s 799MB
Feb 13 05:15:45 Starting examples/sat_encodings/translation
Feb 13 05:21:32 Finished examples/sat_encodings/translation                    5m47s   5GB
Feb 13 05:21:33 Starting examples/sat_encodings/translation/compilation
Feb 13 06:10:07 Finished examples/sat_encodings/translation/compilation       48m34s  23GB
Feb 13 06:10:07 Starting translator/okasaki-examples
Feb 13 06:14:50 Finished translator/okasaki-examples                           4m42s   1GB
Feb 13 06:14:51 Starting translator/other-examples
Feb 13 06:15:39 Finished translator/other-examples                               48s   1GB
Feb 13 06:15:39 Starting compiler/parsing/tests
Feb 13 06:16:09 Finished compiler/parsing/tests                                  29s 590MB
Feb 13 06:16:09 Starting compiler/inference/tests
Feb 13 06:24:20 Finished compiler/inference/tests                              8m11s   3GB
Feb 13 06:24:21 Starting compiler/bootstrap/translation
Feb 13 09:00:36 Finished compiler/bootstrap/translation                     2h36m12s  40GB
Feb 13 09:00:36 Starting unverified/sexpr-bootstrap/x64/64
Feb 13 09:10:57 Finished unverified/sexpr-bootstrap/x64/64                    10m20s   8GB
Feb 13 09:10:57 Starting unverified/sexpr-bootstrap/x64/32
Feb 13 09:19:46 Finished unverified/sexpr-bootstrap/x64/32                     8m49s   8GB
Feb 13 09:19:46 Starting compiler/benchmarks
Feb 13 09:20:42 Finished compiler/benchmarks                                     56s 674MB
Feb 13 09:20:42 Starting compiler/bootstrap/compilation/x64/64
Feb 13 22:19:21 Finished compiler/bootstrap/compilation/x64/64             12h58m37s  64GB
Feb 13 22:19:22 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 13 22:22:12 Finished compiler/bootstrap/compilation/x64/64/proofs          2m50s  24GB
Feb 13 22:22:12 Starting compiler/bootstrap/compilation/x64/32
Feb 14 09:30:01 Finished compiler/bootstrap/compilation/x64/32             11h07m47s  64GB
Feb 14 09:30:01 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 14 09:33:39 Finished compiler/bootstrap/compilation/x64/32/proofs          3m37s  13GB
Feb 14 09:33:39 Starting compiler/bootstrap/compilation/ag32/32
Feb 14 20:37:55 Finished compiler/bootstrap/compilation/ag32/32            11h04m14s  64GB
Feb 14 20:37:55 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 14 20:53:56 Finished compiler/bootstrap/compilation/ag32/32/proofs        16m00s  26GB
Feb 14 20:53:56 SUCCESS