Job 2479

CakeML:030aba6c2987c7c7d44d4dad65cb6dc8f778a40a
  Lift out basis_def translation from compilerXProg [Jul 16 06:31:21]
#1013 (basis_def-translation)
Merging into:6cdeb10d4b89bd7583574cdfb1d7a3c11bf8f52d
  Adjust translations of toSortedAList [Jul 19 09:41:46]
HOL:c37de731916a5fe5fdc6218d4b2e19234435e4ce
  Add lots of regexp matching regression tests for DBSearchParser [Jul 15 06:13:45]
Machine:pavlova

Jul 22 02:50:25 Claimed job
Jul 22 02:50:29 Reusing HOL
Jul 22 02:50:40 Starting developers
Jul 22 02:50:43 Finished developers                                               2s 218MB
Jul 22 02:50:44 Starting developers/bin
Jul 22 02:50:56 Finished developers/bin                                          10s   1GB
Jul 22 02:50:56 Starting compiler/proofs
Jul 22 04:43:27 Finished compiler/proofs                                    1h52m29s  33GB
Jul 22 04:43:28 Starting compiler/bootstrap/translation
Jul 22 12:53:55 Finished compiler/bootstrap/translation                     8h10m25s  61GB
Jul 22 12:53:56 Starting semantics/ffi
Jul 22 12:54:05 Finished semantics/ffi                                            7s 639MB
Jul 22 12:54:06 Starting semantics
Jul 22 12:54:07 Finished semantics                                                0s  69MB
Jul 22 12:54:08 Starting semantics/proofs
Jul 22 12:54:45 Finished semantics/proofs                                        35s   1GB
Jul 22 12:54:46 Starting semantics/alt_semantics
Jul 22 12:55:27 Finished semantics/alt_semantics                                 40s   1GB
Jul 22 12:55:28 Starting semantics/alt_semantics/proofs
Jul 23 05:33:13 Resuming semantics/alt_semantics/proofs
Jul 23 05:33:14 Finished semantics/alt_semantics/proofs                           0s  82MB
Jul 23 05:33:15 Starting basis/pure
Jul 23 05:33:16 Finished basis/pure                                               0s  70MB
Jul 23 05:33:17 Starting translator
Jul 23 18:09:14 Resuming translator
Jul 23 18:09:16 Finished translator                                               0s  89MB
Jul 23 18:09:17 Starting compiler/parsing
Jul 23 18:09:18 Finished compiler/parsing                                         0s  71MB
Jul 23 18:09:19 Starting characteristic
Jul 23 18:09:21 Finished characteristic                                           0s  88MB
Jul 23 18:09:21 Starting translator/monadic
Jul 23 18:09:23 Finished translator/monadic                                       0s  96MB
Jul 23 18:09:24 Starting basis
Jul 23 18:12:59 Finished basis                                                 3m34s   5GB
Jul 23 18:13:00 Starting compiler/inference
Jul 23 19:38:10 Resuming compiler/inference
Jul 23 19:38:11 Finished compiler/inference                                       0s  87MB
Jul 23 19:38:12 Starting compiler/backend/reg_alloc
Jul 23 19:38:13 Finished compiler/backend/reg_alloc                               0s  69MB
Jul 23 19:38:14 Starting compiler/backend/gc
Jul 23 19:38:16 Finished compiler/backend/gc                                      0s 137MB
Jul 23 19:38:17 Starting compiler/backend
Jul 23 19:38:37 Finished compiler/backend                                        19s   1GB
Jul 23 19:38:38 Starting compiler/encoders/asm
Jul 23 19:38:40 Finished compiler/encoders/asm                                    0s  90MB
Jul 23 19:38:41 Starting compiler/encoders/x64
Jul 23 19:38:42 Finished compiler/encoders/x64                                    0s 102MB
Jul 23 19:38:43 Starting compiler/encoders/arm7
Jul 23 19:38:44 Finished compiler/encoders/arm7                                   0s 102MB
Jul 23 19:38:45 Starting compiler/encoders/arm8
Jul 23 19:38:47 Finished compiler/encoders/arm8                                   0s  93MB
Jul 23 19:38:48 Starting compiler/encoders/arm8_asl
Jul 23 19:41:01 Finished compiler/encoders/arm8_asl                            2m12s   1GB
Jul 23 19:41:02 Starting compiler/encoders/mips
Jul 23 19:41:04 Finished compiler/encoders/mips                                   0s 101MB
Jul 23 19:41:04 Starting compiler/encoders/riscv
Jul 23 19:41:06 Finished compiler/encoders/riscv                                  0s 101MB
Jul 23 19:41:07 Starting compiler/encoders/ag32
Jul 23 19:41:08 Finished compiler/encoders/ag32                                   0s  97MB
Jul 23 19:41:09 Starting compiler/backend/x64
Jul 23 19:41:11 Finished compiler/backend/x64                                     0s 142MB
Jul 23 19:41:12 Starting compiler/backend/arm7
Jul 23 19:41:14 Finished compiler/backend/arm7                                    0s 142MB
Jul 23 19:41:14 Starting compiler/backend/arm8
Jul 23 19:41:16 Finished compiler/backend/arm8                                    0s 142MB
Jul 23 19:41:17 Starting compiler/backend/mips
Jul 23 19:41:19 Finished compiler/backend/mips                                    0s 142MB
Jul 23 19:41:20 Starting compiler/backend/riscv
Jul 23 19:41:22 Finished compiler/backend/riscv                                   0s 142MB
Jul 23 19:41:22 Starting compiler/backend/ag32
Jul 23 19:42:42 Finished compiler/backend/ag32                                 1m19s   2GB
Jul 23 19:42:43 Starting compiler/parsing/proofs
Jul 23 19:42:45 Finished compiler/parsing/proofs                                  0s  73MB
Jul 23 19:42:46 Starting compiler/inference/proofs
Jul 23 19:42:47 Finished compiler/inference/proofs                                0s  95MB
Jul 23 19:42:48 Starting compiler/backend/semantics
Jul 24 16:31:14 Resuming compiler/backend/semantics
Jul 24 16:31:16 Finished compiler/backend/semantics                               1s 152MB
Jul 24 16:31:17 Starting compiler/backend/reg_alloc/proofs
Jul 24 16:31:19 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jul 24 16:31:20 Starting compiler/backend/proofs
Jul 24 16:32:26 Finished compiler/backend/proofs                               1m05s   4GB
Jul 24 16:32:27 Starting compiler/backend/serialiser
Jul 24 16:32:29 Finished compiler/backend/serialiser                              0s 139MB
Jul 24 16:32:29 Starting compiler/encoders/x64/proofs
Jul 24 16:41:54 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Jul 24 16:41:55 Starting compiler/encoders/arm7/proofs
Jul 24 16:54:49 Finished compiler/encoders/arm7/proofs                        12m52s   7GB
Jul 24 16:54:50 Starting compiler/encoders/arm8/proofs
Jul 24 17:01:17 Finished compiler/encoders/arm8/proofs                         6m26s   7GB
Jul 24 17:01:18 Starting compiler/encoders/arm8_asl/proofs
Jul 24 17:15:33 Finished compiler/encoders/arm8_asl/proofs                    14m14s   3GB
Jul 24 17:15:34 Starting compiler/encoders/mips/proofs
Jul 24 17:25:42 Finished compiler/encoders/mips/proofs                        10m06s   9GB
Jul 24 17:25:43 Starting compiler/encoders/riscv/proofs
Jul 24 17:34:06 Finished compiler/encoders/riscv/proofs                        8m22s   5GB
Jul 24 17:34:07 Starting compiler/encoders/ag32/proofs
Jul 24 17:36:30 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Jul 24 17:36:31 Starting compiler/backend/x64/proofs
Jul 24 17:37:15 Finished compiler/backend/x64/proofs                             43s   3GB
Jul 24 17:37:16 Starting compiler/backend/arm7/proofs
Jul 24 17:38:01 Finished compiler/backend/arm7/proofs                            44s   2GB
Jul 24 17:38:02 Starting compiler/backend/arm8/proofs
Jul 24 17:38:43 Finished compiler/backend/arm8/proofs                            41s   3GB
Jul 24 17:38:44 Starting compiler/backend/arm8_asl
Jul 24 17:39:14 Finished compiler/backend/arm8_asl                               28s   2GB
Jul 24 17:39:15 Starting compiler/backend/mips/proofs
Jul 24 17:40:02 Finished compiler/backend/mips/proofs                            46s   3GB
Jul 24 17:40:03 Starting compiler/backend/riscv/proofs
Jul 24 17:40:55 Finished compiler/backend/riscv/proofs                           50s   4GB
Jul 24 17:40:56 Starting compiler/backend/ag32/proofs
Jul 24 17:55:16 Finished compiler/backend/ag32/proofs                         14m19s   6GB
Jul 24 17:55:17 Starting compiler/backend/cv_compute
Jul 24 17:57:01 Finished compiler/backend/cv_compute                           1m43s   3GB
Jul 24 17:57:02 Starting cv_translator
Jul 24 18:16:21 Finished cv_translator                                        19m17s  11GB
Jul 24 18:16:21 Starting candle/set-theory
Jul 24 18:17:10 Finished candle/set-theory                                       48s   1GB
Jul 24 18:17:11 Starting candle/syntax-lib
Jul 24 18:17:13 Finished candle/syntax-lib                                        0s  72MB
Jul 24 18:17:13 Starting candle/standard/syntax
Jul 24 18:17:32 Finished candle/standard/syntax                                  17s   1GB
Jul 24 18:17:33 Starting candle/standard/semantics
Jul 24 18:20:08 Finished candle/standard/semantics                             2m34s   3GB
Jul 24 18:20:09 Starting candle/standard/monadic
Jul 24 18:20:10 Finished candle/standard/monadic                                  0s  98MB
Jul 24 18:20:11 Starting candle/standard/ml_kernel
Jul 24 18:22:05 Finished candle/standard/ml_kernel                             1m52s   6GB
Jul 24 18:22:05 Starting candle/overloading/syntax
Jul 24 18:25:36 Finished candle/overloading/syntax                             3m29s   3GB
Jul 24 18:25:37 Starting candle/overloading/semantics
Jul 24 18:37:20 Finished candle/overloading/semantics                         11m41s  10GB
Jul 24 18:37:21 Starting candle/overloading/monadic
Jul 24 18:40:01 Finished candle/overloading/monadic                            2m38s   3GB
Jul 24 18:40:02 Starting candle/overloading/ml_kernel
Jul 24 18:47:53 Finished candle/overloading/ml_kernel                          7m50s   6GB
Jul 24 18:47:54 Starting candle/overloading/ml_checker
Jul 24 18:50:33 Finished candle/overloading/ml_checker                         2m38s   7GB
Jul 24 18:50:34 Starting candle/prover
Jul 24 19:00:43 Finished candle/prover                                        10m08s   5GB
Jul 24 19:00:44 Starting pancake
Jul 24 19:01:53 Finished pancake                                               1m07s   1GB
Jul 24 19:01:54 Starting pancake/ffi
Jul 24 19:01:55 Finished pancake/ffi                                              0s  23MB
Jul 24 19:01:55 Starting pancake/semantics
Jul 24 19:04:39 Finished pancake/semantics                                     2m42s   4GB
Jul 24 19:04:40 Starting pancake/parser
Jul 24 19:05:14 Finished pancake/parser                                          32s   2GB
Jul 24 19:05:15 Starting pancake/proofs
Jul 24 19:36:31 Finished pancake/proofs                                       31m15s   8GB
Jul 24 19:36:32 Starting characteristic/examples
Jul 24 19:38:11 Finished characteristic/examples                               1m38s   6GB
Jul 24 19:38:12 Starting tutorial/solutions
Jul 24 19:40:50 Finished tutorial/solutions                                    2m36s   4GB
Jul 24 19:40:51 Starting translator/monadic/examples
Jul 24 19:44:49 Finished translator/monadic/examples                           3m57s   5GB
Jul 24 19:44:50 Starting examples
Jul 24 19:59:28 Finished examples                                             14m36s   8GB
Jul 24 19:59:29 Starting examples/compilation/x64
Jul 24 20:08:39 Finished examples/compilation/x64                              9m09s   7GB
Jul 24 20:08:40 Starting examples/compilation/x64/proofs
Jul 24 20:13:08 Finished examples/compilation/x64/proofs                       4m26s   8GB
Jul 24 20:13:09 Starting examples/compilation/ag32
Jul 24 20:15:45 Finished examples/compilation/ag32                             2m35s   5GB
Jul 24 20:15:46 Starting examples/compilation/ag32/proofs
Jul 24 20:17:41 Finished examples/compilation/ag32/proofs                      1m54s  10GB
Jul 24 20:17:42 Starting examples/compilation/to_word
Jul 24 20:21:39 Finished examples/compilation/to_word                          3m56s  12GB
Jul 24 20:21:40 Starting examples/lpr_checker
Jul 24 20:22:57 Finished examples/lpr_checker                                  1m15s   2GB
Jul 24 20:22:58 Starting examples/lpr_checker/array
Jul 24 20:51:54 Finished examples/lpr_checker/array                           28m54s  11GB
Jul 24 20:51:55 Starting examples/lpr_checker/array/compilation
Jul 24 20:54:25 Finished examples/lpr_checker/array/compilation                2m29s   9GB
Jul 24 20:54:26 Starting examples/lpr_checker/array/compilation/proofs
Jul 24 20:56:17 Finished examples/lpr_checker/array/compilation/proofs         1m49s   9GB
Jul 24 20:56:18 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 24 20:58:03 Finished examples/lpr_checker/array/compilation/proofsARM8     1m44s   8GB
Jul 24 20:58:04 Starting examples/xlrup_checker
Jul 24 20:59:18 Finished examples/xlrup_checker                                1m12s   1GB
Jul 24 20:59:19 Starting examples/xlrup_checker/array
Jul 24 21:14:34 Finished examples/xlrup_checker/array                         15m14s   6GB
Jul 24 21:14:35 Starting examples/xlrup_checker/array/compilation
Jul 24 21:15:59 Finished examples/xlrup_checker/array/compilation              1m23s   6GB
Jul 24 21:16:00 Starting examples/xlrup_checker/array/compilation/proofs
Jul 24 21:17:45 Finished examples/xlrup_checker/array/compilation/proofs       1m43s   9GB
Jul 24 21:17:45 Starting examples/pseudo_bool
Jul 24 21:19:59 Finished examples/pseudo_bool                                  2m12s   2GB
Jul 24 21:20:00 Starting examples/pseudo_bool/cnf_encoding
Jul 24 21:20:38 Finished examples/pseudo_bool/cnf_encoding                       37s   1GB
Jul 24 21:20:39 Starting examples/pseudo_bool/graph_encoding
Jul 24 21:21:31 Finished examples/pseudo_bool/graph_encoding                     50s   1GB
Jul 24 21:21:32 Starting examples/pseudo_bool/array
Jul 24 22:28:00 Finished examples/pseudo_bool/array                         1h06m27s  31GB
Jul 24 22:28:01 Starting examples/pseudo_bool/array/compilation
Jul 24 22:41:04 Finished examples/pseudo_bool/array/compilation               13m02s  30GB
Jul 24 22:41:05 Starting examples/pseudo_bool/array/compilation/proofs
Jul 24 22:45:03 Finished examples/pseudo_bool/array/compilation/proofs         3m57s  10GB
Jul 24 22:45:04 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jul 24 22:46:51 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m46s   9GB
Jul 24 22:46:52 Starting examples/opentheory
Jul 24 22:57:40 Finished examples/opentheory                                  10m47s   8GB
Jul 24 22:57:41 Starting examples/opentheory
Jul 24 22:57:43 Finished examples/opentheory                                      0s 131MB
Jul 24 22:57:44 Starting examples/opentheory/compilation
Jul 24 22:59:48 Finished examples/opentheory/compilation                       2m03s   7GB
Jul 24 22:59:48 Starting examples/opentheory/compilation/proofs
Jul 24 23:01:33 Finished examples/opentheory/compilation/proofs                1m43s   8GB
Jul 24 23:01:34 Starting examples/opentheory/compilation/ag32
Jul 24 23:03:37 Finished examples/opentheory/compilation/ag32                  2m02s   9GB
Jul 24 23:03:38 Starting examples/opentheory/compilation/ag32/proofs
Jul 24 23:06:00 Finished examples/opentheory/compilation/ag32/proofs           2m20s  14GB
Jul 24 23:06:01 Starting examples/sat_encodings
Jul 24 23:08:55 Finished examples/sat_encodings                                2m52s   1GB
Jul 24 23:08:55 Starting examples/sat_encodings/case_studies
Jul 24 23:11:03 Finished examples/sat_encodings/case_studies                   2m06s   2GB
Jul 24 23:11:04 Starting examples/sat_encodings/translation
Jul 24 23:17:29 Finished examples/sat_encodings/translation                    6m24s   8GB
Jul 24 23:17:30 Starting examples/sat_encodings/translation/compilation
Jul 24 23:19:49 Finished examples/sat_encodings/translation/compilation        2m18s   6GB
Jul 24 23:19:50 Starting examples/deflate
Jul 24 23:21:12 Finished examples/deflate                                      1m20s   1GB
Jul 24 23:21:12 Starting examples/deflate/translation
Jul 24 23:22:48 Finished examples/deflate/translation                          1m35s   7GB
Jul 24 23:22:49 Starting examples/deflate/translation/compilation
Jul 24 23:23:54 Finished examples/deflate/translation/compilation              1m04s   5GB
Jul 24 23:23:55 Starting examples/vipr
Jul 24 23:28:05 Finished examples/vipr                                         4m08s   8GB
Jul 24 23:28:06 Starting examples/vipr/compilation
Jul 24 23:29:23 Finished examples/vipr/compilation                             1m16s   6GB
Jul 24 23:29:24 Starting translator/okasaki-examples
Jul 24 23:34:30 Finished translator/okasaki-examples                           5m05s   4GB
Jul 24 23:34:31 Starting translator/other-examples
Jul 24 23:35:45 Finished translator/other-examples                             1m13s   3GB
Jul 24 23:35:46 Starting compiler/parsing/tests
Jul 24 23:36:20 Finished compiler/parsing/tests                                  33s   1GB
Jul 24 23:36:21 Starting compiler/inference/tests
Jul 24 23:37:02 Finished compiler/inference/tests                                39s   3GB
Jul 24 23:37:02 Starting compiler/printing/test
Jul 24 23:38:35 Finished compiler/printing/test                                1m32s   6GB
Jul 24 23:38:36 Starting icing/flover
Jul 25 00:15:42 Finished icing/flover                                         37m04s   3GB
Jul 25 00:15:43 Starting icing/
Jul 25 00:44:03 Finished icing/                                               28m19s  10GB
Jul 25 00:44:04 Starting icing/examples
Jul 25 00:45:52 Finished icing/examples                                        1m47s   8GB
Jul 25 00:45:53 Starting compiler/repl
Jul 25 00:54:59 Finished compiler/repl                                         9m05s  11GB
Jul 25 00:55:00 Starting unverified/sexpr-bootstrap/x64/64
Jul 25 01:06:49 Finished unverified/sexpr-bootstrap/x64/64                    11m48s  17GB
Jul 25 01:06:50 Starting unverified/sexpr-bootstrap/x64/32
Jul 25 01:16:18 Finished unverified/sexpr-bootstrap/x64/32                     9m26s  14GB
Jul 25 01:16:19 Starting compiler/benchmarks
Jul 25 01:17:05 Finished compiler/benchmarks                                     44s 713MB
Jul 25 01:17:05 Starting compiler/bootstrap/compilation/x64/64
Jul 25 02:14:26 Finished compiler/bootstrap/compilation/x64/64                57m20s 124GB
Jul 25 02:14:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 25 02:37:53 Finished compiler/bootstrap/compilation/x64/64/proofs         23m24s  57GB
Jul 25 02:37:53 Starting compiler/bootstrap/compilation/x64/32
Jul 25 03:17:07 Finished compiler/bootstrap/compilation/x64/32                39m12s 102GB
Jul 25 03:17:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 25 03:21:50 Finished compiler/bootstrap/compilation/x64/32/proofs          4m41s  25GB
Jul 25 03:21:51 Starting compiler/bootstrap/compilation/ag32/32
Jul 25 03:59:35 Finished compiler/bootstrap/compilation/ag32/32               37m42s  89GB
Jul 25 03:59:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 25 04:05:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m24s  31GB
Jul 25 04:05:02 SUCCESS