Job 2579

CakeML:b534b6cfe6952ec55e6467bfa95ca5f9744db09e
  Translation adjustments [Aug 22 23:53:36]
#1046 (pancake_annot_comments)
Merging into:f2acd9026b44c751edc2f113caaffb9ce76b8348
  Merge pull request #1048 from halogentlepersuasion/pan_mainretval [Aug 24 11:22:44]
HOL:5fc7a6047d48839800489adfb2c2eac7f3ffd5fc
  Add missing export [Aug 21 10:25:23]
Machine:pavlova

Aug 25 10:07:17 Claimed job
Aug 25 10:07:21 Reusing HOL
Aug 25 10:07:32 Starting developers
Aug 25 10:07:35 Finished developers                                               2s 235MB
Aug 25 10:07:36 Starting developers/bin
Aug 25 10:07:46 Finished developers/bin                                           9s   1GB
Aug 25 10:07:47 Starting compiler/proofs
Aug 25 11:49:10 Finished compiler/proofs                                    1h41m21s  36GB
Aug 25 11:49:11 Starting compiler/bootstrap/translation
Aug 25 20:27:55 Finished compiler/bootstrap/translation                     8h38m43s  70GB
Aug 25 20:27:56 Starting semantics/ffi
Aug 25 20:28:05 Finished semantics/ffi                                            7s 830MB
Aug 25 20:28:06 Starting semantics
Aug 25 20:28:07 Finished semantics                                                0s  64MB
Aug 25 20:28:08 Starting semantics/proofs
Aug 25 20:28:31 Finished semantics/proofs                                        22s 777MB
Aug 25 20:28:32 Starting semantics/alt_semantics
Aug 25 20:28:57 Finished semantics/alt_semantics                                 24s 916MB
Aug 25 20:28:58 Starting semantics/alt_semantics/proofs
Aug 25 20:39:11 Finished semantics/alt_semantics/proofs                       10m12s   2GB
Aug 25 20:39:12 Starting basis/pure
Aug 25 20:39:14 Finished basis/pure                                               0s  70MB
Aug 25 20:39:15 Starting translator
Aug 25 20:40:50 Finished translator                                            1m34s   3GB
Aug 25 20:40:51 Starting compiler/parsing
Aug 25 20:40:52 Finished compiler/parsing                                         0s  73MB
Aug 25 20:40:53 Starting characteristic
Aug 25 20:40:55 Finished characteristic                                           0s  90MB
Aug 25 20:40:56 Starting translator/monadic
Aug 25 20:40:57 Finished translator/monadic                                       0s  98MB
Aug 25 20:40:58 Starting basis
Aug 25 20:44:17 Finished basis                                                 3m17s   7GB
Aug 25 20:44:18 Starting compiler/inference
Aug 25 20:44:19 Finished compiler/inference                                       0s  94MB
Aug 25 20:44:20 Starting compiler/backend/reg_alloc
Aug 25 20:44:22 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 25 20:44:22 Starting compiler/backend/gc
Aug 25 20:44:24 Finished compiler/backend/gc                                      0s 148MB
Aug 25 20:44:25 Starting compiler/backend
Aug 25 20:44:30 Finished compiler/backend                                         4s 355MB
Aug 25 20:44:31 Starting compiler/encoders/asm
Aug 25 20:44:32 Finished compiler/encoders/asm                                    0s  91MB
Aug 25 20:44:33 Starting compiler/encoders/x64
Aug 25 20:44:35 Finished compiler/encoders/x64                                    0s 103MB
Aug 25 20:44:36 Starting compiler/encoders/arm7
Aug 25 20:44:37 Finished compiler/encoders/arm7                                   0s 102MB
Aug 25 20:44:38 Starting compiler/encoders/arm8
Aug 25 20:44:40 Finished compiler/encoders/arm8                                   0s 104MB
Aug 25 20:44:40 Starting compiler/encoders/arm8_asl
Aug 25 20:46:51 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Aug 25 20:46:52 Starting compiler/encoders/mips
Aug 25 20:46:54 Finished compiler/encoders/mips                                   0s 105MB
Aug 25 20:46:54 Starting compiler/encoders/riscv
Aug 25 20:46:56 Finished compiler/encoders/riscv                                  0s 103MB
Aug 25 20:46:57 Starting compiler/encoders/ag32
Aug 25 20:46:58 Finished compiler/encoders/ag32                                   0s  94MB
Aug 25 20:46:59 Starting compiler/backend/x64
Aug 25 20:47:01 Finished compiler/backend/x64                                     0s 146MB
Aug 25 20:47:02 Starting compiler/backend/arm7
Aug 25 20:47:04 Finished compiler/backend/arm7                                    0s 146MB
Aug 25 20:47:05 Starting compiler/backend/arm8
Aug 25 20:47:06 Finished compiler/backend/arm8                                    0s 141MB
Aug 25 20:47:07 Starting compiler/backend/mips
Aug 25 20:47:09 Finished compiler/backend/mips                                    0s 135MB
Aug 25 20:47:10 Starting compiler/backend/riscv
Aug 25 20:47:12 Finished compiler/backend/riscv                                   0s 134MB
Aug 25 20:47:13 Starting compiler/backend/ag32
Aug 25 20:48:34 Finished compiler/backend/ag32                                 1m20s   3GB
Aug 25 20:48:35 Starting compiler/parsing/proofs
Aug 25 20:48:37 Finished compiler/parsing/proofs                                  0s  75MB
Aug 25 20:48:38 Starting compiler/inference/proofs
Aug 25 20:48:39 Finished compiler/inference/proofs                                0s  95MB
Aug 25 20:48:40 Starting compiler/backend/semantics
Aug 25 20:51:51 Finished compiler/backend/semantics                            3m10s   2GB
Aug 25 20:51:52 Starting compiler/backend/reg_alloc/proofs
Aug 25 20:51:54 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Aug 25 20:51:55 Starting compiler/backend/proofs
Aug 25 20:52:52 Finished compiler/backend/proofs                                 56s   4GB
Aug 25 20:52:53 Starting compiler/backend/serialiser
Aug 25 20:52:55 Finished compiler/backend/serialiser                              0s 142MB
Aug 25 20:52:55 Starting compiler/encoders/x64/proofs
Aug 25 21:02:04 Finished compiler/encoders/x64/proofs                          9m07s   5GB
Aug 25 21:02:05 Starting compiler/encoders/arm7/proofs
Aug 25 21:14:56 Finished compiler/encoders/arm7/proofs                        12m50s  10GB
Aug 25 21:14:57 Starting compiler/encoders/arm8/proofs
Aug 25 21:21:31 Finished compiler/encoders/arm8/proofs                         6m32s   5GB
Aug 25 21:21:32 Starting compiler/encoders/arm8_asl/proofs
Aug 25 21:35:22 Finished compiler/encoders/arm8_asl/proofs                    13m49s   4GB
Aug 25 21:35:23 Starting compiler/encoders/mips/proofs
Aug 25 21:45:30 Finished compiler/encoders/mips/proofs                        10m05s   7GB
Aug 25 21:45:31 Starting compiler/encoders/riscv/proofs
Aug 25 21:54:04 Finished compiler/encoders/riscv/proofs                        8m32s   6GB
Aug 25 21:54:05 Starting compiler/encoders/ag32/proofs
Aug 25 21:56:30 Finished compiler/encoders/ag32/proofs                         2m24s   3GB
Aug 25 21:56:31 Starting compiler/backend/x64/proofs
Aug 25 21:57:14 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 25 21:57:15 Starting compiler/backend/arm7/proofs
Aug 25 21:58:00 Finished compiler/backend/arm7/proofs                            44s   3GB
Aug 25 21:58:01 Starting compiler/backend/arm8/proofs
Aug 25 21:58:44 Finished compiler/backend/arm8/proofs                            42s   3GB
Aug 25 21:58:45 Starting compiler/backend/arm8_asl
Aug 25 21:59:14 Finished compiler/backend/arm8_asl                               28s   2GB
Aug 25 21:59:15 Starting compiler/backend/mips/proofs
Aug 25 22:00:01 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 25 22:00:02 Starting compiler/backend/riscv/proofs
Aug 25 22:00:54 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 25 22:00:55 Starting compiler/backend/ag32/proofs
Aug 25 22:15:17 Finished compiler/backend/ag32/proofs                         14m20s   6GB
Aug 25 22:15:18 Starting compiler/backend/cv_compute
Aug 25 22:17:00 Finished compiler/backend/cv_compute                           1m41s   3GB
Aug 25 22:17:01 Starting cv_translator
Aug 25 22:36:09 Finished cv_translator                                        19m06s  11GB
Aug 25 22:36:09 Starting candle/set-theory
Aug 25 22:36:58 Finished candle/set-theory                                       47s   1GB
Aug 25 22:36:59 Starting candle/syntax-lib
Aug 25 22:37:00 Finished candle/syntax-lib                                        0s  77MB
Aug 25 22:37:01 Starting candle/standard/syntax
Aug 25 22:37:20 Finished candle/standard/syntax                                  18s   1GB
Aug 25 22:37:21 Starting candle/standard/semantics
Aug 25 22:40:01 Finished candle/standard/semantics                             2m38s   3GB
Aug 25 22:40:02 Starting candle/standard/monadic
Aug 25 22:40:03 Finished candle/standard/monadic                                  0s 106MB
Aug 25 22:40:04 Starting candle/standard/ml_kernel
Aug 25 22:42:01 Finished candle/standard/ml_kernel                             1m56s   4GB
Aug 25 22:42:02 Starting candle/overloading/syntax
Aug 25 22:45:40 Finished candle/overloading/syntax                             3m37s   2GB
Aug 25 22:45:41 Starting candle/overloading/semantics
Aug 25 22:57:12 Finished candle/overloading/semantics                         11m29s   3GB
Aug 25 22:57:13 Starting candle/overloading/monadic
Aug 25 22:59:49 Finished candle/overloading/monadic                            2m35s   2GB
Aug 25 22:59:50 Starting candle/overloading/ml_kernel
Aug 25 23:07:33 Finished candle/overloading/ml_kernel                          7m42s   7GB
Aug 25 23:07:34 Starting candle/overloading/ml_checker
Aug 25 23:10:11 Finished candle/overloading/ml_checker                         2m35s   6GB
Aug 25 23:10:12 Starting candle/prover
Aug 25 23:20:24 Finished candle/prover                                        10m11s   5GB
Aug 25 23:20:25 Starting pancake
Aug 25 23:20:50 Finished pancake                                                 23s 834MB
Aug 25 23:20:50 Starting pancake/ffi
Aug 25 23:20:51 Finished pancake/ffi                                              0s  23MB
Aug 25 23:20:52 Starting pancake/semantics
Aug 25 23:22:57 Finished pancake/semantics                                     2m03s   2GB
Aug 25 23:22:58 Starting pancake/parser
Aug 25 23:23:19 Finished pancake/parser                                          20s 812MB
Aug 25 23:23:20 Starting pancake/proofs
Aug 25 23:38:18 Finished pancake/proofs                                       14m56s   7GB
Aug 25 23:38:19 Starting characteristic/examples
Aug 25 23:39:45 Finished characteristic/examples                               1m25s   5GB
Aug 25 23:39:46 Starting tutorial/solutions
Aug 25 23:42:30 Finished tutorial/solutions                                    2m43s   5GB
Aug 25 23:42:31 Starting translator/monadic/examples
Aug 25 23:45:40 Finished translator/monadic/examples                           3m08s   4GB
Aug 25 23:45:41 Starting examples
Aug 25 23:57:52 Finished examples                                             12m10s   4GB
Aug 25 23:57:53 Starting examples/compilation/x64
Aug 26 00:07:33 Finished examples/compilation/x64                              9m38s   7GB
Aug 26 00:07:34 Starting examples/compilation/x64/proofs
Aug 26 00:12:07 Finished examples/compilation/x64/proofs                       4m32s   8GB
Aug 26 00:12:08 Starting examples/compilation/ag32
Aug 26 00:14:50 Finished examples/compilation/ag32                             2m41s   5GB
Aug 26 00:14:51 Starting examples/compilation/ag32/proofs
Aug 26 00:16:32 Finished examples/compilation/ag32/proofs                      1m39s  10GB
Aug 26 00:16:33 Starting examples/compilation/to_word
Aug 26 00:20:34 Finished examples/compilation/to_word                          4m00s  13GB
Aug 26 00:20:35 Starting examples/lpr_checker
Aug 26 00:21:12 Finished examples/lpr_checker                                    36s   1GB
Aug 26 00:21:13 Starting examples/lpr_checker/array
Aug 26 00:47:38 Finished examples/lpr_checker/array                           26m24s  18GB
Aug 26 00:47:39 Starting examples/lpr_checker/array/compilation
Aug 26 00:50:14 Finished examples/lpr_checker/array/compilation                2m33s   9GB
Aug 26 00:50:15 Starting examples/lpr_checker/array/compilation/proofs
Aug 26 00:52:10 Finished examples/lpr_checker/array/compilation/proofs         1m54s   8GB
Aug 26 00:52:11 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 26 00:53:59 Finished examples/lpr_checker/array/compilation/proofsARM8     1m47s   9GB
Aug 26 00:54:00 Starting examples/xlrup_checker
Aug 26 00:54:35 Finished examples/xlrup_checker                                  33s   1GB
Aug 26 00:54:36 Starting examples/xlrup_checker/array
Aug 26 01:07:39 Finished examples/xlrup_checker/array                         13m01s  11GB
Aug 26 01:07:40 Starting examples/xlrup_checker/array/compilation
Aug 26 01:09:05 Finished examples/xlrup_checker/array/compilation              1m24s   6GB
Aug 26 01:09:06 Starting examples/xlrup_checker/array/compilation/proofs
Aug 26 01:10:48 Finished examples/xlrup_checker/array/compilation/proofs       1m41s   8GB
Aug 26 01:10:49 Starting examples/pseudo_bool
Aug 26 01:12:12 Finished examples/pseudo_bool                                  1m21s   1GB
Aug 26 01:12:13 Starting examples/pseudo_bool/cnf_encoding
Aug 26 01:12:51 Finished examples/pseudo_bool/cnf_encoding                       37s   1GB
Aug 26 01:12:52 Starting examples/pseudo_bool/graph_encoding
Aug 26 01:13:46 Finished examples/pseudo_bool/graph_encoding                     52s   2GB
Aug 26 01:13:47 Starting examples/pseudo_bool/array
Aug 26 02:16:22 Finished examples/pseudo_bool/array                         1h02m34s  30GB
Aug 26 02:16:23 Starting examples/pseudo_bool/array/compilation
Aug 26 02:29:53 Finished examples/pseudo_bool/array/compilation               13m28s  31GB
Aug 26 02:29:54 Starting examples/pseudo_bool/array/compilation/proofs
Aug 26 02:33:59 Finished examples/pseudo_bool/array/compilation/proofs         4m04s  10GB
Aug 26 02:34:00 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 26 02:35:52 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m51s   9GB
Aug 26 02:35:53 Starting examples/opentheory
Aug 26 02:44:21 Finished examples/opentheory                                   8m27s   5GB
Aug 26 02:44:22 Starting examples/opentheory
Aug 26 02:44:24 Finished examples/opentheory                                      0s 130MB
Aug 26 02:44:25 Starting examples/opentheory/compilation
Aug 26 02:46:28 Finished examples/opentheory/compilation                       2m02s   9GB
Aug 26 02:46:29 Starting examples/opentheory/compilation/proofs
Aug 26 02:48:08 Finished examples/opentheory/compilation/proofs                1m38s   7GB
Aug 26 02:48:09 Starting examples/opentheory/compilation/ag32
Aug 26 02:50:16 Finished examples/opentheory/compilation/ag32                  2m06s  10GB
Aug 26 02:50:17 Starting examples/opentheory/compilation/ag32/proofs
Aug 26 02:52:37 Finished examples/opentheory/compilation/ag32/proofs           2m19s  11GB
Aug 26 02:52:38 Starting examples/sat_encodings
Aug 26 02:53:38 Finished examples/sat_encodings                                  58s 905MB
Aug 26 02:53:38 Starting examples/sat_encodings/case_studies
Aug 26 02:55:45 Finished examples/sat_encodings/case_studies                   2m05s   2GB
Aug 26 02:55:45 Starting examples/sat_encodings/translation
Aug 26 02:59:24 Finished examples/sat_encodings/translation                    3m38s   3GB
Aug 26 02:59:25 Starting examples/sat_encodings/translation/compilation
Aug 26 03:01:51 Finished examples/sat_encodings/translation/compilation        2m25s   7GB
Aug 26 03:01:52 Starting examples/deflate
Aug 26 03:02:19 Finished examples/deflate                                        25s 706MB
Aug 26 03:02:20 Starting examples/deflate/translation
Aug 26 03:03:18 Finished examples/deflate/translation                            57s   2GB
Aug 26 03:03:18 Starting examples/deflate/translation/compilation
Aug 26 03:04:26 Finished examples/deflate/translation/compilation              1m06s   5GB
Aug 26 03:04:27 Starting examples/vipr
Aug 26 03:08:01 Finished examples/vipr                                         3m33s   7GB
Aug 26 03:08:02 Starting examples/vipr/compilation
Aug 26 03:09:20 Finished examples/vipr/compilation                             1m17s   6GB
Aug 26 03:09:20 Starting translator/okasaki-examples
Aug 26 03:13:44 Finished translator/okasaki-examples                           4m22s   4GB
Aug 26 03:13:45 Starting translator/other-examples
Aug 26 03:15:04 Finished translator/other-examples                             1m17s   3GB
Aug 26 03:15:05 Starting compiler/parsing/tests
Aug 26 03:15:42 Finished compiler/parsing/tests                                  36s   2GB
Aug 26 03:15:43 Starting compiler/inference/tests
Aug 26 03:16:28 Finished compiler/inference/tests                                43s   3GB
Aug 26 03:16:29 Starting compiler/printing/test
Aug 26 03:18:01 Finished compiler/printing/test                                1m31s   5GB
Aug 26 03:18:02 Starting icing/flover
Aug 26 03:54:50 Finished icing/flover                                         36m47s   4GB
Aug 26 03:54:51 Starting icing/
Aug 26 04:22:45 Finished icing/                                               27m52s   9GB
Aug 26 04:22:46 Starting icing/examples
Aug 26 04:24:30 Finished icing/examples                                        1m43s   6GB
Aug 26 04:24:31 Starting compiler/repl
Aug 26 04:33:29 Finished compiler/repl                                         8m57s  11GB
Aug 26 04:33:30 Starting unverified/sexpr-bootstrap/x64/64
Aug 26 04:46:36 Finished unverified/sexpr-bootstrap/x64/64                    13m04s  18GB
Aug 26 04:46:37 Starting unverified/sexpr-bootstrap/x64/32
Aug 26 04:57:02 Finished unverified/sexpr-bootstrap/x64/32                    10m24s  15GB
Aug 26 04:57:03 Starting compiler/benchmarks
Aug 26 04:57:47 Finished compiler/benchmarks                                     43s 713MB
Aug 26 04:57:48 Starting compiler/bootstrap/compilation/x64/64
Aug 26 05:41:42 Finished compiler/bootstrap/compilation/x64/64                43m53s 132GB
Aug 26 05:41:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 26 06:05:39 Finished compiler/bootstrap/compilation/x64/64/proofs         23m54s  53GB
Aug 26 06:05:40 Starting compiler/bootstrap/compilation/x64/32
Aug 26 06:43:59 Finished compiler/bootstrap/compilation/x64/32                38m17s  94GB
Aug 26 06:44:00 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 26 06:48:49 Finished compiler/bootstrap/compilation/x64/32/proofs          4m47s  28GB
Aug 26 06:48:50 Starting compiler/bootstrap/compilation/arm8/64
Aug 26 07:45:03 Finished compiler/bootstrap/compilation/arm8/64               56m12s 133GB
Aug 26 07:45:04 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 26 07:50:07 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m01s  29GB
Aug 26 07:50:08 Starting compiler/bootstrap/compilation/ag32/32
Aug 26 08:28:44 Finished compiler/bootstrap/compilation/ag32/32               38m35s  92GB
Aug 26 08:28:45 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 26 08:34:12 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m26s  29GB
Aug 26 08:34:13 SUCCESS