Job 2100

CakeML:360f94ee2844eca3537766800ba2de892a6824b4
  Fix file ending for panConcreteExamples [Feb 23 11:00:07]
#927 (translation_update)
Merging into:d7c29417e7a6c5bd1a3c00154a5159dbce3d6e2a
  Merge pull request #928 from CakeML/packing [Feb 10 07:12:04]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 23 20:55:26 Claimed job
Feb 23 20:55:28 Reusing HOL
Feb 23 20:56:09 Starting developers
Feb 23 20:56:14 Finished developers                                               5s  84MB
Feb 23 20:56:14 Starting developers/bin
Feb 23 20:56:20 Finished developers/bin                                           5s   1GB
Feb 23 20:56:20 Starting compiler/proofs
Feb 23 22:46:40 Finished compiler/proofs                                    1h50m18s  16GB
Feb 23 22:46:40 Starting compiler/bootstrap/translation
Feb 24 06:43:01 Finished compiler/bootstrap/translation                     7h56m19s  37GB
Feb 24 06:43:01 Starting semantics/ffi
Feb 24 06:43:06 Finished semantics/ffi                                            4s 428MB
Feb 24 06:43:06 Starting semantics
Feb 24 06:43:07 Finished semantics                                                1s  18MB
Feb 24 06:43:07 Starting semantics/proofs
Feb 24 06:43:40 Finished semantics/proofs                                        32s 731MB
Feb 24 06:43:40 Starting semantics/alt_semantics
Feb 24 06:44:10 Finished semantics/alt_semantics                                 30s 843MB
Feb 24 06:44:10 Starting semantics/alt_semantics/proofs
Feb 24 06:56:01 Finished semantics/alt_semantics/proofs                       11m50s   2GB
Feb 24 06:56:01 Starting basis/pure
Feb 24 06:56:02 Finished basis/pure                                               1s  23MB
Feb 24 06:56:03 Starting translator
Feb 24 06:57:52 Finished translator                                            1m49s   1GB
Feb 24 06:57:52 Starting compiler/parsing
Feb 24 06:57:54 Finished compiler/parsing                                         1s  21MB
Feb 24 06:57:54 Starting characteristic
Feb 24 06:57:56 Finished characteristic                                           1s  23MB
Feb 24 06:57:56 Starting translator/monadic
Feb 24 06:57:58 Finished translator/monadic                                       1s  24MB
Feb 24 06:57:58 Starting basis
Feb 24 07:01:56 Finished basis                                                 3m57s   3GB
Feb 24 07:01:56 Starting compiler/inference
Feb 24 07:01:58 Finished compiler/inference                                       1s  20MB
Feb 24 07:01:58 Starting compiler/backend/reg_alloc
Feb 24 07:01:59 Finished compiler/backend/reg_alloc                               1s  18MB
Feb 24 07:01:59 Starting compiler/backend/gc
Feb 24 07:02:02 Finished compiler/backend/gc                                      2s  23MB
Feb 24 07:02:02 Starting compiler/backend
Feb 24 07:02:14 Finished compiler/backend                                        12s 813MB
Feb 24 07:02:14 Starting compiler/encoders/asm
Feb 24 07:02:16 Finished compiler/encoders/asm                                    1s  25MB
Feb 24 07:02:16 Starting compiler/encoders/x64
Feb 24 07:02:18 Finished compiler/encoders/x64                                    1s  21MB
Feb 24 07:02:18 Starting compiler/encoders/arm7
Feb 24 07:02:20 Finished compiler/encoders/arm7                                   1s  28MB
Feb 24 07:02:20 Starting compiler/encoders/arm8
Feb 24 07:02:22 Finished compiler/encoders/arm8                                   1s  23MB
Feb 24 07:02:22 Starting compiler/encoders/arm8_asl
Feb 24 07:05:36 Finished compiler/encoders/arm8_asl                            3m13s   1GB
Feb 24 07:05:36 Starting compiler/encoders/mips
Feb 24 07:05:38 Finished compiler/encoders/mips                                   1s  20MB
Feb 24 07:05:38 Starting compiler/encoders/riscv
Feb 24 07:05:40 Finished compiler/encoders/riscv                                  1s  22MB
Feb 24 07:05:40 Starting compiler/encoders/ag32
Feb 24 07:05:42 Finished compiler/encoders/ag32                                   1s  19MB
Feb 24 07:05:42 Starting compiler/backend/x64
Feb 24 07:05:44 Finished compiler/backend/x64                                     2s  28MB
Feb 24 07:05:44 Starting compiler/backend/arm7
Feb 24 07:05:46 Finished compiler/backend/arm7                                    2s  29MB
Feb 24 07:05:46 Starting compiler/backend/arm8
Feb 24 07:05:49 Finished compiler/backend/arm8                                    2s  23MB
Feb 24 07:05:49 Starting compiler/backend/mips
Feb 24 07:05:51 Finished compiler/backend/mips                                    2s  28MB
Feb 24 07:05:51 Starting compiler/backend/riscv
Feb 24 07:05:53 Finished compiler/backend/riscv                                   2s  25MB
Feb 24 07:05:54 Starting compiler/backend/ag32
Feb 24 07:07:21 Finished compiler/backend/ag32                                 1m27s   1GB
Feb 24 07:07:21 Starting compiler/parsing/proofs
Feb 24 07:07:23 Finished compiler/parsing/proofs                                  1s  17MB
Feb 24 07:07:23 Starting compiler/inference/proofs
Feb 24 07:07:25 Finished compiler/inference/proofs                                1s  22MB
Feb 24 07:07:25 Starting compiler/backend/semantics
Feb 24 07:08:39 Finished compiler/backend/semantics                            1m14s   1GB
Feb 24 07:08:39 Starting compiler/backend/reg_alloc/proofs
Feb 24 07:08:41 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Feb 24 07:08:41 Starting compiler/backend/proofs
Feb 24 07:09:36 Finished compiler/backend/proofs                                 54s   2GB
Feb 24 07:09:36 Starting compiler/backend/serialiser
Feb 24 07:09:39 Finished compiler/backend/serialiser                              2s  30MB
Feb 24 07:09:39 Starting compiler/encoders/x64/proofs
Feb 24 07:19:26 Finished compiler/encoders/x64/proofs                          9m47s   6GB
Feb 24 07:19:26 Starting compiler/encoders/arm7/proofs
Feb 24 07:33:20 Finished compiler/encoders/arm7/proofs                        13m53s   3GB
Feb 24 07:33:20 Starting compiler/encoders/arm8/proofs
Feb 24 07:40:17 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Feb 24 07:40:17 Starting compiler/encoders/arm8_asl/proofs
Feb 24 07:56:17 Finished compiler/encoders/arm8_asl/proofs                    15m58s   2GB
Feb 24 07:56:17 Starting compiler/encoders/mips/proofs
Feb 24 08:07:11 Finished compiler/encoders/mips/proofs                        10m53s   2GB
Feb 24 08:07:11 Starting compiler/encoders/riscv/proofs
Feb 24 08:16:00 Finished compiler/encoders/riscv/proofs                        8m49s   2GB
Feb 24 08:16:01 Starting compiler/encoders/ag32/proofs
Feb 24 08:18:39 Finished compiler/encoders/ag32/proofs                         2m38s 955MB
Feb 24 08:18:39 Starting compiler/backend/x64/proofs
Feb 24 08:19:08 Finished compiler/backend/x64/proofs                             28s   1GB
Feb 24 08:19:08 Starting compiler/backend/arm7/proofs
Feb 24 08:19:41 Finished compiler/backend/arm7/proofs                            32s   2GB
Feb 24 08:19:41 Starting compiler/backend/arm8/proofs
Feb 24 08:20:10 Finished compiler/backend/arm8/proofs                            29s   1GB
Feb 24 08:20:11 Starting compiler/backend/arm8_asl
Feb 24 08:20:34 Finished compiler/backend/arm8_asl                               23s   1GB
Feb 24 08:20:34 Starting compiler/backend/mips/proofs
Feb 24 08:21:05 Finished compiler/backend/mips/proofs                            30s   1GB
Feb 24 08:21:05 Starting compiler/backend/riscv/proofs
Feb 24 08:21:39 Finished compiler/backend/riscv/proofs                           33s   2GB
Feb 24 08:21:39 Starting compiler/backend/ag32/proofs
Feb 24 08:35:24 Finished compiler/backend/ag32/proofs                         13m45s   2GB
Feb 24 08:35:24 Starting candle/set-theory
Feb 24 08:36:03 Finished candle/set-theory                                       38s   1GB
Feb 24 08:36:03 Starting candle/syntax-lib
Feb 24 08:36:04 Finished candle/syntax-lib                                        1s  24MB
Feb 24 08:36:05 Starting candle/standard/syntax
Feb 24 08:36:15 Finished candle/standard/syntax                                  10s 688MB
Feb 24 08:36:16 Starting candle/standard/semantics
Feb 24 08:38:12 Finished candle/standard/semantics                             1m56s   1GB
Feb 24 08:38:12 Starting candle/standard/monadic
Feb 24 08:38:14 Finished candle/standard/monadic                                  1s  26MB
Feb 24 08:38:14 Starting candle/standard/ml_kernel
Feb 24 08:39:52 Finished candle/standard/ml_kernel                             1m37s   3GB
Feb 24 08:39:52 Starting candle/overloading/syntax
Feb 24 08:43:14 Finished candle/overloading/syntax                             3m21s   1GB
Feb 24 08:43:14 Starting candle/overloading/semantics
Feb 24 08:55:14 Finished candle/overloading/semantics                         12m00s   4GB
Feb 24 08:55:15 Starting candle/overloading/monadic
Feb 24 08:57:57 Finished candle/overloading/monadic                            2m41s   1GB
Feb 24 08:57:57 Starting candle/overloading/ml_kernel
Feb 24 09:05:52 Finished candle/overloading/ml_kernel                          7m54s   3GB
Feb 24 09:05:52 Starting candle/overloading/ml_checker
Feb 24 09:08:23 Finished candle/overloading/ml_checker                         2m30s   4GB
Feb 24 09:08:23 Starting candle/prover
Feb 24 09:18:10 Finished candle/prover                                         9m46s   3GB
Feb 24 09:18:10 Starting pancake
Feb 24 09:18:54 Finished pancake                                                 44s 883MB
Feb 24 09:18:54 Starting pancake/ffi
Feb 24 09:18:55 Finished pancake/ffi                                              0s  13MB
Feb 24 09:18:55 Starting pancake/semantics
Feb 24 09:21:27 Finished pancake/semantics                                     2m31s   1GB
Feb 24 09:21:27 Starting pancake/proofs
Feb 24 09:25:35 Finished pancake/proofs                                        4m08s   1GB
Feb 24 09:25:35 Starting characteristic/examples
Feb 24 09:27:07 Finished characteristic/examples                               1m31s   4GB
Feb 24 09:27:07 Starting tutorial/solutions
Feb 24 09:42:16 Finished tutorial/solutions                                   15m09s  10GB
Feb 24 09:42:16 Starting translator/monadic/examples
Feb 24 09:46:16 Finished translator/monadic/examples                           3m59s   3GB
Feb 24 09:46:16 Starting examples
Feb 24 10:02:03 Finished examples                                             15m46s   5GB
Feb 24 10:02:04 Starting examples/compilation/x64
Feb 24 12:01:30 Finished examples/compilation/x64                           1h59m25s  17GB
Feb 24 12:01:30 Starting examples/compilation/x64/proofs
Feb 24 12:04:01 Finished examples/compilation/x64/proofs                       2m30s   4GB
Feb 24 12:04:01 Starting examples/compilation/ag32
Feb 24 12:34:34 Finished examples/compilation/ag32                            30m32s   7GB
Feb 24 12:34:34 Starting examples/compilation/ag32/proofs
Feb 24 12:35:37 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Feb 24 12:35:38 Starting examples/compilation/to_word
Feb 24 12:38:58 Finished examples/compilation/to_word                          3m20s   6GB
Feb 24 12:38:58 Starting examples/lpr_checker
Feb 24 12:40:03 Finished examples/lpr_checker                                  1m05s   2GB
Feb 24 12:40:03 Starting examples/lpr_checker/array
Feb 24 13:16:44 Finished examples/lpr_checker/array                           36m39s   5GB
Feb 24 13:16:44 Starting examples/lpr_checker/array/compilation
Feb 24 13:56:41 Finished examples/lpr_checker/array/compilation               39m56s  25GB
Feb 24 13:56:41 Starting examples/lpr_checker/array/compilation/proofs
Feb 24 13:58:14 Finished examples/lpr_checker/array/compilation/proofs         1m33s   7GB
Feb 24 13:58:14 Starting examples/opentheory
Feb 24 14:09:04 Finished examples/opentheory                                  10m49s   5GB
Feb 24 14:09:04 Starting examples/opentheory
Feb 24 14:09:06 Finished examples/opentheory                                      1s  27MB
Feb 24 14:09:06 Starting examples/opentheory/compilation
Feb 24 14:47:11 Finished examples/opentheory/compilation                      38m03s  31GB
Feb 24 14:47:11 Starting examples/opentheory/compilation/proofs
Feb 24 14:48:08 Finished examples/opentheory/compilation/proofs                  56s   4GB
Feb 24 14:48:08 Starting examples/opentheory/compilation/ag32
Feb 24 15:21:07 Finished examples/opentheory/compilation/ag32                 32m58s  28GB
Feb 24 15:21:07 Starting examples/opentheory/compilation/ag32/proofs
Feb 24 15:23:00 Finished examples/opentheory/compilation/ag32/proofs           1m53s   7GB
Feb 24 15:23:00 Starting examples/sat_encodings
Feb 24 15:25:00 Finished examples/sat_encodings                                1m59s 864MB
Feb 24 15:25:00 Starting examples/sat_encodings/case_studies
Feb 24 15:26:47 Finished examples/sat_encodings/case_studies                   1m46s 951MB
Feb 24 15:26:47 Starting examples/sat_encodings/translation
Feb 24 15:32:56 Finished examples/sat_encodings/translation                    6m08s   3GB
Feb 24 15:32:56 Starting examples/sat_encodings/translation/compilation
Feb 24 16:19:50 Finished examples/sat_encodings/translation/compilation       46m52s  20GB
Feb 24 16:19:50 Starting examples/deflate
Feb 24 16:20:50 Finished examples/deflate                                      1m00s   1GB
Feb 24 16:20:50 Starting examples/deflate/translation
Feb 24 16:22:32 Finished examples/deflate/translation                          1m41s   3GB
Feb 24 16:22:32 Starting examples/deflate/translation/compilation
Feb 24 16:42:01 Finished examples/deflate/translation/compilation             19m29s  12GB
Feb 24 16:42:02 Starting translator/okasaki-examples
Feb 24 16:47:11 Finished translator/okasaki-examples                           5m09s   2GB
Feb 24 16:47:11 Starting translator/other-examples
Feb 24 16:48:05 Finished translator/other-examples                               53s   1GB
Feb 24 16:48:05 Starting compiler/parsing/tests
Feb 24 16:48:37 Finished compiler/parsing/tests                                  31s 780MB
Feb 24 16:48:37 Starting compiler/inference/tests
Feb 24 16:57:13 Finished compiler/inference/tests                              8m35s   3GB
Feb 24 16:57:13 Starting compiler/printing/test
Feb 24 17:01:01 Finished compiler/printing/test                                3m47s   3GB
Feb 24 17:01:01 Starting icing/flover
Feb 24 17:43:24 Finished icing/flover                                         42m22s   2GB
Feb 24 17:43:24 Starting icing/
Feb 26 14:14:07 Resuming icing/