Job 2570

CakeML:b534b6cfe6952ec55e6467bfa95ca5f9744db09e
  Translation adjustments [Aug 22 23:53:36]
#1046 (pancake_annot_comments)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:5fc7a6047d48839800489adfb2c2eac7f3ffd5fc
  Add missing export [Aug 21 10:25:23]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 23 05:10:59 Claimed job
Aug 23 05:11:07 Reusing HOL
Aug 23 05:11:53 Starting developers
Aug 23 05:11:59 Finished developers                                               5s 200MB
Aug 23 05:11:59 Starting developers/bin
Aug 23 05:12:05 Finished developers/bin                                           6s   1GB
Aug 23 05:12:05 Starting compiler/proofs
Aug 23 10:44:45 Resuming compiler/proofs
Aug 23 10:57:07 Finished compiler/proofs                                      12m22s   5GB
Aug 23 10:57:07 Starting compiler/bootstrap/translation
Aug 24 10:17:11 Resuming compiler/bootstrap/translation
Aug 24 12:36:05 Finished compiler/bootstrap/translation                     2h18m53s  62GB
Aug 24 12:36:05 Starting semantics/ffi
Aug 24 12:36:11 Finished semantics/ffi                                            5s 360MB
Aug 24 12:36:11 Starting semantics
Aug 24 12:36:12 Finished semantics                                                1s  20MB
Aug 24 12:36:12 Starting semantics/proofs
Aug 24 12:36:46 Finished semantics/proofs                                        33s 885MB
Aug 24 12:36:46 Starting semantics/alt_semantics
Aug 24 12:37:26 Finished semantics/alt_semantics                                 40s   1GB
Aug 24 12:37:26 Starting semantics/alt_semantics/proofs
Aug 24 12:49:32 Finished semantics/alt_semantics/proofs                       12m05s   1GB
Aug 24 12:49:32 Starting basis/pure
Aug 24 12:49:34 Finished basis/pure                                               1s  19MB
Aug 24 12:49:34 Starting translator
Aug 24 12:51:26 Finished translator                                            1m52s   1GB
Aug 24 12:51:26 Starting compiler/parsing
Aug 24 12:51:28 Finished compiler/parsing                                         1s  20MB
Aug 24 12:51:28 Starting characteristic
Aug 24 12:51:30 Finished characteristic                                           1s  25MB
Aug 24 12:51:30 Starting translator/monadic
Aug 24 12:51:32 Finished translator/monadic                                       1s  21MB
Aug 24 12:51:32 Starting basis
Aug 24 12:55:14 Finished basis                                                 3m41s   4GB
Aug 24 12:55:14 Starting compiler/inference
Aug 24 12:55:16 Finished compiler/inference                                       1s  21MB
Aug 24 12:55:16 Starting compiler/backend/reg_alloc
Aug 24 12:55:17 Finished compiler/backend/reg_alloc                               1s  19MB
Aug 24 12:55:17 Starting compiler/backend/gc
Aug 24 12:55:20 Finished compiler/backend/gc                                      2s  22MB
Aug 24 12:55:20 Starting compiler/backend
Aug 24 12:55:35 Finished compiler/backend                                        15s 970MB
Aug 24 12:55:35 Starting compiler/encoders/asm
Aug 24 12:55:37 Finished compiler/encoders/asm                                    1s  24MB
Aug 24 12:55:37 Starting compiler/encoders/x64
Aug 24 12:55:39 Finished compiler/encoders/x64                                    1s  27MB
Aug 24 12:55:39 Starting compiler/encoders/arm7
Aug 24 12:55:41 Finished compiler/encoders/arm7                                   1s  20MB
Aug 24 12:55:41 Starting compiler/encoders/arm8
Aug 24 12:55:43 Finished compiler/encoders/arm8                                   1s  22MB
Aug 24 12:55:43 Starting compiler/encoders/arm8_asl
Aug 24 12:58:49 Finished compiler/encoders/arm8_asl                            3m05s   1GB
Aug 24 12:58:49 Starting compiler/encoders/mips
Aug 24 12:58:51 Finished compiler/encoders/mips                                   1s  22MB
Aug 24 12:58:51 Starting compiler/encoders/riscv
Aug 24 12:58:53 Finished compiler/encoders/riscv                                  1s  29MB
Aug 24 12:58:53 Starting compiler/encoders/ag32
Aug 24 12:58:55 Finished compiler/encoders/ag32                                   1s  25MB
Aug 24 12:58:55 Starting compiler/backend/x64
Aug 24 12:58:57 Finished compiler/backend/x64                                     2s  32MB
Aug 24 12:58:57 Starting compiler/backend/arm7
Aug 24 12:59:00 Finished compiler/backend/arm7                                    2s  29MB
Aug 24 12:59:00 Starting compiler/backend/arm8
Aug 24 12:59:02 Finished compiler/backend/arm8                                    2s  32MB
Aug 24 12:59:02 Starting compiler/backend/mips
Aug 24 12:59:05 Finished compiler/backend/mips                                    2s  23MB
Aug 24 12:59:05 Starting compiler/backend/riscv
Aug 24 12:59:07 Finished compiler/backend/riscv                                   2s  25MB
Aug 24 12:59:07 Starting compiler/backend/ag32
Aug 24 13:00:35 Finished compiler/backend/ag32                                 1m27s   1GB
Aug 24 13:00:35 Starting compiler/parsing/proofs
Aug 24 13:00:37 Finished compiler/parsing/proofs                                  1s  20MB
Aug 24 13:00:37 Starting compiler/inference/proofs
Aug 24 13:00:39 Finished compiler/inference/proofs                                1s  20MB
Aug 24 13:00:39 Starting compiler/backend/semantics
Aug 24 13:04:32 Finished compiler/backend/semantics                            3m52s   1GB
Aug 24 13:04:32 Starting compiler/backend/reg_alloc/proofs
Aug 24 13:04:34 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Aug 24 13:04:34 Starting compiler/backend/proofs
Aug 24 13:05:34 Finished compiler/backend/proofs                               1m00s   3GB
Aug 24 13:05:34 Starting compiler/backend/serialiser
Aug 24 13:05:37 Finished compiler/backend/serialiser                              2s  27MB
Aug 24 13:05:37 Starting compiler/encoders/x64/proofs
Aug 24 13:15:28 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Aug 24 13:15:28 Starting compiler/encoders/arm7/proofs
Aug 24 13:29:20 Finished compiler/encoders/arm7/proofs                        13m51s   4GB
Aug 24 13:29:20 Starting compiler/encoders/arm8/proofs
Aug 24 13:36:28 Finished compiler/encoders/arm8/proofs                         7m08s   1GB
Aug 24 13:36:28 Starting compiler/encoders/arm8_asl/proofs
Aug 24 13:52:24 Finished compiler/encoders/arm8_asl/proofs                    15m55s   2GB
Aug 24 13:52:24 Starting compiler/encoders/mips/proofs
Aug 24 14:03:05 Finished compiler/encoders/mips/proofs                        10m40s   3GB
Aug 24 14:03:05 Starting compiler/encoders/riscv/proofs
Aug 24 14:12:06 Finished compiler/encoders/riscv/proofs                        9m01s   2GB
Aug 24 14:12:06 Starting compiler/encoders/ag32/proofs
Aug 24 14:14:36 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Aug 24 14:14:36 Starting compiler/backend/x64/proofs
Aug 24 14:15:07 Finished compiler/backend/x64/proofs                             31s   1GB
Aug 24 14:15:08 Starting compiler/backend/arm7/proofs
Aug 24 14:15:41 Finished compiler/backend/arm7/proofs                            33s   1GB
Aug 24 14:15:41 Starting compiler/backend/arm8/proofs
Aug 24 14:16:13 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 24 14:16:14 Starting compiler/backend/arm8_asl
Aug 24 14:16:38 Finished compiler/backend/arm8_asl                               24s   2GB
Aug 24 14:16:38 Starting compiler/backend/mips/proofs
Aug 24 14:17:13 Finished compiler/backend/mips/proofs                            34s   1GB
Aug 24 14:17:13 Starting compiler/backend/riscv/proofs
Aug 24 14:17:51 Finished compiler/backend/riscv/proofs                           37s   2GB
Aug 24 14:17:51 Starting compiler/backend/ag32/proofs
Aug 24 14:32:30 Finished compiler/backend/ag32/proofs                         14m38s   3GB
Aug 24 14:32:30 Starting compiler/backend/cv_compute
Aug 24 14:33:52 Finished compiler/backend/cv_compute                           1m21s   2GB
Aug 24 14:33:52 Starting cv_translator
Aug 24 14:54:26 Finished cv_translator                                        20m34s   8GB
Aug 24 14:54:26 Starting candle/set-theory
Aug 24 14:55:08 Finished candle/set-theory                                       41s   1GB
Aug 24 14:55:08 Starting candle/syntax-lib
Aug 24 14:55:10 Finished candle/syntax-lib                                        1s  19MB
Aug 24 14:55:10 Starting candle/standard/syntax
Aug 24 14:55:22 Finished candle/standard/syntax                                  12s 668MB
Aug 24 14:55:22 Starting candle/standard/semantics
Aug 24 14:57:35 Finished candle/standard/semantics                             2m12s   1GB
Aug 24 14:57:35 Starting candle/standard/monadic
Aug 24 14:57:37 Finished candle/standard/monadic                                  1s  22MB
Aug 24 14:57:37 Starting candle/standard/ml_kernel
Aug 24 14:59:24 Finished candle/standard/ml_kernel                             1m46s   4GB
Aug 24 14:59:24 Starting candle/overloading/syntax
Aug 24 15:02:57 Finished candle/overloading/syntax                             3m32s   1GB
Aug 24 15:02:57 Starting candle/overloading/semantics
Aug 24 15:15:23 Finished candle/overloading/semantics                         12m25s   2GB
Aug 24 15:15:23 Starting candle/overloading/monadic
Aug 24 15:18:05 Finished candle/overloading/monadic                            2m41s   1GB
Aug 24 15:18:05 Starting candle/overloading/ml_kernel
Aug 24 15:26:15 Finished candle/overloading/ml_kernel                          8m10s   4GB
Aug 24 15:26:16 Starting candle/overloading/ml_checker
Aug 24 15:28:56 Finished candle/overloading/ml_checker                         2m40s   2GB
Aug 24 15:28:56 Starting candle/prover
Aug 24 15:39:08 Finished candle/prover                                        10m12s   3GB
Aug 24 15:39:08 Starting pancake
Aug 24 15:39:59 Finished pancake                                                 50s   1GB
Aug 24 15:39:59 Starting pancake/ffi
Aug 24 15:40:00 Finished pancake/ffi                                              0s  13MB
Aug 24 15:40:00 Starting pancake/semantics
Aug 24 15:42:46 Finished pancake/semantics                                     2m46s   1GB
Aug 24 15:42:46 Starting pancake/parser
Aug 24 15:43:19 Finished pancake/parser                                          32s   1GB
Aug 24 15:43:19 Starting pancake/proofs
Aug 24 16:01:12 Finished pancake/proofs                                       17m52s   5GB
Aug 24 16:01:12 Starting characteristic/examples
Aug 24 16:02:49 Finished characteristic/examples                               1m37s   3GB
Aug 24 16:02:50 Starting tutorial/solutions
Aug 24 16:05:39 Finished tutorial/solutions                                    2m49s   3GB
Aug 24 16:05:39 Starting translator/monadic/examples
Aug 24 16:10:00 Finished translator/monadic/examples                           4m20s   2GB
Aug 24 16:10:00 Starting examples
Aug 24 16:26:22 Finished examples                                             16m21s   6GB
Aug 24 16:26:22 Starting examples/compilation/x64
Aug 24 16:35:23 Finished examples/compilation/x64                              9m00s   6GB
Aug 24 16:35:23 Starting examples/compilation/x64/proofs
Aug 24 16:38:17 Finished examples/compilation/x64/proofs                       2m53s   5GB
Aug 24 16:38:17 Starting examples/compilation/ag32
Aug 24 16:40:30 Finished examples/compilation/ag32                             2m12s   2GB
Aug 24 16:40:30 Starting examples/compilation/ag32/proofs
Aug 24 16:41:39 Finished examples/compilation/ag32/proofs                      1m08s   5GB
Aug 24 16:41:39 Starting examples/compilation/to_word
Aug 24 16:45:10 Finished examples/compilation/to_word                          3m30s   4GB
Aug 24 16:45:10 Starting examples/lpr_checker
Aug 24 16:46:19 Finished examples/lpr_checker                                  1m08s 978MB
Aug 24 16:46:19 Starting examples/lpr_checker/array
Aug 24 17:17:03 Finished examples/lpr_checker/array                           30m43s   5GB
Aug 24 17:17:03 Starting examples/lpr_checker/array/compilation
Aug 24 17:19:45 Finished examples/lpr_checker/array/compilation                2m41s   7GB
Aug 24 17:19:45 Starting examples/lpr_checker/array/compilation/proofs
Aug 24 17:21:07 Finished examples/lpr_checker/array/compilation/proofs         1m21s   5GB
Aug 24 17:21:07 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 24 17:22:21 Finished examples/lpr_checker/array/compilation/proofsARM8     1m14s   7GB
Aug 24 17:22:21 Starting examples/xlrup_checker
Aug 24 17:23:26 Finished examples/xlrup_checker                                1m04s   1GB
Aug 24 17:23:26 Starting examples/xlrup_checker/array
Aug 24 17:39:53 Finished examples/xlrup_checker/array                         16m26s   5GB
Aug 24 17:39:53 Starting examples/xlrup_checker/array/compilation
Aug 24 17:41:17 Finished examples/xlrup_checker/array/compilation              1m24s   5GB
Aug 24 17:41:18 Starting examples/xlrup_checker/array/compilation/proofs
Aug 24 17:42:24 Finished examples/xlrup_checker/array/compilation/proofs       1m06s   5GB
Aug 24 17:42:24 Starting examples/pseudo_bool
Aug 24 17:44:28 Finished examples/pseudo_bool                                  2m03s   1GB
Aug 24 17:44:28 Starting examples/pseudo_bool/cnf_encoding
Aug 24 17:44:58 Finished examples/pseudo_bool/cnf_encoding                       29s 913MB
Aug 24 17:44:58 Starting examples/pseudo_bool/graph_encoding
Aug 24 17:45:45 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Aug 24 17:45:45 Starting examples/pseudo_bool/array
Aug 24 18:56:32 Finished examples/pseudo_bool/array                         1h10m47s   9GB
Aug 24 18:56:32 Starting examples/pseudo_bool/array/compilation
Aug 24 19:11:38 Finished examples/pseudo_bool/array/compilation               15m06s  23GB
Aug 24 19:11:38 Starting examples/pseudo_bool/array/compilation/proofs
Aug 24 19:14:33 Finished examples/pseudo_bool/array/compilation/proofs         2m55s   7GB
Aug 24 19:14:34 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 24 19:15:57 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m23s   7GB
Aug 24 19:15:57 Starting examples/opentheory
Aug 24 19:27:18 Finished examples/opentheory                                  11m20s   5GB
Aug 24 19:27:18 Starting examples/opentheory
Aug 24 19:27:20 Finished examples/opentheory                                      1s  25MB
Aug 24 19:27:20 Starting examples/opentheory/compilation
Aug 24 19:29:22 Finished examples/opentheory/compilation                       2m01s   6GB
Aug 24 19:29:22 Starting examples/opentheory/compilation/proofs
Aug 24 19:30:30 Finished examples/opentheory/compilation/proofs                1m07s   5GB
Aug 24 19:30:30 Starting examples/opentheory/compilation/ag32
Aug 24 19:32:32 Finished examples/opentheory/compilation/ag32                  2m01s   5GB
Aug 24 19:32:32 Starting examples/opentheory/compilation/ag32/proofs
Aug 24 19:34:16 Finished examples/opentheory/compilation/ag32/proofs           1m44s   8GB
Aug 24 19:34:16 Starting examples/sat_encodings
Aug 24 19:36:37 Finished examples/sat_encodings                                2m21s   1GB
Aug 24 19:36:38 Starting examples/sat_encodings/case_studies
Aug 24 19:38:31 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Aug 24 19:38:31 Starting examples/sat_encodings/translation
Aug 24 19:45:04 Finished examples/sat_encodings/translation                    6m33s   4GB
Aug 24 19:45:04 Starting examples/sat_encodings/translation/compilation
Aug 24 19:47:29 Finished examples/sat_encodings/translation/compilation        2m24s   6GB
Aug 24 19:47:29 Starting examples/deflate
Aug 24 19:48:39 Finished examples/deflate                                      1m10s   1GB
Aug 24 19:48:39 Starting examples/deflate/translation
Aug 24 19:50:27 Finished examples/deflate/translation                          1m47s   3GB
Aug 24 19:50:27 Starting examples/deflate/translation/compilation
Aug 24 19:51:37 Finished examples/deflate/translation/compilation              1m10s   4GB
Aug 24 19:51:37 Starting examples/vipr
Aug 24 19:55:56 Finished examples/vipr                                         4m18s   5GB
Aug 24 19:55:57 Starting examples/vipr/compilation
Aug 24 19:57:13 Finished examples/vipr/compilation                             1m16s   4GB
Aug 24 19:57:13 Starting translator/okasaki-examples
Aug 24 20:02:33 Finished translator/okasaki-examples                           5m19s   2GB
Aug 24 20:02:33 Starting translator/other-examples
Aug 24 20:06:25 Finished translator/other-examples                             3m51s   1GB
Aug 24 20:06:25 Starting compiler/parsing/tests
Aug 24 20:07:01 Finished compiler/parsing/tests                                  36s   1GB
Aug 24 20:07:01 Starting compiler/inference/tests
Aug 24 20:07:34 Finished compiler/inference/tests                                32s   1GB
Aug 24 20:07:34 Starting compiler/printing/test
Aug 24 20:09:07 Finished compiler/printing/test                                1m32s   3GB
Aug 24 20:09:07 Starting icing/flover
Aug 24 20:54:47 Finished icing/flover                                         45m39s   2GB
Aug 24 20:54:47 Starting icing/
Aug 24 21:24:03 Finished icing/                                               29m16s   3GB
Aug 24 21:24:03 Starting icing/examples
Aug 24 21:25:55 Finished icing/examples                                        1m51s   4GB
Aug 24 21:25:55 Starting compiler/repl
Aug 24 21:34:42 Finished compiler/repl                                         8m46s   6GB
Aug 24 21:34:42 Starting unverified/sexpr-bootstrap/x64/64
Aug 24 21:51:04 Finished unverified/sexpr-bootstrap/x64/64                    16m22s  19GB
Aug 24 21:51:04 Starting unverified/sexpr-bootstrap/x64/32
Aug 24 22:04:10 Finished unverified/sexpr-bootstrap/x64/32                    13m05s  15GB
Aug 24 22:04:10 Starting compiler/benchmarks
Aug 24 22:19:50 Finished compiler/benchmarks                                  15m40s   2GB
Aug 24 22:19:50 Starting compiler/bootstrap/compilation/x64/64
Aug 24 23:00:04 Finished compiler/bootstrap/compilation/x64/64                40m13s  63GB
Aug 24 23:00:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 24 23:24:52 Finished compiler/bootstrap/compilation/x64/64/proofs         24m47s  59GB
Aug 24 23:24:52 Starting compiler/bootstrap/compilation/x64/32
Aug 25 00:04:27 Finished compiler/bootstrap/compilation/x64/32                39m35s  64GB
Aug 25 00:04:27 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 25 00:10:33 Finished compiler/bootstrap/compilation/x64/32/proofs          6m05s  20GB
Aug 25 00:10:33 Starting compiler/bootstrap/compilation/arm8/64
Aug 25 01:01:45 Finished compiler/bootstrap/compilation/arm8/64               51m11s  64GB
Aug 25 01:01:45 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 25 01:06:49 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m03s  31GB
Aug 25 01:06:49 Starting compiler/bootstrap/compilation/ag32/32
Aug 25 01:43:20 Finished compiler/bootstrap/compilation/ag32/32               36m31s  64GB
Aug 25 01:43:20 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 25 01:50:00 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m40s  20GB
Aug 25 01:50:01 SUCCESS