Job 2182

CakeML:de787171f1c2ef362fff6762e464a6496de600ed
  Fix for tap_config_enc' evaluation [Aug 07 21:21:17]
#965 (explorer)
Merging into:e6db84d62373636cd9788a3ebd3d245e4a58b720
  Fix errors caused by HOL deleting various quotient_*Theory [Jul 31 03:35:47]
HOL:7c8e22955100417422378e0bc5028d1e44abac81
  remove unicode [Aug 02 01:29:48]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Aug 07 21:43:07 Claimed job
Aug 07 21:43:15 Building HOL
Aug 07 21:56:51 Starting developers
Aug 07 21:56:56 Finished developers                                               5s 151MB
Aug 07 21:56:56 Starting developers/bin
Aug 07 21:57:02 Finished developers/bin                                           5s   1GB
Aug 07 21:57:02 Starting compiler/proofs
Aug 08 09:37:19 Resuming compiler/proofs
Aug 08 09:39:50 Finished compiler/proofs                                       2m30s   4GB
Aug 08 09:39:50 Starting compiler/bootstrap/translation
Aug 08 17:42:22 Finished compiler/bootstrap/translation                     8h02m29s  46GB
Aug 08 17:42:24 Starting semantics/ffi
Aug 08 17:42:29 Finished semantics/ffi                                            5s 213MB
Aug 08 17:42:29 Starting semantics
Aug 08 17:42:31 Finished semantics                                                1s  18MB
Aug 08 17:42:31 Starting semantics/proofs
Aug 08 17:43:03 Finished semantics/proofs                                        32s 726MB
Aug 08 17:43:04 Starting semantics/alt_semantics
Aug 08 17:43:35 Finished semantics/alt_semantics                                 31s 790MB
Aug 08 17:43:35 Starting semantics/alt_semantics/proofs
Aug 08 17:55:29 Finished semantics/alt_semantics/proofs                       11m53s   1GB
Aug 08 17:55:29 Starting basis/pure
Aug 08 17:55:30 Finished basis/pure                                               1s  21MB
Aug 08 17:55:30 Starting translator
Aug 08 17:57:20 Finished translator                                            1m49s   1GB
Aug 08 17:57:20 Starting compiler/parsing
Aug 08 17:57:22 Finished compiler/parsing                                         1s  20MB
Aug 08 17:57:22 Starting characteristic
Aug 08 17:57:24 Finished characteristic                                           1s  23MB
Aug 08 17:57:24 Starting translator/monadic
Aug 08 17:57:26 Finished translator/monadic                                       1s  26MB
Aug 08 17:57:26 Starting basis
Aug 08 18:01:28 Finished basis                                                 4m01s   3GB
Aug 08 18:01:28 Starting compiler/inference
Aug 08 18:01:30 Finished compiler/inference                                       1s  21MB
Aug 08 18:01:30 Starting compiler/backend/reg_alloc
Aug 08 18:01:32 Finished compiler/backend/reg_alloc                               1s  20MB
Aug 08 18:01:32 Starting compiler/backend/gc
Aug 08 18:01:34 Finished compiler/backend/gc                                      2s  21MB
Aug 08 18:01:34 Starting compiler/backend
Aug 08 18:01:46 Finished compiler/backend                                        11s 674MB
Aug 08 18:01:46 Starting compiler/encoders/asm
Aug 08 18:01:48 Finished compiler/encoders/asm                                    1s  24MB
Aug 08 18:01:48 Starting compiler/encoders/x64
Aug 08 18:01:50 Finished compiler/encoders/x64                                    1s  23MB
Aug 08 18:01:50 Starting compiler/encoders/arm7
Aug 08 18:01:52 Finished compiler/encoders/arm7                                   1s  19MB
Aug 08 18:01:52 Starting compiler/encoders/arm8
Aug 08 18:01:54 Finished compiler/encoders/arm8                                   1s  25MB
Aug 08 18:01:57 Starting compiler/encoders/arm8_asl
Aug 08 20:25:37 Finished compiler/encoders/arm8_asl                         2h23m37s  32GB
Aug 08 20:25:37 Starting compiler/encoders/mips
Aug 08 20:25:39 Finished compiler/encoders/mips                                   1s  20MB
Aug 08 20:25:39 Starting compiler/encoders/riscv
Aug 08 20:25:41 Finished compiler/encoders/riscv                                  1s  21MB
Aug 08 20:25:41 Starting compiler/encoders/ag32
Aug 08 20:25:43 Finished compiler/encoders/ag32                                   1s  21MB
Aug 08 20:25:43 Starting compiler/backend/x64
Aug 08 20:25:45 Finished compiler/backend/x64                                     2s  24MB
Aug 08 20:25:45 Starting compiler/backend/arm7
Aug 08 20:25:48 Finished compiler/backend/arm7                                    2s  24MB
Aug 08 20:25:48 Starting compiler/backend/arm8
Aug 08 20:25:50 Finished compiler/backend/arm8                                    2s  25MB
Aug 08 20:25:50 Starting compiler/backend/mips
Aug 08 20:25:52 Finished compiler/backend/mips                                    2s  23MB
Aug 08 20:25:52 Starting compiler/backend/riscv
Aug 08 20:25:55 Finished compiler/backend/riscv                                   2s  27MB
Aug 08 20:25:55 Starting compiler/backend/ag32
Aug 08 20:27:22 Finished compiler/backend/ag32                                 1m26s   1GB
Aug 08 20:27:22 Starting compiler/parsing/proofs
Aug 08 20:27:23 Finished compiler/parsing/proofs                                  1s  19MB
Aug 08 20:27:23 Starting compiler/inference/proofs
Aug 08 20:27:25 Finished compiler/inference/proofs                                1s  19MB
Aug 08 20:27:25 Starting compiler/backend/semantics
Aug 08 20:28:39 Finished compiler/backend/semantics                            1m13s   1GB
Aug 08 20:28:39 Starting compiler/backend/reg_alloc/proofs
Aug 08 20:28:41 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Aug 08 20:28:41 Starting compiler/backend/proofs
Aug 08 20:29:41 Finished compiler/backend/proofs                                 59s   2GB
Aug 08 20:29:41 Starting compiler/backend/serialiser
Aug 08 20:29:44 Finished compiler/backend/serialiser                              2s  29MB
Aug 08 20:29:44 Starting compiler/encoders/x64/proofs
Aug 08 20:39:32 Finished compiler/encoders/x64/proofs                          9m47s   5GB
Aug 08 20:39:32 Starting compiler/encoders/arm7/proofs
Aug 08 20:53:19 Finished compiler/encoders/arm7/proofs                        13m46s   3GB
Aug 08 20:53:19 Starting compiler/encoders/arm8/proofs
Aug 08 21:00:23 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Aug 08 21:00:23 Starting compiler/encoders/arm8_asl/proofs
Aug 08 21:52:51 Finished compiler/encoders/arm8_asl/proofs                    52m27s   5GB
Aug 08 21:52:51 Starting compiler/encoders/mips/proofs
Aug 08 22:03:35 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Aug 08 22:03:35 Starting compiler/encoders/riscv/proofs
Aug 08 22:12:32 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
Aug 08 22:12:32 Starting compiler/encoders/ag32/proofs
Aug 08 22:15:06 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Aug 08 22:15:06 Starting compiler/backend/x64/proofs
Aug 08 22:15:35 Finished compiler/backend/x64/proofs                             29s   1GB
Aug 08 22:15:36 Starting compiler/backend/arm7/proofs
Aug 08 22:16:09 Finished compiler/backend/arm7/proofs                            32s   2GB
Aug 08 22:16:09 Starting compiler/backend/arm8/proofs
Aug 08 22:16:43 Finished compiler/backend/arm8/proofs                            33s   1GB
Aug 08 22:16:43 Starting compiler/backend/arm8_asl
Aug 08 22:17:07 Finished compiler/backend/arm8_asl                               23s   1GB
Aug 08 22:17:07 Starting compiler/backend/mips/proofs
Aug 08 22:17:38 Finished compiler/backend/mips/proofs                            31s   2GB
Aug 08 22:17:38 Starting compiler/backend/riscv/proofs
Aug 08 22:18:12 Finished compiler/backend/riscv/proofs                           33s   2GB
Aug 08 22:18:12 Starting compiler/backend/ag32/proofs
Aug 08 22:32:01 Finished compiler/backend/ag32/proofs                         13m48s   2GB
Aug 08 22:32:01 Starting candle/set-theory
Aug 08 22:32:40 Finished candle/set-theory                                       38s 983MB
Aug 08 22:32:40 Starting candle/syntax-lib
Aug 08 22:32:41 Finished candle/syntax-lib                                        1s  20MB
Aug 08 22:32:42 Starting candle/standard/syntax
Aug 08 22:32:52 Finished candle/standard/syntax                                  10s 741MB
Aug 08 22:32:52 Starting candle/standard/semantics
Aug 08 22:34:49 Finished candle/standard/semantics                             1m56s   1GB
Aug 08 22:34:49 Starting candle/standard/monadic
Aug 08 22:34:51 Finished candle/standard/monadic                                  1s  19MB
Aug 08 22:34:52 Starting candle/standard/ml_kernel
Aug 08 22:36:33 Finished candle/standard/ml_kernel                             1m41s   3GB
Aug 08 22:36:33 Starting candle/overloading/syntax
Aug 08 22:39:57 Finished candle/overloading/syntax                             3m23s   1GB
Aug 08 22:39:57 Starting candle/overloading/semantics
Aug 08 22:52:16 Finished candle/overloading/semantics                         12m19s   3GB
Aug 08 22:52:16 Starting candle/overloading/monadic
Aug 08 22:55:05 Finished candle/overloading/monadic                            2m46s   1GB
Aug 08 22:55:05 Starting candle/overloading/ml_kernel
Aug 08 23:02:57 Finished candle/overloading/ml_kernel                          7m51s   3GB
Aug 08 23:02:57 Starting candle/overloading/ml_checker
Aug 08 23:05:30 Finished candle/overloading/ml_checker                         2m33s   2GB
Aug 08 23:05:30 Starting candle/prover
Aug 08 23:15:17 Finished candle/prover                                         9m47s   3GB
Aug 08 23:15:17 Starting pancake
Aug 08 23:16:03 Finished pancake                                                 45s 885MB
Aug 08 23:16:03 Starting pancake/ffi
Aug 08 23:16:03 Finished pancake/ffi                                              0s  13MB
Aug 08 23:16:03 Starting pancake/semantics
Aug 08 23:18:32 Finished pancake/semantics                                     2m28s   1GB
Aug 08 23:18:32 Starting pancake/parser
Aug 08 23:18:52 Finished pancake/parser                                          19s 633MB
Aug 08 23:18:52 Starting pancake/proofs
Aug 08 23:52:03 Finished pancake/proofs                                       33m11s   4GB
Aug 08 23:52:03 Starting characteristic/examples
Aug 08 23:53:33 Finished characteristic/examples                               1m29s   3GB
Aug 08 23:53:33 Starting tutorial/solutions
Aug 09 00:08:34 Finished tutorial/solutions                                   15m00s  10GB
Aug 09 00:08:35 Starting translator/monadic/examples
Aug 09 00:12:37 Finished translator/monadic/examples                           4m02s   3GB
Aug 09 00:12:37 Starting examples
Aug 09 00:28:39 Finished examples                                             16m01s   4GB
Aug 09 00:28:39 Starting examples/compilation/x64
Aug 09 02:27:59 Finished examples/compilation/x64                           1h59m17s  18GB
Aug 09 02:28:01 Starting examples/compilation/x64/proofs
Aug 09 02:30:36 Finished examples/compilation/x64/proofs                       2m35s   4GB
Aug 09 02:30:36 Starting examples/compilation/ag32
Aug 09 03:00:50 Finished examples/compilation/ag32                            30m13s   8GB
Aug 09 03:00:50 Starting examples/compilation/ag32/proofs
Aug 09 03:01:53 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Aug 09 03:01:53 Starting examples/compilation/to_word
Aug 09 03:05:16 Finished examples/compilation/to_word                          3m22s   5GB
Aug 09 03:05:16 Starting examples/lpr_checker
Aug 09 03:06:22 Finished examples/lpr_checker                                  1m06s   1GB
Aug 09 03:06:23 Starting examples/lpr_checker/array
Aug 09 03:43:27 Finished examples/lpr_checker/array                           37m03s   9GB
Aug 09 03:43:27 Starting examples/lpr_checker/array/compilation
Aug 09 04:23:26 Finished examples/lpr_checker/array/compilation               39m58s  25GB
Aug 09 04:23:26 Starting examples/lpr_checker/array/compilation/proofs
Aug 09 04:25:27 Finished examples/lpr_checker/array/compilation/proofs         2m00s   3GB
Aug 09 04:25:27 Starting examples/opentheory
Aug 09 04:36:28 Finished examples/opentheory                                  11m00s   3GB
Aug 09 04:36:28 Starting examples/opentheory
Aug 09 04:36:30 Finished examples/opentheory                                      1s  32MB
Aug 09 04:36:30 Starting examples/opentheory/compilation
Aug 09 05:13:40 Finished examples/opentheory/compilation                      37m08s  28GB
Aug 09 05:13:40 Starting examples/opentheory/compilation/proofs
Aug 09 05:14:45 Finished examples/opentheory/compilation/proofs                1m04s   4GB
Aug 09 05:14:45 Starting examples/opentheory/compilation/ag32
Aug 09 05:47:48 Finished examples/opentheory/compilation/ag32                 33m02s  30GB
Aug 09 05:47:48 Starting examples/opentheory/compilation/ag32/proofs
Aug 09 05:49:42 Finished examples/opentheory/compilation/ag32/proofs           1m53s   7GB
Aug 09 05:49:42 Starting examples/sat_encodings
Aug 09 05:51:45 Finished examples/sat_encodings                                2m02s   1GB
Aug 09 05:51:45 Starting examples/sat_encodings/case_studies
Aug 09 05:53:35 Finished examples/sat_encodings/case_studies                   1m49s   1GB
Aug 09 05:53:35 Starting examples/sat_encodings/translation
Aug 09 05:59:41 Finished examples/sat_encodings/translation                    6m05s   4GB
Aug 09 05:59:41 Starting examples/sat_encodings/translation/compilation
Aug 09 06:45:25 Finished examples/sat_encodings/translation/compilation       45m42s  23GB
Aug 09 06:45:25 Starting examples/deflate
Aug 09 06:46:26 Finished examples/deflate                                      1m00s   1GB
Aug 09 06:46:26 Starting examples/deflate/translation
Aug 09 06:48:09 Finished examples/deflate/translation                          1m42s   2GB
Aug 09 06:48:09 Starting examples/deflate/translation/compilation
Aug 09 07:08:17 Finished examples/deflate/translation/compilation             20m07s  14GB
Aug 09 07:08:17 Starting examples/vipr
Aug 09 07:12:22 Finished examples/vipr                                         4m05s   5GB
Aug 09 07:12:22 Starting examples/vipr/compilation
Aug 09 07:33:24 Finished examples/vipr/compilation                            21m01s  16GB
Aug 09 07:33:24 Starting translator/okasaki-examples
Aug 09 07:38:38 Finished translator/okasaki-examples                           5m14s   2GB
Aug 09 07:38:38 Starting translator/other-examples
Aug 09 07:41:21 Finished translator/other-examples                             2m42s   1GB
Aug 09 07:41:21 Starting compiler/parsing/tests
Aug 09 07:41:53 Finished compiler/parsing/tests                                  31s 767MB
Aug 09 07:41:53 Starting compiler/inference/tests
Aug 09 07:50:21 Finished compiler/inference/tests                              8m26s   5GB
Aug 09 07:50:21 Starting compiler/printing/test
Aug 09 07:54:17 Finished compiler/printing/test                                3m55s   3GB
Aug 09 07:54:17 Starting icing/flover
Aug 09 08:38:03 Finished icing/flover                                         43m45s   2GB
Aug 09 08:38:03 Starting icing/
Aug 09 09:33:31 Finished icing/                                               55m25s   7GB
Aug 09 09:33:31 Starting icing/examples
Aug 09 09:35:09 Finished icing/examples                                        1m38s   4GB
Aug 09 09:35:10 Starting compiler/repl
Aug 09 09:43:44 Finished compiler/repl                                         8m34s   5GB
Aug 09 09:43:44 Starting unverified/sexpr-bootstrap/x64/64
Aug 09 09:57:06 Finished unverified/sexpr-bootstrap/x64/64                    13m21s  16GB
Aug 09 09:57:06 Starting unverified/sexpr-bootstrap/x64/32
Aug 09 10:08:01 Finished unverified/sexpr-bootstrap/x64/32                    10m55s  13GB
Aug 09 10:08:01 Starting compiler/benchmarks
Aug 09 10:23:26 Finished compiler/benchmarks                                  15m24s   2GB
Aug 09 10:23:26 Starting compiler/bootstrap/compilation/x64/64
Aug 09 22:25:59 Finished compiler/bootstrap/compilation/x64/64             12h02m32s  64GB
Aug 09 22:25:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 09 22:46:19 Finished compiler/bootstrap/compilation/x64/64/proofs         20m19s  33GB
Aug 09 22:46:19 Starting compiler/bootstrap/compilation/x64/32
Aug 10 05:53:55 Finished compiler/bootstrap/compilation/x64/32              7h07m34s  64GB
Aug 10 05:53:55 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 10 05:56:58 Finished compiler/bootstrap/compilation/x64/32/proofs          3m03s  18GB
Aug 10 05:56:58 Starting compiler/bootstrap/compilation/ag32/32
Aug 10 13:16:29 Finished compiler/bootstrap/compilation/ag32/32             7h19m27s  64GB
Aug 10 13:16:30 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 10 13:25:46 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m15s  31GB
Aug 10 13:25:46 SUCCESS