Job 2200

CakeML:6ff7f36f3d121f06266c2280d68bf9e2dd52a6de
  Update perms_ok proofs [Aug 17 19:40:01]
#969 (issue-916)
Merging into:5696cf2a85f55b22b92cbb2810d120e9259e144e
  Merge pull request #967 from CakeML/lpr_arm8 [Aug 21 07:03:02]
HOL:1b35c0108cfd82d6f6a4960cfe747ff4e5cf3ee5
  Initial work on making triangular unification tail-recursive [Aug 18 07:44:40]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Aug 22 17:46:59 Claimed job
Aug 22 17:47:07 Building HOL
Aug 22 18:00:47 Starting developers
Aug 22 18:00:52 Finished developers                                               5s 131MB
Aug 22 18:00:52 Starting developers/bin
Aug 22 18:00:58 Finished developers/bin                                           6s   1GB
Aug 22 18:00:59 Starting compiler/proofs
Aug 22 19:54:21 Finished compiler/proofs                                    1h53m20s  17GB
Aug 22 19:54:22 Starting compiler/bootstrap/translation
Aug 23 03:59:55 Finished compiler/bootstrap/translation                     8h05m30s  40GB
Aug 23 03:59:55 Starting semantics/ffi
Aug 23 04:00:00 Finished semantics/ffi                                            4s 382MB
Aug 23 04:00:00 Starting semantics
Aug 23 04:00:01 Finished semantics                                                1s  18MB
Aug 23 04:00:01 Starting semantics/proofs
Aug 23 04:00:35 Finished semantics/proofs                                        33s   1GB
Aug 23 04:00:35 Starting semantics/alt_semantics
Aug 23 04:01:06 Finished semantics/alt_semantics                                 31s 758MB
Aug 23 04:01:06 Starting semantics/alt_semantics/proofs
Aug 23 04:13:04 Finished semantics/alt_semantics/proofs                       11m57s   1GB
Aug 23 04:13:04 Starting basis/pure
Aug 23 04:13:05 Finished basis/pure                                               1s  23MB
Aug 23 04:13:06 Starting translator
Aug 23 04:14:51 Finished translator                                            1m44s   2GB
Aug 23 04:14:51 Starting compiler/parsing
Aug 23 04:14:52 Finished compiler/parsing                                         1s  24MB
Aug 23 04:14:52 Starting characteristic
Aug 23 04:14:54 Finished characteristic                                           1s  21MB
Aug 23 04:14:55 Starting translator/monadic
Aug 23 04:14:57 Finished translator/monadic                                       1s  21MB
Aug 23 04:14:57 Starting basis
Aug 23 04:19:02 Finished basis                                                 4m04s   3GB
Aug 23 04:19:02 Starting compiler/inference
Aug 23 04:19:04 Finished compiler/inference                                       1s  17MB
Aug 23 04:19:04 Starting compiler/backend/reg_alloc
Aug 23 04:19:05 Finished compiler/backend/reg_alloc                               1s  21MB
Aug 23 04:19:05 Starting compiler/backend/gc
Aug 23 04:19:08 Finished compiler/backend/gc                                      2s  30MB
Aug 23 04:19:08 Starting compiler/backend
Aug 23 04:19:20 Finished compiler/backend                                        12s 831MB
Aug 23 04:19:20 Starting compiler/encoders/asm
Aug 23 04:19:22 Finished compiler/encoders/asm                                    1s  22MB
Aug 23 04:19:22 Starting compiler/encoders/x64
Aug 23 04:19:24 Finished compiler/encoders/x64                                    1s  23MB
Aug 23 04:19:24 Starting compiler/encoders/arm7
Aug 23 04:19:26 Finished compiler/encoders/arm7                                   1s  25MB
Aug 23 04:19:26 Starting compiler/encoders/arm8
Aug 23 04:19:28 Finished compiler/encoders/arm8                                   1s  22MB
Aug 23 04:19:28 Starting compiler/encoders/arm8_asl
Aug 23 06:48:45 Finished compiler/encoders/arm8_asl                         2h29m16s  38GB
Aug 23 06:48:45 Starting compiler/encoders/mips
Aug 23 06:48:47 Finished compiler/encoders/mips                                   1s  21MB
Aug 23 06:48:47 Starting compiler/encoders/riscv
Aug 23 06:48:49 Finished compiler/encoders/riscv                                  1s  25MB
Aug 23 06:48:49 Starting compiler/encoders/ag32
Aug 23 06:48:51 Finished compiler/encoders/ag32                                   1s  21MB
Aug 23 06:48:51 Starting compiler/backend/x64
Aug 23 06:48:53 Finished compiler/backend/x64                                     2s  29MB
Aug 23 06:48:53 Starting compiler/backend/arm7
Aug 23 06:48:56 Finished compiler/backend/arm7                                    2s  25MB
Aug 23 06:48:56 Starting compiler/backend/arm8
Aug 23 06:48:58 Finished compiler/backend/arm8                                    2s  26MB
Aug 23 06:48:58 Starting compiler/backend/mips
Aug 23 06:49:00 Finished compiler/backend/mips                                    2s  21MB
Aug 23 06:49:00 Starting compiler/backend/riscv
Aug 23 06:49:03 Finished compiler/backend/riscv                                   2s  31MB
Aug 23 06:49:03 Starting compiler/backend/ag32
Aug 23 06:50:30 Finished compiler/backend/ag32                                 1m26s   1GB
Aug 23 06:50:30 Starting compiler/parsing/proofs
Aug 23 06:50:32 Finished compiler/parsing/proofs                                  1s  20MB
Aug 23 06:50:32 Starting compiler/inference/proofs
Aug 23 06:50:34 Finished compiler/inference/proofs                                1s  18MB
Aug 23 06:50:34 Starting compiler/backend/semantics
Aug 23 06:51:47 Finished compiler/backend/semantics                            1m13s   1GB
Aug 23 06:51:47 Starting compiler/backend/reg_alloc/proofs
Aug 23 06:51:49 Finished compiler/backend/reg_alloc/proofs                        1s  28MB
Aug 23 06:51:50 Starting compiler/backend/proofs
Aug 23 06:52:45 Finished compiler/backend/proofs                                 55s   2GB
Aug 23 06:52:45 Starting compiler/backend/serialiser
Aug 23 06:52:48 Finished compiler/backend/serialiser                              2s  33MB
Aug 23 06:52:48 Starting compiler/encoders/x64/proofs
Aug 23 07:02:35 Finished compiler/encoders/x64/proofs                          9m46s   7GB
Aug 23 07:02:35 Starting compiler/encoders/arm7/proofs
Aug 23 07:16:13 Finished compiler/encoders/arm7/proofs                        13m38s   3GB
Aug 23 07:16:13 Starting compiler/encoders/arm8/proofs
Aug 23 07:23:01 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
Aug 23 07:23:01 Starting compiler/encoders/arm8_asl/proofs
Aug 23 08:16:50 Finished compiler/encoders/arm8_asl/proofs                    53m45s   8GB
Aug 23 08:16:50 Starting compiler/encoders/mips/proofs
Aug 23 08:27:39 Finished compiler/encoders/mips/proofs                        10m48s   2GB
Aug 23 08:27:39 Starting compiler/encoders/riscv/proofs
Aug 23 08:36:30 Finished compiler/encoders/riscv/proofs                        8m50s   1GB
Aug 23 08:36:30 Starting compiler/encoders/ag32/proofs
Aug 23 08:39:05 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Aug 23 08:39:05 Starting compiler/backend/x64/proofs
Aug 23 08:39:35 Finished compiler/backend/x64/proofs                             29s   1GB
Aug 23 08:39:35 Starting compiler/backend/arm7/proofs
Aug 23 08:40:09 Finished compiler/backend/arm7/proofs                            33s   2GB
Aug 23 08:40:09 Starting compiler/backend/arm8/proofs
Aug 23 08:40:39 Finished compiler/backend/arm8/proofs                            29s   1GB
Aug 23 08:40:39 Starting compiler/backend/arm8_asl
Aug 23 08:41:02 Finished compiler/backend/arm8_asl                               22s   1GB
Aug 23 08:41:02 Starting compiler/backend/mips/proofs
Aug 23 08:41:34 Finished compiler/backend/mips/proofs                            32s   2GB
Aug 23 08:41:35 Starting compiler/backend/riscv/proofs
Aug 23 08:42:09 Finished compiler/backend/riscv/proofs                           34s   2GB
Aug 23 08:42:09 Starting compiler/backend/ag32/proofs
Aug 23 08:55:47 Finished compiler/backend/ag32/proofs                         13m38s   3GB
Aug 23 08:55:47 Starting candle/set-theory
Aug 23 08:56:26 Finished candle/set-theory                                       38s 958MB
Aug 23 08:56:26 Starting candle/syntax-lib
Aug 23 08:56:28 Finished candle/syntax-lib                                        1s  19MB
Aug 23 08:56:28 Starting candle/standard/syntax
Aug 23 08:56:38 Finished candle/standard/syntax                                  10s 866MB
Aug 23 08:56:39 Starting candle/standard/semantics
Aug 23 08:58:36 Finished candle/standard/semantics                             1m57s   1GB
Aug 23 08:58:36 Starting candle/standard/monadic
Aug 23 08:58:38 Finished candle/standard/monadic                                  1s  23MB
Aug 23 08:58:38 Starting candle/standard/ml_kernel
Aug 23 09:00:14 Finished candle/standard/ml_kernel                             1m35s   3GB
Aug 23 09:00:14 Starting candle/overloading/syntax
Aug 23 09:03:35 Finished candle/overloading/syntax                             3m21s   1GB
Aug 23 09:03:35 Starting candle/overloading/semantics
Aug 23 09:16:02 Finished candle/overloading/semantics                         12m26s   2GB
Aug 23 09:16:02 Starting candle/overloading/monadic
Aug 23 09:18:48 Finished candle/overloading/monadic                            2m45s   1GB
Aug 23 09:18:49 Starting candle/overloading/ml_kernel
Aug 23 09:26:49 Finished candle/overloading/ml_kernel                          8m00s   3GB
Aug 23 09:26:49 Starting candle/overloading/ml_checker
Aug 23 09:29:24 Finished candle/overloading/ml_checker                         2m34s   2GB
Aug 23 09:29:24 Starting candle/prover
Aug 23 09:39:21 Finished candle/prover                                         9m56s   3GB
Aug 23 09:39:21 Starting pancake
Aug 23 09:40:05 Finished pancake                                                 44s   1GB
Aug 23 09:40:05 Starting pancake/ffi
Aug 23 09:40:05 Finished pancake/ffi                                              0s  13MB
Aug 23 09:40:06 Starting pancake/semantics
Aug 23 09:42:33 Finished pancake/semantics                                     2m27s   1GB
Aug 23 09:42:33 Starting pancake/parser
Aug 23 09:42:52 Finished pancake/parser                                          18s 812MB
Aug 23 09:42:52 Starting pancake/proofs
Aug 23 10:16:14 Finished pancake/proofs                                       33m21s   6GB
Aug 23 10:16:14 Starting characteristic/examples
Aug 23 10:17:46 Finished characteristic/examples                               1m31s   2GB
Aug 23 10:17:46 Starting tutorial/solutions
Aug 23 10:33:07 Finished tutorial/solutions                                   15m17s  10GB
Aug 23 10:33:08 Starting translator/monadic/examples
Aug 23 10:37:14 Finished translator/monadic/examples                           4m05s   3GB
Aug 23 10:37:14 Starting examples
Aug 23 10:53:25 Finished examples                                             16m10s   5GB
Aug 23 10:53:25 Starting examples/compilation/x64
Aug 23 12:52:27 Finished examples/compilation/x64                           1h59m01s  15GB
Aug 23 12:52:28 Starting examples/compilation/x64/proofs
Aug 23 12:55:01 Finished examples/compilation/x64/proofs                       2m33s   4GB
Aug 23 12:55:01 Starting examples/compilation/ag32
Aug 23 13:24:59 Finished examples/compilation/ag32                            29m57s  10GB
Aug 23 13:24:59 Starting examples/compilation/ag32/proofs
Aug 23 13:26:00 Finished examples/compilation/ag32/proofs                      1m01s   4GB
Aug 23 13:26:01 Starting examples/compilation/to_word
Aug 23 13:29:31 Finished examples/compilation/to_word                          3m30s   4GB
Aug 23 13:29:31 Starting examples/lpr_checker
Aug 23 13:30:37 Finished examples/lpr_checker                                  1m05s   1GB
Aug 23 13:30:37 Starting examples/lpr_checker/array
Aug 23 14:07:41 Finished examples/lpr_checker/array                           37m01s   4GB
Aug 23 14:07:42 Starting examples/lpr_checker/array/compilation
Aug 23 15:00:06 Finished examples/lpr_checker/array/compilation               52m24s  24GB
Aug 23 15:00:06 Starting examples/lpr_checker/array/compilation/proofs
Aug 23 15:02:06 Finished examples/lpr_checker/array/compilation/proofs         1m59s   3GB
Aug 23 15:02:07 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 23 15:14:39 Finished examples/lpr_checker/array/compilation/proofsARM8    12m31s  21GB
Aug 23 15:14:39 Starting examples/opentheory
Aug 23 15:25:41 Finished examples/opentheory                                  11m01s   3GB
Aug 23 15:25:41 Starting examples/opentheory
Aug 23 15:25:43 Finished examples/opentheory                                      1s  32MB
Aug 23 15:25:43 Starting examples/opentheory/compilation
Aug 23 16:02:31 Finished examples/opentheory/compilation                      36m47s  27GB
Aug 23 16:02:31 Starting examples/opentheory/compilation/proofs
Aug 23 16:03:31 Finished examples/opentheory/compilation/proofs                  59s   5GB
Aug 23 16:03:31 Starting examples/opentheory/compilation/ag32
Aug 23 16:36:45 Finished examples/opentheory/compilation/ag32                 33m11s  28GB
Aug 23 16:36:47 Starting examples/opentheory/compilation/ag32/proofs
Aug 23 16:38:37 Finished examples/opentheory/compilation/ag32/proofs           1m50s   5GB
Aug 23 16:38:37 Starting examples/sat_encodings
Aug 23 16:40:39 Finished examples/sat_encodings                                2m01s   1GB
Aug 23 16:40:39 Starting examples/sat_encodings/case_studies
Aug 23 16:42:23 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Aug 23 16:42:23 Starting examples/sat_encodings/translation
Aug 23 16:48:41 Finished examples/sat_encodings/translation                    6m17s   5GB
Aug 23 16:48:41 Starting examples/sat_encodings/translation/compilation
Aug 23 17:34:57 Finished examples/sat_encodings/translation/compilation       46m15s  22GB
Aug 23 17:34:57 Starting examples/deflate
Aug 23 17:35:59 Finished examples/deflate                                      1m01s 980MB
Aug 23 17:35:59 Starting examples/deflate/translation
Aug 23 17:37:50 Finished examples/deflate/translation                          1m49s   3GB
Aug 23 17:37:50 Starting examples/deflate/translation/compilation
Aug 23 17:58:03 Finished examples/deflate/translation/compilation             20m13s  12GB
Aug 23 17:58:03 Starting examples/vipr
Aug 23 18:02:12 Finished examples/vipr                                         4m09s   5GB
Aug 23 18:02:12 Starting examples/vipr/compilation
Aug 23 18:22:43 Finished examples/vipr/compilation                            20m30s  17GB
Aug 23 18:22:43 Starting translator/okasaki-examples
Aug 23 18:27:56 Finished translator/okasaki-examples                           5m13s   2GB
Aug 23 18:27:56 Starting translator/other-examples
Aug 23 18:30:42 Finished translator/other-examples                             2m45s   2GB
Aug 23 18:30:42 Starting compiler/parsing/tests
Aug 23 18:31:14 Finished compiler/parsing/tests                                  31s 935MB
Aug 23 18:31:14 Starting compiler/inference/tests
Aug 23 18:39:50 Finished compiler/inference/tests                              8m32s   3GB
Aug 23 18:39:50 Starting compiler/printing/test
Aug 23 18:43:41 Finished compiler/printing/test                                3m50s   3GB
Aug 23 18:43:42 Starting icing/flover
Aug 23 19:27:18 Finished icing/flover                                         43m36s   2GB
Aug 23 19:27:18 Starting icing/
Aug 23 20:22:29 Finished icing/                                               55m09s  10GB
Aug 23 20:22:29 Starting icing/examples
Aug 23 20:24:05 Finished icing/examples                                        1m35s   4GB
Aug 23 20:24:05 Starting compiler/repl
Aug 23 20:32:41 Finished compiler/repl                                         8m35s   6GB
Aug 23 20:32:41 Starting unverified/sexpr-bootstrap/x64/64
Aug 23 20:45:52 Finished unverified/sexpr-bootstrap/x64/64                    13m11s  14GB
Aug 23 20:45:52 Starting unverified/sexpr-bootstrap/x64/32
Aug 23 20:56:40 Finished unverified/sexpr-bootstrap/x64/32                    10m47s  14GB
Aug 23 20:56:40 Starting compiler/benchmarks
Aug 23 21:12:00 Finished compiler/benchmarks                                  15m19s   2GB
Aug 23 21:12:00 Starting compiler/bootstrap/compilation/x64/64
Aug 24 10:06:28 Finished compiler/bootstrap/compilation/x64/64             12h54m27s  64GB
Aug 24 10:06:28 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 24 10:26:53 Finished compiler/bootstrap/compilation/x64/64/proofs         20m24s  28GB
Aug 24 10:26:53 Starting compiler/bootstrap/compilation/x64/32
Aug 24 17:36:16 Finished compiler/bootstrap/compilation/x64/32              7h09m20s  64GB
Aug 24 17:36:16 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 24 17:39:40 Finished compiler/bootstrap/compilation/x64/32/proofs          3m23s  21GB
Aug 24 17:39:40 Starting compiler/bootstrap/compilation/ag32/32
Aug 25 00:57:25 Finished compiler/bootstrap/compilation/ag32/32             7h17m43s  64GB
Aug 25 00:57:25 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 25 01:04:09 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m44s  32GB
Aug 25 01:04:09 SUCCESS