Job 2461

CakeML:16892fbea4d168094376f24a43c042f95496f967
  Make sure REPL has compiler configured to be fast [Jul 16 17:12:18]
#1015 (fix-repl)
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:pavlova

Jul 18 03:43:19 Claimed job
Jul 18 03:43:28 Reusing HOL
Jul 18 03:43:39 Starting developers
Jul 18 03:43:42 Finished developers                                               2s 222MB
Jul 18 03:43:43 Starting developers/bin
Jul 18 03:43:53 Finished developers/bin                                           9s   1GB
Jul 18 03:43:54 Starting compiler/proofs
Jul 18 05:37:01 Finished compiler/proofs                                    1h53m06s  31GB
Jul 18 05:37:02 Starting compiler/bootstrap/translation
Jul 18 13:59:24 Finished compiler/bootstrap/translation                     8h22m20s  55GB
Jul 18 13:59:25 Starting semantics/ffi
Jul 18 13:59:34 Finished semantics/ffi                                            8s 662MB
Jul 18 13:59:35 Starting semantics
Jul 18 13:59:36 Finished semantics                                                0s  68MB
Jul 18 13:59:37 Starting semantics/proofs
Jul 18 14:00:13 Finished semantics/proofs                                        35s   2GB
Jul 18 14:00:14 Starting semantics/alt_semantics
Jul 18 14:00:55 Finished semantics/alt_semantics                                 40s   1GB
Jul 18 14:00:56 Starting semantics/alt_semantics/proofs
Jul 18 14:12:02 Finished semantics/alt_semantics/proofs                       11m05s   3GB
Jul 18 14:12:03 Starting basis/pure
Jul 18 14:12:05 Finished basis/pure                                               0s  70MB
Jul 18 14:12:06 Starting translator
Jul 18 14:13:51 Finished translator                                            1m45s   4GB
Jul 18 14:13:52 Starting compiler/parsing
Jul 18 14:13:54 Finished compiler/parsing                                         0s  71MB
Jul 18 14:13:54 Starting characteristic
Jul 18 14:13:56 Finished characteristic                                           0s  89MB
Jul 18 14:13:57 Starting translator/monadic
Jul 18 14:13:58 Finished translator/monadic                                       0s  92MB
Jul 18 14:13:59 Starting basis
Jul 18 14:17:33 Finished basis                                                 3m32s   5GB
Jul 18 14:17:34 Starting compiler/inference
Jul 18 14:17:35 Finished compiler/inference                                       0s 100MB
Jul 18 14:17:36 Starting compiler/backend/reg_alloc
Jul 18 14:17:37 Finished compiler/backend/reg_alloc                               0s  69MB
Jul 18 14:17:38 Starting compiler/backend/gc
Jul 18 14:17:40 Finished compiler/backend/gc                                      0s 138MB
Jul 18 14:17:41 Starting compiler/backend
Jul 18 14:18:01 Finished compiler/backend                                        19s   1GB
Jul 18 14:18:02 Starting compiler/encoders/asm
Jul 18 14:18:03 Finished compiler/encoders/asm                                    0s  89MB
Jul 18 14:18:04 Starting compiler/encoders/x64
Jul 18 14:18:06 Finished compiler/encoders/x64                                    0s 101MB
Jul 18 14:18:06 Starting compiler/encoders/arm7
Jul 18 14:18:08 Finished compiler/encoders/arm7                                   0s 101MB
Jul 18 14:18:09 Starting compiler/encoders/arm8
Jul 18 14:18:10 Finished compiler/encoders/arm8                                   0s  93MB
Jul 18 14:18:11 Starting compiler/encoders/arm8_asl
Jul 18 14:20:24 Finished compiler/encoders/arm8_asl                            2m12s   1GB
Jul 18 14:20:25 Starting compiler/encoders/mips
Jul 18 14:20:26 Finished compiler/encoders/mips                                   0s 101MB
Jul 18 14:20:27 Starting compiler/encoders/riscv
Jul 18 14:20:29 Finished compiler/encoders/riscv                                  0s 101MB
Jul 18 14:20:30 Starting compiler/encoders/ag32
Jul 18 14:20:31 Finished compiler/encoders/ag32                                   0s  96MB
Jul 18 14:20:32 Starting compiler/backend/x64
Jul 18 14:20:34 Finished compiler/backend/x64                                     0s 135MB
Jul 18 14:20:35 Starting compiler/backend/arm7
Jul 18 14:20:36 Finished compiler/backend/arm7                                    0s 142MB
Jul 18 14:20:37 Starting compiler/backend/arm8
Jul 18 14:20:39 Finished compiler/backend/arm8                                    0s 135MB
Jul 18 14:20:40 Starting compiler/backend/mips
Jul 18 14:20:42 Finished compiler/backend/mips                                    0s 135MB
Jul 18 14:20:43 Starting compiler/backend/riscv
Jul 18 14:20:44 Finished compiler/backend/riscv                                   0s 135MB
Jul 18 14:20:45 Starting compiler/backend/ag32
Jul 18 14:22:09 Finished compiler/backend/ag32                                 1m22s   3GB
Jul 18 14:22:10 Starting compiler/parsing/proofs
Jul 18 14:22:11 Finished compiler/parsing/proofs                                  0s  73MB
Jul 18 14:22:12 Starting compiler/inference/proofs
Jul 18 14:22:14 Finished compiler/inference/proofs                                0s  91MB
Jul 18 14:22:15 Starting compiler/backend/semantics
Jul 18 14:26:04 Finished compiler/backend/semantics                            3m47s   3GB
Jul 18 14:26:04 Starting compiler/backend/reg_alloc/proofs
Jul 18 14:26:06 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jul 18 14:26:07 Starting compiler/backend/proofs
Jul 18 14:27:14 Finished compiler/backend/proofs                               1m05s   4GB
Jul 18 14:27:15 Starting compiler/backend/serialiser
Jul 18 14:27:16 Finished compiler/backend/serialiser                              0s 151MB
Jul 18 14:27:17 Starting compiler/encoders/x64/proofs
Jul 18 14:36:28 Finished compiler/encoders/x64/proofs                          9m09s   5GB
Jul 18 14:36:29 Starting compiler/encoders/arm7/proofs
Jul 18 14:49:22 Finished compiler/encoders/arm7/proofs                        12m52s  11GB
Jul 18 14:49:23 Starting compiler/encoders/arm8/proofs
Jul 18 14:55:44 Finished compiler/encoders/arm8/proofs                         6m19s   6GB
Jul 18 14:55:45 Starting compiler/encoders/arm8_asl/proofs
Jul 18 15:09:27 Finished compiler/encoders/arm8_asl/proofs                    13m41s   3GB
Jul 18 15:09:28 Starting compiler/encoders/mips/proofs
Jul 18 15:19:35 Finished compiler/encoders/mips/proofs                        10m05s   7GB
Jul 18 15:19:36 Starting compiler/encoders/riscv/proofs
Jul 18 15:27:42 Finished compiler/encoders/riscv/proofs                        8m05s   3GB
Jul 18 15:27:43 Starting compiler/encoders/ag32/proofs
Jul 18 15:30:09 Finished compiler/encoders/ag32/proofs                         2m25s   3GB
Jul 18 15:30:10 Starting compiler/backend/x64/proofs
Jul 18 15:30:53 Finished compiler/backend/x64/proofs                             41s   3GB
Jul 18 15:30:54 Starting compiler/backend/arm7/proofs
Jul 18 15:31:39 Finished compiler/backend/arm7/proofs                            44s   2GB
Jul 18 15:31:40 Starting compiler/backend/arm8/proofs
Jul 18 15:32:22 Finished compiler/backend/arm8/proofs                            40s   3GB
Jul 18 15:32:22 Starting compiler/backend/arm8_asl
Jul 18 15:32:50 Finished compiler/backend/arm8_asl                               26s   2GB
Jul 18 15:32:51 Starting compiler/backend/mips/proofs
Jul 18 15:33:37 Finished compiler/backend/mips/proofs                            45s   4GB
Jul 18 15:33:38 Starting compiler/backend/riscv/proofs
Jul 18 15:34:31 Finished compiler/backend/riscv/proofs                           51s   4GB
Jul 18 15:34:32 Starting compiler/backend/ag32/proofs
Jul 18 15:48:35 Finished compiler/backend/ag32/proofs                         14m01s   6GB
Jul 18 15:48:35 Starting compiler/backend/cv_compute
Jul 18 15:50:18 Finished compiler/backend/cv_compute                           1m41s   3GB
Jul 18 15:50:18 Starting cv_translator
Jul 18 16:09:40 Finished cv_translator                                        19m20s  14GB
Jul 18 16:09:41 Starting candle/set-theory
Jul 18 16:10:30 Finished candle/set-theory                                       47s   1GB
Jul 18 16:10:31 Starting candle/syntax-lib
Jul 18 16:10:32 Finished candle/syntax-lib                                        0s  72MB
Jul 18 16:10:33 Starting candle/standard/syntax
Jul 18 16:10:51 Finished candle/standard/syntax                                  17s   1GB
Jul 18 16:10:52 Starting candle/standard/semantics
Jul 18 16:13:28 Finished candle/standard/semantics                             2m35s   3GB
Jul 18 16:13:29 Starting candle/standard/monadic
Jul 18 16:13:31 Finished candle/standard/monadic                                  0s  98MB
Jul 18 16:13:32 Starting candle/standard/ml_kernel
Jul 18 16:15:28 Finished candle/standard/ml_kernel                             1m55s   5GB
Jul 18 16:15:29 Starting candle/overloading/syntax
Jul 18 16:19:02 Finished candle/overloading/syntax                             3m32s   4GB
Jul 18 16:19:03 Starting candle/overloading/semantics
Jul 18 16:30:36 Finished candle/overloading/semantics                         11m32s   6GB
Jul 18 16:30:37 Starting candle/overloading/monadic
Jul 18 16:33:17 Finished candle/overloading/monadic                            2m38s   2GB
Jul 18 16:33:18 Starting candle/overloading/ml_kernel
Jul 18 16:40:54 Finished candle/overloading/ml_kernel                          7m35s   6GB
Jul 18 16:40:55 Starting candle/overloading/ml_checker
Jul 18 16:43:31 Finished candle/overloading/ml_checker                         2m35s   7GB
Jul 18 16:43:32 Starting candle/prover
Jul 18 16:53:38 Finished candle/prover                                        10m04s   5GB
Jul 18 16:53:39 Starting pancake
Jul 18 16:54:46 Finished pancake                                               1m06s   1GB
Jul 18 16:54:47 Starting pancake/ffi
Jul 18 16:54:48 Finished pancake/ffi                                              0s  22MB
Jul 18 16:54:49 Starting pancake/semantics
Jul 18 16:57:38 Finished pancake/semantics                                     2m47s   3GB
Jul 18 16:57:39 Starting pancake/parser
Jul 18 16:58:12 Finished pancake/parser                                          32s   2GB
Jul 18 16:58:13 Starting pancake/proofs
Jul 18 17:29:36 Finished pancake/proofs                                       31m22s   9GB
Jul 18 17:29:37 Starting characteristic/examples
Jul 18 17:31:15 Finished characteristic/examples                               1m37s   6GB
Jul 18 17:31:16 Starting tutorial/solutions
Jul 18 17:33:50 Finished tutorial/solutions                                    2m33s   4GB
Jul 18 17:33:51 Starting translator/monadic/examples
Jul 18 17:37:46 Finished translator/monadic/examples                           3m54s   5GB
Jul 18 17:37:47 Starting examples
Jul 18 17:52:08 Finished examples                                             14m19s   8GB
Jul 18 17:52:09 Starting examples/compilation/x64
Jul 18 18:01:18 Finished examples/compilation/x64                              9m08s   7GB
Jul 18 18:01:19 Starting examples/compilation/x64/proofs
Jul 18 18:05:38 Finished examples/compilation/x64/proofs                       4m18s   9GB
Jul 18 18:05:39 Starting examples/compilation/ag32
Jul 18 18:08:17 Finished examples/compilation/ag32                             2m36s   5GB
Jul 18 18:08:17 Starting examples/compilation/ag32/proofs
Jul 18 18:10:04 Finished examples/compilation/ag32/proofs                      1m45s   8GB
Jul 18 18:10:05 Starting examples/compilation/to_word
Jul 18 18:14:01 Finished examples/compilation/to_word                          3m54s  12GB
Jul 18 18:14:02 Starting examples/lpr_checker
Jul 18 18:15:21 Finished examples/lpr_checker                                  1m18s   2GB
Jul 18 18:15:22 Starting examples/lpr_checker/array
Jul 18 18:43:57 Finished examples/lpr_checker/array                           28m34s  11GB
Jul 18 18:43:58 Starting examples/lpr_checker/array/compilation
Jul 18 18:46:24 Finished examples/lpr_checker/array/compilation                2m25s   9GB
Jul 18 18:46:25 Starting examples/lpr_checker/array/compilation/proofs
Jul 18 18:48:16 Finished examples/lpr_checker/array/compilation/proofs         1m49s   9GB
Jul 18 18:48:17 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 18 18:50:04 Finished examples/lpr_checker/array/compilation/proofsARM8     1m45s   8GB
Jul 18 18:50:04 Starting examples/xlrup_checker
Jul 18 18:51:17 Finished examples/xlrup_checker                                1m12s   1GB
Jul 18 18:51:18 Starting examples/xlrup_checker/array
Jul 18 18:56:33 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                                             (240s)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"
 Saved definition ____ "tn_to_string_def"
 /scratch/cakeml/regression/cakeml-2461/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
 error in quse /scratch/cakeml/regression/cakeml-2461/examples/xlrup_checker/array/xlrup_arrayProgScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-2461/examples/xlrup_checker/array/xlrup_arrayProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"