Job 1844

CakeML:82bbc7aaff75d6af713057a1095be95f322a08fd
  Merge pull request #870 from CakeML/itree-semantics [Apr 01 07:08:11]
HOL:9808526b233f88ea0a3b91583172af86bafc46ab
  Fix broken proofs after changing several extreal lemmas into [simp] [Mar 31 07:35:03]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 01 08:29:36 Claimed job
Apr 01 08:29:44 Building HOL
Apr 01 08:39:15 Starting developers
Apr 01 08:39:19 Finished developers                                               4s 122MB
Apr 01 08:39:19 Starting developers/bin
Apr 01 08:39:44 Finished developers/bin                                          24s   1GB
Apr 01 08:39:44 Starting semantics/ffi
Apr 01 08:39:53 Finished semantics/ffi                                            9s 245MB
Apr 01 08:39:54 Starting semantics
Apr 01 08:42:02 Finished semantics                                             2m08s   1GB
Apr 01 08:42:02 Starting semantics/proofs
Apr 01 08:46:09 Finished semantics/proofs                                      4m06s   4GB
Apr 01 08:46:09 Starting semantics/alt_semantics
Apr 01 08:46:35 Finished semantics/alt_semantics                                 25s 575MB
Apr 01 08:46:35 Starting semantics/alt_semantics/proofs
Apr 01 08:49:44 Finished semantics/alt_semantics/proofs                        3m08s   1GB
Apr 01 08:49:44 Starting basis/pure
Apr 01 08:52:55 Finished basis/pure                                            3m10s 922MB
Apr 01 08:52:55 Starting translator
Apr 01 08:55:55 Finished translator                                            2m59s   1GB
Apr 01 08:55:55 Starting compiler/parsing
Apr 01 08:57:09 Finished compiler/parsing                                      1m14s   2GB
Apr 01 08:57:09 Starting characteristic
Apr 01 09:03:38 Finished characteristic                                        6m28s   2GB
Apr 01 09:03:38 Starting translator/monadic
Apr 01 09:05:35 Finished translator/monadic                                    1m56s   1GB
Apr 01 09:05:35 Starting basis
Apr 01 09:53:08 Finished basis                                                47m31s  16GB
Apr 01 09:53:08 Starting compiler/inference
Apr 01 09:54:37 Finished compiler/inference                                    1m28s   1GB
Apr 01 09:54:37 Starting compiler/backend/reg_alloc
Apr 01 09:56:21 Finished compiler/backend/reg_alloc                            1m44s   1GB
Apr 01 09:56:21 Starting compiler/backend/gc
Apr 01 10:00:44 Finished compiler/backend/gc                                   4m22s   2GB
Apr 01 10:00:44 Starting compiler/backend
Apr 01 10:06:24 Finished compiler/backend                                      5m39s   2GB
Apr 01 10:06:25 Starting compiler/encoders/asm
Apr 01 10:06:54 Finished compiler/encoders/asm                                   29s 690MB
Apr 01 10:06:55 Starting compiler/encoders/x64
Apr 01 10:08:03 Finished compiler/encoders/x64                                 1m08s 995MB
Apr 01 10:08:03 Starting compiler/encoders/arm7
Apr 01 10:10:08 Finished compiler/encoders/arm7                                2m05s   1GB
Apr 01 10:10:08 Starting compiler/encoders/arm8
Apr 01 10:10:50 Finished compiler/encoders/arm8                                  41s   1GB
Apr 01 10:10:51 Starting compiler/encoders/arm8_asl
Apr 01 12:20:50 Finished compiler/encoders/arm8_asl                         2h09m56s  24GB
Apr 01 12:20:50 Starting compiler/encoders/mips
Apr 01 12:22:22 Finished compiler/encoders/mips                                1m32s   1GB
Apr 01 12:22:22 Starting compiler/encoders/riscv
Apr 01 12:24:11 Finished compiler/encoders/riscv                               1m48s   1GB
Apr 01 12:24:11 Starting compiler/encoders/ag32
Apr 01 12:24:33 Finished compiler/encoders/ag32                                  21s 699MB
Apr 01 12:24:33 Starting compiler/backend/x64
Apr 01 12:24:56 Finished compiler/backend/x64                                    22s   1GB
Apr 01 12:24:56 Starting compiler/backend/arm7
Apr 01 12:25:20 Finished compiler/backend/arm7                                   24s   1GB
Apr 01 12:25:20 Starting compiler/backend/arm8
Apr 01 12:25:42 Finished compiler/backend/arm8                                   21s   1GB
Apr 01 12:25:42 Starting compiler/backend/mips
Apr 01 12:26:05 Finished compiler/backend/mips                                   22s   1GB
Apr 01 12:26:05 Starting compiler/backend/riscv
Apr 01 12:26:29 Finished compiler/backend/riscv                                  23s   1GB
Apr 01 12:26:29 Starting compiler/backend/ag32
Apr 01 12:27:56 Finished compiler/backend/ag32                                 1m26s   1GB
Apr 01 12:27:56 Starting compiler/parsing/proofs
Apr 01 12:31:41 Finished compiler/parsing/proofs                               3m45s   1GB
Apr 01 12:31:41 Starting compiler/inference/proofs
Apr 01 12:34:13 Finished compiler/inference/proofs                             2m31s   1GB
Apr 01 12:34:13 Starting compiler/backend/semantics
Apr 01 13:03:18 Finished compiler/backend/semantics                           29m04s   2GB
Apr 01 13:03:18 Starting compiler/backend/reg_alloc/proofs
Apr 01 13:06:52 Finished compiler/backend/reg_alloc/proofs                     3m34s 751MB
Apr 01 13:06:52 Starting compiler/backend/proofs
Apr 01 13:57:57 Finished compiler/backend/proofs                              51m02s  16GB
Apr 01 13:57:59 Starting compiler/backend/serialiser
Apr 01 13:59:38 Finished compiler/backend/serialiser                           1m38s   2GB
Apr 01 13:59:38 Starting compiler/encoders/x64/proofs
Apr 01 14:09:13 Finished compiler/encoders/x64/proofs                          9m34s   5GB
Apr 01 14:09:13 Starting compiler/encoders/arm7/proofs
Apr 01 14:22:17 Finished compiler/encoders/arm7/proofs                        13m03s   4GB
Apr 01 14:22:17 Starting compiler/encoders/arm8/proofs
Apr 01 14:28:59 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Apr 01 14:28:59 Starting compiler/encoders/arm8_asl/proofs
Apr 01 15:18:47 Finished compiler/encoders/arm8_asl/proofs                    49m47s   6GB
Apr 01 15:18:47 Starting compiler/encoders/mips/proofs
Apr 01 15:28:50 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Apr 01 15:28:50 Starting compiler/encoders/riscv/proofs
Apr 01 15:37:30 Finished compiler/encoders/riscv/proofs                        8m39s   1GB
Apr 01 15:37:30 Starting compiler/encoders/ag32/proofs
Apr 01 15:40:04 Finished compiler/encoders/ag32/proofs                         2m34s 657MB
Apr 01 15:40:05 Starting compiler/backend/x64/proofs
Apr 01 15:40:32 Finished compiler/backend/x64/proofs                             27s   1GB
Apr 01 15:40:33 Starting compiler/backend/arm7/proofs
Apr 01 15:41:00 Finished compiler/backend/arm7/proofs                            27s   1GB
Apr 01 15:41:00 Starting compiler/backend/arm8/proofs
Apr 01 15:41:29 Finished compiler/backend/arm8/proofs                            28s   1GB
Apr 01 15:41:29 Starting compiler/backend/arm8_asl
Apr 01 15:41:52 Finished compiler/backend/arm8_asl                               23s   1GB
Apr 01 15:41:52 Starting compiler/backend/mips/proofs
Apr 01 15:42:22 Finished compiler/backend/mips/proofs                            29s   1GB
Apr 01 15:42:22 Starting compiler/backend/riscv/proofs
Apr 01 15:42:50 Finished compiler/backend/riscv/proofs                           27s   1GB
Apr 01 15:42:50 Starting compiler/backend/ag32/proofs
Apr 01 15:55:46 Finished compiler/backend/ag32/proofs                         12m55s   2GB
Apr 01 15:55:46 Starting compiler/proofs
Apr 01 15:58:12 Finished compiler/proofs                                       2m25s   3GB
Apr 01 15:58:12 Starting candle/set-theory
Apr 01 15:58:46 Finished candle/set-theory                                       33s 948MB
Apr 01 15:58:46 Starting candle/syntax-lib
Apr 01 15:59:00 Finished candle/syntax-lib                                       13s 639MB
Apr 01 15:59:00 Starting candle/standard/syntax
Apr 01 16:01:02 Finished candle/standard/syntax                                2m02s   1GB
Apr 01 16:01:03 Starting candle/standard/semantics
Apr 01 16:02:53 Finished candle/standard/semantics                             1m50s   2GB
Apr 01 16:02:54 Starting candle/standard/monadic
Apr 01 16:04:46 Finished candle/standard/monadic                               1m52s   1GB
Apr 01 16:04:46 Starting candle/standard/ml_kernel
Apr 01 16:10:52 Finished candle/standard/ml_kernel                             6m05s   3GB
Apr 01 16:10:52 Starting candle/overloading/syntax
Apr 01 16:14:04 Finished candle/overloading/syntax                             3m11s   1GB
Apr 01 16:14:04 Starting candle/overloading/semantics
Apr 01 16:25:50 Finished candle/overloading/semantics                         11m44s   2GB
Apr 01 16:25:50 Starting candle/overloading/monadic
Apr 01 16:28:23 Finished candle/overloading/monadic                            2m33s   1GB
Apr 01 16:28:23 Starting candle/overloading/ml_kernel
Apr 01 16:35:30 Finished candle/overloading/ml_kernel                          7m07s   3GB
Apr 01 16:35:31 Starting candle/overloading/ml_checker
Apr 01 16:38:03 Finished candle/overloading/ml_checker                         2m32s   2GB
Apr 01 16:38:04 Starting candle/prover
Apr 01 16:46:14 Finished candle/prover                                         8m10s   2GB
Apr 01 16:46:14 Starting pancake
Apr 01 16:49:57 Finished pancake                                               3m43s   3GB
Apr 01 16:49:58 Starting pancake/ffi
Apr 01 16:49:58 Finished pancake/ffi                                              0s  35MB
Apr 01 16:49:58 Starting pancake/semantics
Apr 01 16:52:27 Finished pancake/semantics                                     2m29s   1GB
Apr 01 16:52:27 Starting pancake/proofs
Apr 01 17:04:24 Finished pancake/proofs                                       11m56s   7GB
Apr 01 17:04:24 Starting characteristic/examples
Apr 01 17:05:47 Finished characteristic/examples                               1m22s   3GB
Apr 01 17:05:47 Starting tutorial/solutions
Apr 01 17:22:22 Finished tutorial/solutions                                   16m34s  12GB
Apr 01 17:22:22 Starting translator/monadic/examples
Apr 01 17:26:20 Finished translator/monadic/examples                           3m53s   2GB
Apr 01 17:26:20 Starting examples
Apr 01 17:35:42 Finished examples                                              9m22s   4GB
Apr 01 17:35:43 Starting examples/compilation/x64
Apr 01 20:06:05 Finished examples/compilation/x64                           2h30m20s  16GB
Apr 01 20:06:05 Starting examples/compilation/x64/proofs
Apr 01 20:08:16 Finished examples/compilation/x64/proofs                       2m10s   3GB
Apr 01 20:08:16 Starting examples/compilation/ag32
Apr 01 20:43:34 Finished examples/compilation/ag32                            35m17s   9GB
Apr 01 20:43:34 Starting examples/compilation/ag32/proofs
Apr 01 20:44:32 Finished examples/compilation/ag32/proofs                        57s   4GB
Apr 01 20:44:32 Starting examples/cost
Apr 01 21:40:28 Finished examples/cost                                        55m55s   9GB
Apr 01 21:40:28 Starting examples/lpr_checker
Apr 01 21:41:31 Finished examples/lpr_checker                                  1m02s   1GB
Apr 01 21:41:31 Starting examples/lpr_checker/array
Apr 01 22:10:02 Finished examples/lpr_checker/array                           28m30s   6GB
Apr 01 22:10:02 Starting examples/lpr_checker/array/compilation
Apr 01 23:34:45 Finished examples/lpr_checker/array/compilation             1h24m41s  29GB
Apr 01 23:34:45 Starting examples/lpr_checker/array/compilation/proofs
Apr 01 23:36:14 Finished examples/lpr_checker/array/compilation/proofs         1m29s   8GB
Apr 01 23:36:15 Starting examples/opentheory
Apr 01 23:46:14 Finished examples/opentheory                                   9m58s   5GB
Apr 01 23:46:14 Starting examples/opentheory
Apr 01 23:46:15 Finished examples/opentheory                                      1s 133MB
Apr 01 23:46:15 Starting examples/opentheory/compilation
Apr 02 00:26:34 Finished examples/opentheory/compilation                      40m18s  24GB
Apr 02 00:26:34 Starting examples/opentheory/compilation/proofs
Apr 02 00:27:29 Finished examples/opentheory/compilation/proofs                  54s   4GB
Apr 02 00:27:29 Starting examples/opentheory/compilation/ag32
Apr 02 01:05:20 Finished examples/opentheory/compilation/ag32                 37m49s  26GB
Apr 02 01:05:21 Starting examples/opentheory/compilation/ag32/proofs
Apr 02 01:07:07 Finished examples/opentheory/compilation/ag32/proofs           1m46s   7GB
Apr 02 01:07:07 Starting examples/sat_encodings
Apr 02 01:09:08 Finished examples/sat_encodings                                2m00s 738MB
Apr 02 01:09:08 Starting examples/sat_encodings/case_studies
Apr 02 01:10:50 Finished examples/sat_encodings/case_studies                   1m42s 759MB
Apr 02 01:10:50 Starting examples/sat_encodings/translation
Apr 02 01:16:43 Finished examples/sat_encodings/translation                    5m52s   3GB
Apr 02 01:16:43 Starting examples/sat_encodings/translation/compilation
Apr 02 02:06:23 Finished examples/sat_encodings/translation/compilation       49m36s  20GB
Apr 02 02:06:23 Starting translator/okasaki-examples
Apr 02 02:11:08 Finished translator/okasaki-examples                           4m44s   1GB
Apr 02 02:11:09 Starting translator/other-examples
Apr 02 02:13:05 Finished translator/other-examples                             1m55s   1GB
Apr 02 02:13:05 Starting compiler/parsing/tests
Apr 02 02:13:34 Finished compiler/parsing/tests                                  29s 663MB
Apr 02 02:13:34 Starting compiler/inference/tests
Apr 02 02:21:32 Finished compiler/inference/tests                              7m57s   6GB
Apr 02 02:21:32 Starting compiler/printing/test
Apr 02 02:25:09 Finished compiler/printing/test                                3m37s   3GB
Apr 02 02:25:10 Starting compiler/repl
Apr 02 02:37:41 Finished compiler/repl                                        12m31s   5GB
Apr 02 02:37:41 Starting compiler/bootstrap/translation
Apr 02 06:33:18 Finished compiler/bootstrap/translation                     3h55m35s  60GB
Apr 02 06:33:18 Starting unverified/sexpr-bootstrap/x64/64
Apr 02 06:44:45 Finished unverified/sexpr-bootstrap/x64/64                    11m26s  11GB
Apr 02 06:44:45 Starting unverified/sexpr-bootstrap/x64/32
Apr 02 06:54:05 Finished unverified/sexpr-bootstrap/x64/32                     9m18s  10GB
Apr 02 06:54:05 Starting compiler/benchmarks
Apr 02 06:55:00 Finished compiler/benchmarks                                     55s 674MB
Apr 02 06:55:01 Starting compiler/bootstrap/compilation/x64/64
Apr 03 03:09:30 Finished compiler/bootstrap/compilation/x64/64             20h14m27s  64GB
Apr 03 03:09:30 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 03 03:28:14 Finished compiler/bootstrap/compilation/x64/64/proofs         18m43s  38GB
Apr 03 03:28:14 Starting compiler/bootstrap/compilation/x64/32
Apr 03 16:26:48 Finished compiler/bootstrap/compilation/x64/32             12h58m30s  64GB
Apr 03 16:26:48 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 03 16:31:15 Finished compiler/bootstrap/compilation/x64/32/proofs          4m26s  16GB
Apr 03 16:31:15 Starting compiler/bootstrap/compilation/ag32/32
Apr 04 05:44:49 Finished compiler/bootstrap/compilation/ag32/32            13h13m32s  64GB
Apr 04 05:44:49 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 04 06:06:46 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m57s  29GB
Apr 04 06:06:46 SUCCESS