Job 2459

CakeML:030aba6c2987c7c7d44d4dad65cb6dc8f778a40a
  Lift out basis_def translation from compilerXProg [Jul 16 06:31:21]
#1013 (basis_def-translation)
Merging into:1791142331ecadf0de62e3834aa2785ffbd51f8b
  Make a theorem name unambiguous [Jul 17 09:29:17]
HOL:c37de731916a5fe5fdc6218d4b2e19234435e4ce
  Add lots of regexp matching regression tests for DBSearchParser [Jul 15 06:13:45]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Jul 17 14:04:58 Claimed job
Jul 17 14:04:59 Reusing HOL
Jul 17 14:05:44 Starting developers
Jul 17 14:05:49 Finished developers                                               5s 107MB
Jul 17 14:05:50 Starting developers/bin
Jul 17 14:05:55 Finished developers/bin                                           5s   1GB
Jul 17 14:05:56 Starting compiler/proofs
Jul 17 16:08:50 Finished compiler/proofs                                    2h02m53s  16GB
Jul 17 16:08:50 Starting compiler/bootstrap/translation
Jul 18 00:34:58 Finished compiler/bootstrap/translation                     8h26m07s  50GB
Jul 18 00:34:58 Starting semantics/ffi
Jul 18 00:35:03 Finished semantics/ffi                                            5s 436MB
Jul 18 00:35:03 Starting semantics
Jul 18 00:35:05 Finished semantics                                                1s  18MB
Jul 18 00:35:05 Starting semantics/proofs
Jul 18 00:35:39 Finished semantics/proofs                                        33s 859MB
Jul 18 00:35:39 Starting semantics/alt_semantics
Jul 18 00:36:13 Finished semantics/alt_semantics                                 34s 689MB
Jul 18 00:36:13 Starting semantics/alt_semantics/proofs
Jul 18 00:48:16 Finished semantics/alt_semantics/proofs                       12m02s   2GB
Jul 18 00:48:16 Starting basis/pure
Jul 18 00:48:18 Finished basis/pure                                               1s  25MB
Jul 18 00:48:18 Starting translator
Jul 18 00:50:09 Finished translator                                            1m50s   2GB
Jul 18 00:50:09 Starting compiler/parsing
Jul 18 00:50:11 Finished compiler/parsing                                         1s  18MB
Jul 18 00:50:11 Starting characteristic
Jul 18 00:50:13 Finished characteristic                                           1s  24MB
Jul 18 00:50:13 Starting translator/monadic
Jul 18 00:50:15 Finished translator/monadic                                       1s  20MB
Jul 18 00:50:15 Starting basis
Jul 18 00:53:57 Finished basis                                                 3m41s   2GB
Jul 18 00:53:57 Starting compiler/inference
Jul 18 00:53:59 Finished compiler/inference                                       1s  23MB
Jul 18 00:53:59 Starting compiler/backend/reg_alloc
Jul 18 00:54:00 Finished compiler/backend/reg_alloc                               1s  18MB
Jul 18 00:54:00 Starting compiler/backend/gc
Jul 18 00:54:03 Finished compiler/backend/gc                                      2s  25MB
Jul 18 00:54:03 Starting compiler/backend
Jul 18 00:54:18 Finished compiler/backend                                        14s 844MB
Jul 18 00:54:18 Starting compiler/encoders/asm
Jul 18 00:54:20 Finished compiler/encoders/asm                                    1s  21MB
Jul 18 00:54:20 Starting compiler/encoders/x64
Jul 18 00:54:22 Finished compiler/encoders/x64                                    1s  21MB
Jul 18 00:54:22 Starting compiler/encoders/arm7
Jul 18 00:54:23 Finished compiler/encoders/arm7                                   1s  20MB
Jul 18 00:54:24 Starting compiler/encoders/arm8
Jul 18 00:54:25 Finished compiler/encoders/arm8                                   1s  23MB
Jul 18 00:54:26 Starting compiler/encoders/arm8_asl
Jul 18 03:24:50 Finished compiler/encoders/arm8_asl                         2h30m23s  42GB
Jul 18 03:24:50 Starting compiler/encoders/mips
Jul 18 03:24:52 Finished compiler/encoders/mips                                   1s  21MB
Jul 18 03:24:52 Starting compiler/encoders/riscv
Jul 18 03:24:54 Finished compiler/encoders/riscv                                  1s  24MB
Jul 18 03:24:54 Starting compiler/encoders/ag32
Jul 18 03:24:56 Finished compiler/encoders/ag32                                   1s  24MB
Jul 18 03:24:56 Starting compiler/backend/x64
Jul 18 03:24:58 Finished compiler/backend/x64                                     2s  29MB
Jul 18 03:24:58 Starting compiler/backend/arm7
Jul 18 03:25:01 Finished compiler/backend/arm7                                    2s  25MB
Jul 18 03:25:01 Starting compiler/backend/arm8
Jul 18 03:25:03 Finished compiler/backend/arm8                                    2s  20MB
Jul 18 03:25:03 Starting compiler/backend/mips
Jul 18 03:25:06 Finished compiler/backend/mips                                    2s  23MB
Jul 18 03:25:06 Starting compiler/backend/riscv
Jul 18 03:25:08 Finished compiler/backend/riscv                                   2s  30MB
Jul 18 03:25:08 Starting compiler/backend/ag32
Jul 18 03:26:36 Finished compiler/backend/ag32                                 1m28s   1GB
Jul 18 03:26:36 Starting compiler/parsing/proofs
Jul 18 03:26:38 Finished compiler/parsing/proofs                                  1s  20MB
Jul 18 03:26:38 Starting compiler/inference/proofs
Jul 18 03:26:40 Finished compiler/inference/proofs                                1s  20MB
Jul 18 03:26:40 Starting compiler/backend/semantics
Jul 18 03:30:36 Finished compiler/backend/semantics                            3m56s   1GB
Jul 18 03:30:37 Starting compiler/backend/reg_alloc/proofs
Jul 18 03:30:39 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Jul 18 03:30:39 Starting compiler/backend/proofs
Jul 18 03:31:41 Finished compiler/backend/proofs                               1m02s   3GB
Jul 18 03:31:41 Starting compiler/backend/serialiser
Jul 18 03:31:44 Finished compiler/backend/serialiser                              2s  28MB
Jul 18 03:31:44 Starting compiler/encoders/x64/proofs
Jul 18 03:41:35 Finished compiler/encoders/x64/proofs                          9m50s   4GB
Jul 18 03:41:35 Starting compiler/encoders/arm7/proofs
Jul 18 03:55:28 Finished compiler/encoders/arm7/proofs                        13m52s   3GB
Jul 18 03:55:28 Starting compiler/encoders/arm8/proofs
Jul 18 04:02:35 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Jul 18 04:02:35 Starting compiler/encoders/arm8_asl/proofs
Jul 18 04:55:20 Finished compiler/encoders/arm8_asl/proofs                    52m45s   5GB
Jul 18 04:55:20 Starting compiler/encoders/mips/proofs
Jul 18 05:05:59 Finished compiler/encoders/mips/proofs                        10m38s   3GB
Jul 18 05:05:59 Starting compiler/encoders/riscv/proofs
Jul 18 05:14:56 Finished compiler/encoders/riscv/proofs                        8m57s   1GB
Jul 18 05:14:56 Starting compiler/encoders/ag32/proofs
Jul 18 05:17:31 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Jul 18 05:17:31 Starting compiler/backend/x64/proofs
Jul 18 05:18:03 Finished compiler/backend/x64/proofs                             31s   2GB
Jul 18 05:18:03 Starting compiler/backend/arm7/proofs
Jul 18 05:18:40 Finished compiler/backend/arm7/proofs                            37s   2GB
Jul 18 05:18:41 Starting compiler/backend/arm8/proofs
Jul 18 05:19:15 Finished compiler/backend/arm8/proofs                            34s   2GB
Jul 18 05:19:15 Starting compiler/backend/arm8_asl
Jul 18 05:19:40 Finished compiler/backend/arm8_asl                               24s   2GB
Jul 18 05:19:40 Starting compiler/backend/mips/proofs
Jul 18 05:20:14 Finished compiler/backend/mips/proofs                            33s   2GB
Jul 18 05:20:14 Starting compiler/backend/riscv/proofs
Jul 18 05:20:51 Finished compiler/backend/riscv/proofs                           37s   2GB
Jul 18 05:20:52 Starting compiler/backend/ag32/proofs
Jul 18 05:35:22 Finished compiler/backend/ag32/proofs                         14m30s   4GB
Jul 18 05:35:22 Starting compiler/backend/cv_compute
Jul 18 05:36:46 Finished compiler/backend/cv_compute                           1m23s   2GB
Jul 18 05:36:46 Starting cv_translator
Jul 18 05:57:35 Finished cv_translator                                        20m48s   7GB
Jul 18 05:57:35 Starting candle/set-theory
Jul 18 05:58:19 Finished candle/set-theory                                       43s   1GB
Jul 18 05:58:19 Starting candle/syntax-lib
Jul 18 05:58:20 Finished candle/syntax-lib                                        1s  25MB
Jul 18 05:58:20 Starting candle/standard/syntax
Jul 18 05:58:33 Finished candle/standard/syntax                                  12s 793MB
Jul 18 05:58:33 Starting candle/standard/semantics
Jul 18 06:00:41 Finished candle/standard/semantics                             2m07s   1GB
Jul 18 06:00:41 Starting candle/standard/monadic
Jul 18 06:00:43 Finished candle/standard/monadic                                  1s  21MB
Jul 18 06:00:43 Starting candle/standard/ml_kernel
Jul 18 06:02:25 Finished candle/standard/ml_kernel                             1m42s   3GB
Jul 18 06:02:26 Starting candle/overloading/syntax
Jul 18 06:06:03 Finished candle/overloading/syntax                             3m37s   1GB
Jul 18 06:06:03 Starting candle/overloading/semantics
Jul 18 06:18:34 Finished candle/overloading/semantics                         12m30s   2GB
Jul 18 06:18:34 Starting candle/overloading/monadic
Jul 18 06:21:24 Finished candle/overloading/monadic                            2m50s   1GB
Jul 18 06:21:24 Starting candle/overloading/ml_kernel
Jul 18 06:29:25 Finished candle/overloading/ml_kernel                          8m00s   3GB
Jul 18 06:29:25 Starting candle/overloading/ml_checker
Jul 18 06:32:04 Finished candle/overloading/ml_checker                         2m39s   3GB
Jul 18 06:32:04 Starting candle/prover
Jul 18 06:42:14 Finished candle/prover                                        10m09s   2GB
Jul 18 06:42:14 Starting pancake
Jul 18 06:43:04 Finished pancake                                                 50s 992MB
Jul 18 06:43:05 Starting pancake/ffi
Jul 18 06:43:05 Finished pancake/ffi                                              0s  13MB
Jul 18 06:43:05 Starting pancake/semantics
Jul 18 06:45:50 Finished pancake/semantics                                     2m44s   1GB
Jul 18 06:45:50 Starting pancake/parser
Jul 18 06:46:20 Finished pancake/parser                                          30s   1GB
Jul 18 06:46:20 Starting pancake/proofs
Jul 18 07:21:29 Finished pancake/proofs                                       35m09s   4GB
Jul 18 07:21:29 Starting characteristic/examples
Jul 18 07:23:05 Finished characteristic/examples                               1m35s   3GB
Jul 18 07:23:05 Starting tutorial/solutions
Jul 18 07:25:44 Finished tutorial/solutions                                    2m39s   3GB
Jul 18 07:25:45 Starting translator/monadic/examples
Jul 18 07:30:06 Finished translator/monadic/examples                           4m21s   3GB
Jul 18 07:30:06 Starting examples
Jul 18 07:46:15 Finished examples                                             16m08s   4GB
Jul 18 07:46:15 Starting examples/compilation/x64
Jul 18 07:54:56 Finished examples/compilation/x64                              8m40s   5GB
Jul 18 07:54:56 Starting examples/compilation/x64/proofs
Jul 18 07:57:52 Finished examples/compilation/x64/proofs                       2m55s   5GB
Jul 18 07:57:52 Starting examples/compilation/ag32
Jul 18 08:00:00 Finished examples/compilation/ag32                             2m08s   2GB
Jul 18 08:00:00 Starting examples/compilation/ag32/proofs
Jul 18 08:01:12 Finished examples/compilation/ag32/proofs                      1m11s   5GB
Jul 18 08:01:12 Starting examples/compilation/to_word
Jul 18 08:04:42 Finished examples/compilation/to_word                          3m30s   6GB
Jul 18 08:04:42 Starting examples/lpr_checker
Jul 18 08:05:54 Finished examples/lpr_checker                                  1m11s   1GB
Jul 18 08:05:55 Starting examples/lpr_checker/array
Jul 18 08:36:32 Finished examples/lpr_checker/array                           30m37s   9GB
Jul 18 08:36:32 Starting examples/lpr_checker/array/compilation
Jul 18 08:39:16 Finished examples/lpr_checker/array/compilation                2m43s   7GB
Jul 18 08:39:16 Starting examples/lpr_checker/array/compilation/proofs
Jul 18 08:40:34 Finished examples/lpr_checker/array/compilation/proofs         1m17s   6GB
Jul 18 08:40:34 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 18 08:41:47 Finished examples/lpr_checker/array/compilation/proofsARM8     1m13s   6GB
Jul 18 08:41:47 Starting examples/xlrup_checker
Jul 18 08:42:51 Finished examples/xlrup_checker                                1m03s   1GB
Jul 18 08:42:51 Starting examples/xlrup_checker/array
Jul 18 08:48:21 FAILED: examples/xlrup_checker/array
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/xlrup_checker[0m
Scanned 37 directories
Starting work on README.md
Starting work on xlrup_listTheory
README.md                                                                                                                                                                                                 (0s)     OK
xlrup_listTheory                                                                                                                                                                                         (57s)     OK
Starting work on xlrup_arrayProgTheory
xlrup_arrayProgTheory                                                                                                                                                                                   (263s)FAIL<1>
 Using CF specification w8array_substring_spec from theory Word8ArrayProof
 Post condition: POSTv sv. W8ARRAY csv cs * &STRING_TYPE (strlit (MAP (CHR  w2n) cs)) sv
 Using translator specification print_xor_string_v_thm from theory xlrup_arrayProg
 Saved theorem _______ "xor_to_string_spec"
 error in quse /home/cug/hk324/cml-regression/cakeml-2459/examples/xlrup_checker/array/xlrup_arrayProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-2459/examples/xlrup_checker/array/xlrup_arrayProgScript : Fail "Static Errors"
 Saved definition ____ "tn_to_string_def"
 /home/cug/hk324/cml-regression/cakeml-2459/examples/xlrup_checker/array/xlrup_arrayProgScript.sml:1049: error: Value or constructor (combine_rle_def) has not been declared
 Found near translate combine_rle_def
 Uncaught exception: Fail "Static Errors"