Job 2131

CakeML:5e0612a6f93d34e570019c2a768cbd4736402abe
  Fix for change to finite_mapSyntax in HOL [May 25 02:29:21]
HOL:8a1c5607fb8c5be3be18fbe7a3653c704b0ea4da
  Manual: mention that LaTeX munging handles record types OK [May 23 05:56:07]
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

May 25 02:39:52 Claimed job
May 25 02:39:54 Reusing HOL
May 25 02:40:33 Starting developers
May 25 02:40:39 Finished developers                                               5s 138MB
May 25 02:40:39 Starting developers/bin
May 25 02:40:44 Finished developers/bin                                           5s   1GB
May 25 02:40:45 Starting compiler/proofs
May 25 04:30:41 Finished compiler/proofs                                    1h49m55s  19GB
May 25 04:30:41 Starting compiler/bootstrap/translation
May 25 12:25:17 Finished compiler/bootstrap/translation                     7h54m32s  38GB
May 25 12:25:17 Starting semantics/ffi
May 25 12:25:23 Finished semantics/ffi                                            5s 217MB
May 25 12:25:23 Starting semantics
May 25 12:25:25 Finished semantics                                                1s  18MB
May 25 12:25:25 Starting semantics/proofs
May 25 12:25:57 Finished semantics/proofs                                        32s 740MB
May 25 12:25:57 Starting semantics/alt_semantics
May 25 12:26:28 Finished semantics/alt_semantics                                 30s 813MB
May 25 12:26:28 Starting semantics/alt_semantics/proofs
May 25 12:38:16 Finished semantics/alt_semantics/proofs                       11m47s   1GB
May 25 12:38:16 Starting basis/pure
May 26 07:45:55 Resuming basis/pure
May 26 07:45:56 Finished basis/pure                                               1s  17MB
May 26 07:45:56 Starting translator
May 26 07:48:03 Finished translator                                            2m06s   1GB
May 26 07:48:03 Starting compiler/parsing
May 26 07:48:04 Finished compiler/parsing                                         1s  18MB
May 26 07:48:05 Starting characteristic
May 26 07:48:07 Finished characteristic                                           1s  24MB
May 26 07:48:07 Starting translator/monadic
May 26 07:48:09 Finished translator/monadic                                       1s  19MB
May 26 07:48:09 Starting basis
May 26 07:52:03 Finished basis                                                 3m54s   2GB
May 26 07:52:03 Starting compiler/inference
May 26 07:52:05 Finished compiler/inference                                       1s  19MB
May 26 07:52:05 Starting compiler/backend/reg_alloc
May 26 07:52:06 Finished compiler/backend/reg_alloc                               1s  17MB
May 26 07:52:07 Starting compiler/backend/gc
May 26 07:52:09 Finished compiler/backend/gc                                      2s  21MB
May 26 07:52:09 Starting compiler/backend
May 26 07:52:22 Finished compiler/backend                                        12s 843MB
May 26 07:52:22 Starting compiler/encoders/asm
May 26 07:52:23 Finished compiler/encoders/asm                                    1s  24MB
May 26 07:52:24 Starting compiler/encoders/x64
May 26 07:52:25 Finished compiler/encoders/x64                                    1s  24MB
May 26 07:52:25 Starting compiler/encoders/arm7
May 26 07:52:27 Finished compiler/encoders/arm7                                   1s  22MB
May 26 07:52:27 Starting compiler/encoders/arm8
May 26 07:52:29 Finished compiler/encoders/arm8                                   1s  23MB
May 26 07:52:29 Starting compiler/encoders/arm8_asl
May 26 10:25:21 Finished compiler/encoders/arm8_asl                         2h32m50s  43GB
May 26 10:25:21 Starting compiler/encoders/mips
May 26 10:25:23 Finished compiler/encoders/mips                                   1s  22MB
May 26 10:25:23 Starting compiler/encoders/riscv
May 26 10:25:25 Finished compiler/encoders/riscv                                  1s  20MB
May 26 10:25:25 Starting compiler/encoders/ag32
May 26 10:25:27 Finished compiler/encoders/ag32                                   1s  22MB
May 26 10:25:27 Starting compiler/backend/x64
May 26 10:25:29 Finished compiler/backend/x64                                     2s  23MB
May 26 10:25:29 Starting compiler/backend/arm7
May 26 10:25:31 Finished compiler/backend/arm7                                    2s  24MB
May 26 10:25:31 Starting compiler/backend/arm8
May 26 10:25:34 Finished compiler/backend/arm8                                    2s  22MB
May 26 10:25:34 Starting compiler/backend/mips
May 26 10:25:36 Finished compiler/backend/mips                                    2s  23MB
May 26 10:25:36 Starting compiler/backend/riscv
May 26 10:25:38 Finished compiler/backend/riscv                                   2s  22MB
May 26 10:25:39 Starting compiler/backend/ag32
May 26 10:27:07 Finished compiler/backend/ag32                                 1m27s   1GB
May 26 10:27:07 Starting compiler/parsing/proofs
May 26 10:27:08 Finished compiler/parsing/proofs                                  1s  19MB
May 26 10:27:08 Starting compiler/inference/proofs
May 26 10:27:10 Finished compiler/inference/proofs                                1s  20MB
May 26 10:27:10 Starting compiler/backend/semantics
May 26 10:28:24 Finished compiler/backend/semantics                            1m13s   1GB
May 26 10:28:24 Starting compiler/backend/reg_alloc/proofs
May 26 10:28:26 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
May 26 10:28:26 Starting compiler/backend/proofs
May 26 10:29:24 Finished compiler/backend/proofs                                 58s   3GB
May 26 10:29:24 Starting compiler/backend/serialiser
May 26 10:29:27 Finished compiler/backend/serialiser                              2s  34MB
May 26 10:29:27 Starting compiler/encoders/x64/proofs
May 26 10:39:15 Finished compiler/encoders/x64/proofs                          9m47s   6GB
May 26 10:39:15 Starting compiler/encoders/arm7/proofs
May 26 10:53:01 Finished compiler/encoders/arm7/proofs                        13m45s   4GB
May 26 10:53:01 Starting compiler/encoders/arm8/proofs
May 26 10:59:52 Finished compiler/encoders/arm8/proofs                         6m51s   1GB
May 26 10:59:52 Starting compiler/encoders/arm8_asl/proofs
May 26 11:52:14 Finished compiler/encoders/arm8_asl/proofs                    52m19s  10GB
May 26 11:52:14 Starting compiler/encoders/mips/proofs
May 26 12:02:56 Finished compiler/encoders/mips/proofs                        10m41s   2GB
May 26 12:02:56 Starting compiler/encoders/riscv/proofs
May 26 12:11:55 Finished compiler/encoders/riscv/proofs                        8m59s   2GB
May 26 12:11:56 Starting compiler/encoders/ag32/proofs
May 26 12:14:35 Finished compiler/encoders/ag32/proofs                         2m39s   1GB
May 26 12:14:35 Starting compiler/backend/x64/proofs
May 26 12:15:03 Finished compiler/backend/x64/proofs                             28s   1GB
May 26 12:15:03 Starting compiler/backend/arm7/proofs
May 26 12:15:37 Finished compiler/backend/arm7/proofs                            33s   1GB
May 26 12:15:37 Starting compiler/backend/arm8/proofs
May 26 12:16:07 Finished compiler/backend/arm8/proofs                            29s   1GB
May 26 12:16:07 Starting compiler/backend/arm8_asl
May 26 12:16:30 Finished compiler/backend/arm8_asl                               23s   1GB
May 26 12:16:30 Starting compiler/backend/mips/proofs
May 26 12:17:01 Finished compiler/backend/mips/proofs                            31s   1GB
May 26 12:17:02 Starting compiler/backend/riscv/proofs
May 26 12:17:35 Finished compiler/backend/riscv/proofs                           33s   2GB
May 26 12:17:35 Starting compiler/backend/ag32/proofs
May 26 12:31:19 Finished compiler/backend/ag32/proofs                         13m44s   2GB
May 26 12:31:19 Starting candle/set-theory
May 26 12:31:59 Finished candle/set-theory                                       40s   1GB
May 26 12:32:00 Starting candle/syntax-lib
May 26 12:32:01 Finished candle/syntax-lib                                        1s  22MB
May 26 12:32:01 Starting candle/standard/syntax
May 26 12:32:12 Finished candle/standard/syntax                                  10s 800MB
May 26 12:32:12 Starting candle/standard/semantics
May 26 12:34:10 Finished candle/standard/semantics                             1m57s   1GB
May 26 12:34:10 Starting candle/standard/monadic
May 26 12:34:12 Finished candle/standard/monadic                                  1s  21MB
May 26 12:34:12 Starting candle/standard/ml_kernel
May 26 12:35:47 Finished candle/standard/ml_kernel                             1m35s   3GB
May 26 12:35:47 Starting candle/overloading/syntax
May 26 12:39:08 Finished candle/overloading/syntax                             3m20s   1GB
May 26 12:39:08 Starting candle/overloading/semantics
May 26 12:51:24 Finished candle/overloading/semantics                         12m16s   2GB
May 26 12:51:25 Starting candle/overloading/monadic
May 26 12:54:08 Finished candle/overloading/monadic                            2m40s   1GB
May 26 12:54:09 Starting candle/overloading/ml_kernel
May 26 13:02:07 Finished candle/overloading/ml_kernel                          7m57s   3GB
May 26 13:02:07 Starting candle/overloading/ml_checker
May 26 13:04:43 Finished candle/overloading/ml_checker                         2m36s   2GB
May 26 13:04:43 Starting candle/prover
May 26 13:14:32 Finished candle/prover                                         9m48s   3GB
May 26 13:14:32 Starting pancake
May 26 13:15:15 Finished pancake                                                 43s   1GB
May 26 13:15:16 Starting pancake/ffi
May 26 13:15:16 Finished pancake/ffi                                              0s  13MB
May 26 13:15:16 Starting pancake/semantics
May 26 13:17:43 Finished pancake/semantics                                     2m26s   1GB
May 26 13:17:43 Starting pancake/proofs
May 26 13:32:49 Finished pancake/proofs                                       15m05s   4GB
May 26 13:32:49 Starting characteristic/examples
May 26 13:34:21 Finished characteristic/examples                               1m32s   2GB
May 26 13:34:21 Starting tutorial/solutions
May 26 13:49:42 Finished tutorial/solutions                                   15m20s   8GB
May 26 13:49:42 Starting translator/monadic/examples
May 26 13:53:47 Finished translator/monadic/examples                           4m04s   3GB
May 26 13:53:47 Starting examples
May 26 14:10:01 Finished examples                                             16m11s   5GB
May 26 14:10:01 Starting examples/compilation/x64
May 26 16:11:45 Finished examples/compilation/x64                           2h01m43s  14GB
May 26 16:11:46 Starting examples/compilation/x64/proofs
May 26 16:14:18 Finished examples/compilation/x64/proofs                       2m32s   4GB
May 26 16:14:18 Starting examples/compilation/ag32
May 26 16:44:48 Finished examples/compilation/ag32                            30m30s   7GB
May 26 16:44:49 Starting examples/compilation/ag32/proofs
May 26 16:45:51 Finished examples/compilation/ag32/proofs                      1m01s   5GB
May 26 16:45:51 Starting examples/compilation/to_word
May 26 16:49:16 Finished examples/compilation/to_word                          3m25s   6GB
May 26 16:49:16 Starting examples/lpr_checker
May 26 16:50:22 Finished examples/lpr_checker                                  1m04s   1GB
May 26 16:50:22 Starting examples/lpr_checker/array
May 26 17:27:19 Finished examples/lpr_checker/array                           36m55s   8GB
May 26 17:27:19 Starting examples/lpr_checker/array/compilation
May 26 18:07:44 Finished examples/lpr_checker/array/compilation               40m24s  22GB
May 26 18:07:44 Starting examples/lpr_checker/array/compilation/proofs
May 26 18:09:15 Finished examples/lpr_checker/array/compilation/proofs         1m31s   6GB
May 26 18:09:16 Starting examples/opentheory
May 26 18:20:18 Finished examples/opentheory                                  11m02s   4GB
May 26 18:20:19 Starting examples/opentheory
May 26 18:20:20 Finished examples/opentheory                                      1s  22MB
May 26 18:20:21 Starting examples/opentheory/compilation
May 26 18:56:56 Finished examples/opentheory/compilation                      36m34s  30GB
May 26 18:56:56 Starting examples/opentheory/compilation/proofs
May 26 18:57:58 Finished examples/opentheory/compilation/proofs                1m02s   5GB
May 26 18:57:58 Starting examples/opentheory/compilation/ag32
May 26 19:30:56 Finished examples/opentheory/compilation/ag32                 32m57s  27GB
May 26 19:30:56 Starting examples/opentheory/compilation/ag32/proofs
May 26 19:32:50 Finished examples/opentheory/compilation/ag32/proofs           1m53s   8GB
May 26 19:32:50 Starting examples/sat_encodings
May 26 19:34:52 Finished examples/sat_encodings                                2m01s 858MB
May 26 19:34:52 Starting examples/sat_encodings/case_studies
May 26 19:36:41 Finished examples/sat_encodings/case_studies                   1m49s 984MB
May 26 19:36:41 Starting examples/sat_encodings/translation
May 26 19:42:55 Finished examples/sat_encodings/translation                    6m13s   4GB
May 26 19:42:55 Starting examples/sat_encodings/translation/compilation
May 26 20:31:16 Finished examples/sat_encodings/translation/compilation       48m19s  21GB
May 26 20:31:16 Starting examples/deflate
May 26 20:32:15 Finished examples/deflate                                        59s 800MB
May 26 20:32:15 Starting examples/deflate/translation
May 26 20:33:55 Finished examples/deflate/translation                          1m39s   3GB
May 26 20:33:55 Starting examples/deflate/translation/compilation
May 26 20:53:53 Finished examples/deflate/translation/compilation             19m57s  14GB
May 26 20:53:53 Starting translator/okasaki-examples
May 26 20:59:04 Finished translator/okasaki-examples                           5m10s   2GB
May 26 20:59:04 Starting translator/other-examples
May 26 21:01:50 Finished translator/other-examples                             2m45s   1GB
May 26 21:01:50 Starting compiler/parsing/tests
May 26 21:02:22 Finished compiler/parsing/tests                                  32s 739MB
May 26 21:02:22 Starting compiler/inference/tests
May 26 21:10:44 Finished compiler/inference/tests                              8m21s   6GB
May 26 21:10:44 Starting compiler/printing/test
May 26 21:14:38 Finished compiler/printing/test                                3m53s   3GB
May 26 21:14:38 Starting icing/flover
May 26 21:58:01 Finished icing/flover                                         43m22s   2GB
May 26 21:58:01 Starting icing/
May 26 22:54:08 Finished icing/                                               56m07s   8GB
May 26 22:54:09 Starting icing/examples
May 26 22:55:44 Finished icing/examples                                        1m34s   4GB
May 26 22:55:44 Starting compiler/repl
May 26 23:04:31 Finished compiler/repl                                         8m46s   6GB
May 26 23:04:31 Starting unverified/sexpr-bootstrap/x64/64
May 26 23:17:46 Finished unverified/sexpr-bootstrap/x64/64                    13m11s  17GB
May 26 23:17:46 Starting unverified/sexpr-bootstrap/x64/32
May 26 23:28:28 Finished unverified/sexpr-bootstrap/x64/32                    10m39s  14GB
May 26 23:28:28 Starting compiler/benchmarks
May 26 23:43:48 Finished compiler/benchmarks                                  15m19s   2GB
May 26 23:43:48 Starting compiler/bootstrap/compilation/x64/64
May 27 11:55:07 Finished compiler/bootstrap/compilation/x64/64             12h11m16s  64GB
May 27 11:55:07 Starting compiler/bootstrap/compilation/x64/64/proofs
May 27 12:15:57 Finished compiler/bootstrap/compilation/x64/64/proofs         20m49s  39GB
May 27 12:15:57 Starting compiler/bootstrap/compilation/x64/32
May 27 19:12:37 Finished compiler/bootstrap/compilation/x64/32              6h56m38s  64GB
May 27 19:12:37 Starting compiler/bootstrap/compilation/x64/32/proofs
May 27 19:15:27 Finished compiler/bootstrap/compilation/x64/32/proofs          2m49s  19GB
May 27 19:15:27 Starting compiler/bootstrap/compilation/ag32/32
May 28 02:29:10 Finished compiler/bootstrap/compilation/ag32/32             7h13m42s  64GB
May 28 02:29:10 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 28 02:35:47 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m36s  24GB
May 28 02:35:48 SUCCESS