Job 1956

CakeML:4cba31259526004a87507ef2f43cc46a0ef0272d
  Merge remote-tracking branch 'origin/master' into gh859 [Jul 04 21:00:13]
#862 (gh859)
Merging into:939c98b120105252f0e1ee40b7fe9d6d0d028e12
  Fix proof broken by recent HOL change [Jul 06 08:39:40]
HOL:8b0248d705162f895cc7228fd638fe1c7d74b600
  Fix Unicode violation from 5184a58dae1 [Jul 04 06:34:10]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jul 06 08:53:58 Claimed job
Jul 06 08:54:02 Building HOL
Jul 06 09:05:11 Starting developers
Jul 06 09:05:16 Finished developers                                               4s 164MB
Jul 06 09:05:16 Starting developers/bin
Jul 06 09:05:22 Finished developers/bin                                           6s   1GB
Jul 06 09:05:22 Starting semantics/ffi
Jul 06 09:05:32 Finished semantics/ffi                                            9s 231MB
Jul 06 09:05:32 Starting semantics
Jul 06 09:08:10 Finished semantics                                             2m37s   1GB
Jul 06 09:08:10 Starting semantics/proofs
Jul 06 09:15:25 Finished semantics/proofs                                      7m15s   1GB
Jul 06 09:15:25 Starting semantics/alt_semantics
Jul 06 09:15:54 Finished semantics/alt_semantics                                 28s 530MB
Jul 06 09:15:55 Starting semantics/alt_semantics/proofs
Jul 06 09:27:42 Finished semantics/alt_semantics/proofs                       11m46s   1GB
Jul 06 09:27:42 Starting basis/pure
Jul 06 09:31:20 Finished basis/pure                                            3m37s   1GB
Jul 06 09:31:20 Starting translator
Jul 06 09:35:04 Finished translator                                            3m41s   2GB
Jul 06 09:35:04 Starting compiler/parsing
Jul 06 09:36:35 Finished compiler/parsing                                      1m31s   5GB
Jul 06 09:36:35 Starting characteristic
Jul 06 09:43:37 Finished characteristic                                        7m01s   2GB
Jul 06 09:43:37 Starting translator/monadic
Jul 06 09:45:42 Finished translator/monadic                                    2m05s   1GB
Jul 06 09:45:42 Starting basis
Jul 06 10:38:27 Finished basis                                                52m42s  14GB
Jul 06 10:38:27 Starting compiler/inference
Jul 06 10:40:07 Finished compiler/inference                                    1m39s   1GB
Jul 06 10:40:07 Starting compiler/backend/reg_alloc
Jul 06 10:41:52 Finished compiler/backend/reg_alloc                            1m45s   1GB
Jul 06 10:41:52 Starting compiler/backend/gc
Jul 06 10:46:27 Finished compiler/backend/gc                                   4m33s   2GB
Jul 06 10:46:27 Starting compiler/backend
Jul 06 10:52:43 Finished compiler/backend                                      6m16s   3GB
Jul 06 10:52:44 Starting compiler/encoders/asm
Jul 06 10:53:15 Finished compiler/encoders/asm                                   30s 704MB
Jul 06 10:53:15 Starting compiler/encoders/x64
Jul 06 10:54:24 Finished compiler/encoders/x64                                 1m08s 861MB
Jul 06 10:54:24 Starting compiler/encoders/arm7
Jul 06 10:56:30 Finished compiler/encoders/arm7                                2m05s   1GB
Jul 06 10:56:30 Starting compiler/encoders/arm8
Jul 06 10:57:13 Finished compiler/encoders/arm8                                  42s 791MB
Jul 06 10:57:13 Starting compiler/encoders/arm8_asl
Jul 06 13:17:00 Finished compiler/encoders/arm8_asl                         2h19m44s  32GB
Jul 06 13:17:01 Starting compiler/encoders/mips
Jul 06 13:18:34 Finished compiler/encoders/mips                                1m32s   1GB
Jul 06 13:18:34 Starting compiler/encoders/riscv
Jul 06 13:20:22 Finished compiler/encoders/riscv                               1m47s   1GB
Jul 06 13:20:22 Starting compiler/encoders/ag32
Jul 06 13:20:44 Finished compiler/encoders/ag32                                  21s   1GB
Jul 06 13:20:44 Starting compiler/backend/x64
Jul 06 13:21:07 Finished compiler/backend/x64                                    22s   1GB
Jul 06 13:21:07 Starting compiler/backend/arm7
Jul 06 13:21:33 Finished compiler/backend/arm7                                   25s   1GB
Jul 06 13:21:33 Starting compiler/backend/arm8
Jul 06 13:21:55 Finished compiler/backend/arm8                                   22s   1GB
Jul 06 13:21:55 Starting compiler/backend/mips
Jul 06 13:22:19 Finished compiler/backend/mips                                   23s   1GB
Jul 06 13:22:19 Starting compiler/backend/riscv
Jul 06 13:22:43 Finished compiler/backend/riscv                                  24s   1GB
Jul 06 13:22:44 Starting compiler/backend/ag32
Jul 06 13:24:11 Finished compiler/backend/ag32                                 1m26s   1GB
Jul 06 13:24:11 Starting compiler/parsing/proofs
Jul 06 13:27:57 Finished compiler/parsing/proofs                               3m46s   1GB
Jul 06 13:27:57 Starting compiler/inference/proofs
Jul 06 13:30:46 Finished compiler/inference/proofs                             2m48s   1GB
Jul 06 13:30:46 Starting compiler/backend/semantics
Jul 06 13:57:49 Finished compiler/backend/semantics                           27m03s   2GB
Jul 06 13:57:50 Starting compiler/backend/reg_alloc/proofs
Jul 06 14:01:33 Finished compiler/backend/reg_alloc/proofs                     3m42s   1GB
Jul 06 14:01:33 Starting compiler/backend/proofs
Jul 06 14:57:11 Finished compiler/backend/proofs                              55m35s  19GB
Jul 06 14:57:11 Starting compiler/backend/serialiser
Jul 06 14:58:56 Finished compiler/backend/serialiser                           1m44s   2GB
Jul 06 14:58:56 Starting compiler/encoders/x64/proofs
Jul 06 15:08:46 Finished compiler/encoders/x64/proofs                          9m50s   5GB
Jul 06 15:08:46 Starting compiler/encoders/arm7/proofs
Jul 06 15:22:22 Finished compiler/encoders/arm7/proofs                        13m35s   5GB
Jul 06 15:22:23 Starting compiler/encoders/arm8/proofs
Jul 06 15:29:26 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Jul 06 15:29:26 Starting compiler/encoders/arm8_asl/proofs
Jul 06 16:20:36 Finished compiler/encoders/arm8_asl/proofs                    51m09s   6GB
Jul 06 16:20:36 Starting compiler/encoders/mips/proofs
Jul 06 16:31:08 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Jul 06 16:31:09 Starting compiler/encoders/riscv/proofs
Jul 06 16:40:04 Finished compiler/encoders/riscv/proofs                        8m55s   1GB
Jul 06 16:40:04 Starting compiler/encoders/ag32/proofs
Jul 06 16:42:44 Finished compiler/encoders/ag32/proofs                         2m39s 657MB
Jul 06 16:42:44 Starting compiler/backend/x64/proofs
Jul 06 16:43:12 Finished compiler/backend/x64/proofs                             28s   1GB
Jul 06 16:43:13 Starting compiler/backend/arm7/proofs
Jul 06 16:43:43 Finished compiler/backend/arm7/proofs                            30s   1GB
Jul 06 16:43:43 Starting compiler/backend/arm8/proofs
Jul 06 16:44:13 Finished compiler/backend/arm8/proofs                            29s   1GB
Jul 06 16:44:13 Starting compiler/backend/arm8_asl
Jul 06 16:44:38 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 06 16:44:38 Starting compiler/backend/mips/proofs
Jul 06 16:45:05 Finished compiler/backend/mips/proofs                            27s   1GB
Jul 06 16:45:05 Starting compiler/backend/riscv/proofs
Jul 06 16:45:35 Finished compiler/backend/riscv/proofs                           29s   1GB
Jul 06 16:45:35 Starting compiler/backend/ag32/proofs
Jul 06 16:59:30 Finished compiler/backend/ag32/proofs                         13m55s   2GB
Jul 06 16:59:30 Starting compiler/proofs
Jul 06 17:01:59 Finished compiler/proofs                                       2m28s   3GB
Jul 06 17:01:59 Starting candle/set-theory
Jul 06 17:02:34 Finished candle/set-theory                                       34s 990MB
Jul 06 17:02:34 Starting candle/syntax-lib
Jul 06 17:02:47 Finished candle/syntax-lib                                       13s 748MB
Jul 06 17:02:47 Starting candle/standard/syntax
Jul 06 17:04:51 Finished candle/standard/syntax                                2m04s 986MB
Jul 06 17:04:52 Starting candle/standard/semantics
Jul 06 17:06:44 Finished candle/standard/semantics                             1m52s 932MB
Jul 06 17:06:44 Starting candle/standard/monadic
Jul 06 17:08:44 Finished candle/standard/monadic                               1m59s   1GB
Jul 06 17:08:44 Starting candle/standard/ml_kernel
Jul 06 17:15:36 Finished candle/standard/ml_kernel                             6m52s   3GB
Jul 06 17:15:37 Starting candle/overloading/syntax
Jul 06 17:18:52 Finished candle/overloading/syntax                             3m15s   1GB
Jul 06 17:18:52 Starting candle/overloading/semantics
Jul 06 17:30:59 Finished candle/overloading/semantics                         12m05s   3GB
Jul 06 17:30:59 Starting candle/overloading/monadic
Jul 06 17:33:39 Finished candle/overloading/monadic                            2m40s   1GB
Jul 06 17:33:40 Starting candle/overloading/ml_kernel
Jul 06 17:41:08 Finished candle/overloading/ml_kernel                          7m27s   3GB
Jul 06 17:41:08 Starting candle/overloading/ml_checker
Jul 06 17:43:35 Finished candle/overloading/ml_checker                         2m27s   3GB
Jul 06 17:43:36 Starting candle/prover
Jul 06 17:54:36 Finished candle/prover                                        11m00s   3GB
Jul 06 17:54:36 Starting pancake
Jul 06 17:58:34 Finished pancake                                               3m58s   4GB
Jul 06 17:58:35 Starting pancake/ffi
Jul 06 17:58:35 Finished pancake/ffi                                              0s  35MB
Jul 06 17:58:35 Starting pancake/semantics
Jul 06 18:01:10 Finished pancake/semantics                                     2m35s   1GB
Jul 06 18:01:10 Starting pancake/proofs
Jul 06 18:13:43 Finished pancake/proofs                                       12m32s   6GB
Jul 06 18:13:43 Starting characteristic/examples
Jul 06 18:15:12 Finished characteristic/examples                               1m28s   2GB
Jul 06 18:15:12 Starting tutorial/solutions
Jul 06 18:31:07 Finished tutorial/solutions                                   15m53s   9GB
Jul 06 18:31:07 Starting translator/monadic/examples
Jul 06 18:35:02 Finished translator/monadic/examples                           3m54s   2GB
Jul 06 18:35:03 Starting examples
Jul 06 18:45:13 Finished examples                                             10m09s   4GB
Jul 06 18:45:13 Starting examples/compilation/x64
Jul 06 20:47:57 Finished examples/compilation/x64                           2h02m42s  16GB
Jul 06 20:47:57 Starting examples/compilation/x64/proofs
Jul 06 20:50:30 Finished examples/compilation/x64/proofs                       2m32s   3GB
Jul 06 20:50:30 Starting examples/compilation/ag32
Jul 06 21:23:59 Finished examples/compilation/ag32                            33m29s   7GB
Jul 06 21:24:00 Starting examples/compilation/ag32/proofs
Jul 06 21:24:55 Finished examples/compilation/ag32/proofs                        55s   2GB
Jul 06 21:24:55 Starting examples/lpr_checker
Jul 06 21:25:58 Finished examples/lpr_checker                                  1m02s   1GB
Jul 06 21:25:58 Starting examples/lpr_checker/array
Jul 06 22:00:02 Finished examples/lpr_checker/array                           34m02s   7GB
Jul 06 22:00:02 Starting examples/lpr_checker/array/compilation
Jul 06 22:38:04 Finished examples/lpr_checker/array/compilation               38m01s  25GB
Jul 06 22:38:04 Starting examples/lpr_checker/array/compilation/proofs
Jul 06 22:39:28 Finished examples/lpr_checker/array/compilation/proofs         1m23s   5GB
Jul 06 22:39:28 Starting examples/opentheory
Jul 06 22:49:59 Finished examples/opentheory                                  10m31s   4GB
Jul 06 22:50:00 Starting examples/opentheory
Jul 06 22:50:01 Finished examples/opentheory                                      1s 145MB
Jul 06 22:50:01 Starting examples/opentheory/compilation
Jul 06 23:27:04 Finished examples/opentheory/compilation                      37m01s  24GB
Jul 06 23:27:04 Starting examples/opentheory/compilation/proofs
Jul 06 23:28:08 Finished examples/opentheory/compilation/proofs                1m04s   2GB
Jul 06 23:28:08 Starting examples/opentheory/compilation/ag32
Jul 07 00:02:38 Finished examples/opentheory/compilation/ag32                 34m29s  28GB
Jul 07 00:02:38 Starting examples/opentheory/compilation/ag32/proofs
Jul 07 00:04:27 Finished examples/opentheory/compilation/ag32/proofs           1m48s   6GB
Jul 07 00:04:27 Starting examples/sat_encodings
Jul 07 00:06:31 Finished examples/sat_encodings                                2m03s 846MB
Jul 07 00:06:31 Starting examples/sat_encodings/case_studies
Jul 07 00:08:14 Finished examples/sat_encodings/case_studies                   1m43s 971MB
Jul 07 00:08:15 Starting examples/sat_encodings/translation
Jul 07 00:14:12 Finished examples/sat_encodings/translation                    5m57s   3GB
Jul 07 00:14:12 Starting examples/sat_encodings/translation/compilation
Jul 07 01:00:53 Finished examples/sat_encodings/translation/compilation       46m40s  18GB
Jul 07 01:00:54 Starting examples/deflate
Jul 07 01:01:53 Finished examples/deflate                                        58s 776MB
Jul 07 01:01:53 Starting examples/deflate/translation
Jul 07 01:03:26 Finished examples/deflate/translation                          1m33s   3GB
Jul 07 01:03:26 Starting examples/deflate/translation/compilation
Jul 07 01:24:34 Finished examples/deflate/translation/compilation             21m07s  12GB
Jul 07 01:24:34 Starting translator/okasaki-examples
Jul 07 01:29:37 Finished translator/okasaki-examples                           5m02s   1GB
Jul 07 01:29:37 Starting translator/other-examples
Jul 07 01:31:55 Finished translator/other-examples                             2m18s   1GB
Jul 07 01:31:55 Starting compiler/parsing/tests
Jul 07 01:32:25 Finished compiler/parsing/tests                                  29s 596MB
Jul 07 01:32:25 Starting compiler/inference/tests
Jul 07 01:40:53 Finished compiler/inference/tests                              8m28s   4GB
Jul 07 01:40:53 Starting compiler/printing/test
Jul 07 01:44:43 Finished compiler/printing/test                                3m49s   3GB
Jul 07 01:44:43 Starting icing/flover
Jul 07 02:28:58 Finished icing/flover                                         44m11s   1GB
Jul 07 02:28:58 Starting icing/
Jul 07 03:28:28 Finished icing/                                               59m29s   8GB
Jul 07 03:28:28 Starting icing/examples
Jul 07 03:30:09 Finished icing/examples                                        1m37s   3GB
Jul 07 03:30:09 Starting compiler/repl
Jul 07 03:43:33 Finished compiler/repl                                        13m24s   5GB
Jul 07 03:43:33 Starting compiler/bootstrap/translation
Jul 07 08:03:18 Finished compiler/bootstrap/translation                     4h19m43s  41GB
Jul 07 08:03:18 Starting unverified/sexpr-bootstrap/x64/64
Jul 07 08:15:34 Finished unverified/sexpr-bootstrap/x64/64                    12m15s   8GB
Jul 07 08:15:34 Starting unverified/sexpr-bootstrap/x64/32
Jul 07 08:25:14 Finished unverified/sexpr-bootstrap/x64/32                     9m40s  10GB
Jul 07 08:25:15 Starting compiler/benchmarks
Jul 07 08:26:10 Finished compiler/benchmarks                                     55s 673MB
Jul 07 08:26:11 Starting compiler/bootstrap/compilation/x64/64
Jul 07 19:14:25 Finished compiler/bootstrap/compilation/x64/64             10h48m11s  64GB
Jul 07 19:14:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 07 19:31:58 Finished compiler/bootstrap/compilation/x64/64/proofs         17m32s  24GB
Jul 07 19:31:58 Starting compiler/bootstrap/compilation/x64/32
Jul 08 01:53:26 Finished compiler/bootstrap/compilation/x64/32              6h21m26s  64GB
Jul 08 01:53:26 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 08 01:56:31 Finished compiler/bootstrap/compilation/x64/32/proofs          3m05s  14GB
Jul 08 01:56:31 Starting compiler/bootstrap/compilation/ag32/32
Jul 08 08:26:38 Finished compiler/bootstrap/compilation/ag32/32             6h30m05s  64GB
Jul 08 08:26:39 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 08 08:32:39 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m59s  41GB
Jul 08 08:32:39 SUCCESS