CakeML Regression Test

Job 2465

CakeML: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 18 18:07:16 Claimed job
Jul 18 18:07:18 Reusing HOL
Jul 18 18:08:02 Starting developers
Jul 18 18:08:08 Finished developers                                               5s  83MB
Jul 18 18:08:08 Starting developers/bin
Jul 18 18:08:14 Finished developers/bin                                           5s   1GB
Jul 18 18:08:14 Starting compiler/proofs
Jul 18 20:10:01 Finished compiler/proofs                                    2h01m47s  17GB
Jul 18 20:10:02 Starting compiler/bootstrap/translation
Jul 19 05:06:30 Finished compiler/bootstrap/translation                     8h56m27s  48GB
Jul 19 05:06:30 Starting semantics/ffi
Jul 19 05:06:35 Finished semantics/ffi                                            5s 436MB
Jul 19 05:06:35 Starting semantics
Jul 19 05:06:36 Finished semantics                                                1s  18MB
Jul 19 05:06:36 Starting semantics/proofs
Jul 19 05:07:11 Finished semantics/proofs                                        34s 858MB
Jul 19 05:07:11 Starting semantics/alt_semantics
Jul 19 05:07:45 Finished semantics/alt_semantics                                 33s 690MB
Jul 19 05:07:45 Starting semantics/alt_semantics/proofs
Jul 19 05:19:49 Finished semantics/alt_semantics/proofs                       12m04s   2GB
Jul 19 05:19:49 Starting basis/pure
Jul 19 05:19:51 Finished basis/pure                                               1s  19MB
Jul 19 05:19:51 Starting translator
Jul 19 05:21:42 Finished translator                                            1m50s   2GB
Jul 19 05:21:42 Starting compiler/parsing
Jul 19 05:21:43 Finished compiler/parsing                                         1s  22MB
Jul 19 05:21:43 Starting characteristic
Jul 19 05:21:46 Finished characteristic                                           1s  26MB
Jul 19 05:21:46 Starting translator/monadic
Jul 19 05:21:48 Finished translator/monadic                                       1s  21MB
Jul 19 05:21:48 Starting basis
Jul 19 05:25:31 Finished basis                                                 3m43s   3GB
Jul 19 05:25:31 Starting compiler/inference
Jul 19 05:25:33 Finished compiler/inference                                       1s  19MB
Jul 19 05:25:33 Starting compiler/backend/reg_alloc
Jul 19 05:25:35 Finished compiler/backend/reg_alloc                               1s  22MB
Jul 19 05:25:35 Starting compiler/backend/gc
Jul 19 05:25:37 Finished compiler/backend/gc                                      2s  28MB
Jul 19 05:25:37 Starting compiler/backend
Jul 19 05:25:52 Finished compiler/backend                                        14s 815MB
Jul 19 05:25:52 Starting compiler/encoders/asm
Jul 19 05:25:54 Finished compiler/encoders/asm                                    1s  23MB
Jul 19 05:25:54 Starting compiler/encoders/x64
Jul 19 05:25:56 Finished compiler/encoders/x64                                    1s  28MB
Jul 19 05:25:56 Starting compiler/encoders/arm7
Jul 19 05:25:58 Finished compiler/encoders/arm7                                   1s  22MB
Jul 19 05:25:58 Starting compiler/encoders/arm8
Jul 19 05:26:00 Finished compiler/encoders/arm8                                   1s  23MB
Jul 19 05:26:00 Starting compiler/encoders/arm8_asl
Jul 19 05:29:17 Finished compiler/encoders/arm8_asl                            3m16s   1GB
Jul 19 05:29:17 Starting compiler/encoders/mips
Jul 19 05:29:19 Finished compiler/encoders/mips                                   1s  28MB
Jul 19 05:29:19 Starting compiler/encoders/riscv
Jul 19 05:29:21 Finished compiler/encoders/riscv                                  1s  25MB
Jul 19 05:29:21 Starting compiler/encoders/ag32
Jul 19 05:29:23 Finished compiler/encoders/ag32                                   1s  21MB
Jul 19 05:29:23 Starting compiler/backend/x64
Jul 19 05:29:25 Finished compiler/backend/x64                                     2s  27MB
Jul 19 05:29:25 Starting compiler/backend/arm7
Jul 19 05:29:28 Finished compiler/backend/arm7                                    2s  26MB
Jul 19 05:29:28 Starting compiler/backend/arm8
Jul 19 05:29:30 Finished compiler/backend/arm8                                    2s  24MB
Jul 19 05:29:30 Starting compiler/backend/mips
Jul 19 05:29:33 Finished compiler/backend/mips                                    2s  27MB
Jul 19 05:29:33 Starting compiler/backend/riscv
Jul 19 05:29:35 Finished compiler/backend/riscv                                   2s  27MB
Jul 19 05:29:35 Starting compiler/backend/ag32
Jul 19 05:31:03 Finished compiler/backend/ag32                                 1m27s   1GB
Jul 19 05:31:03 Starting compiler/parsing/proofs
Jul 19 05:31:05 Finished compiler/parsing/proofs                                  1s  22MB
Jul 19 05:31:05 Starting compiler/inference/proofs
Jul 19 05:31:07 Finished compiler/inference/proofs                                1s  21MB
Jul 19 05:31:07 Starting compiler/backend/semantics
Jul 19 05:35:03 Finished compiler/backend/semantics                            3m56s   1GB
Jul 19 05:35:03 Starting compiler/backend/reg_alloc/proofs
Jul 19 05:35:05 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Jul 19 05:35:05 Starting compiler/backend/proofs
Jul 19 05:36:08 Finished compiler/backend/proofs                               1m02s   2GB
Jul 19 05:36:08 Starting compiler/backend/serialiser
Jul 19 05:36:10 Finished compiler/backend/serialiser                              2s  28MB
Jul 19 05:36:11 Starting compiler/encoders/x64/proofs
Jul 19 05:46:01 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Jul 19 05:46:02 Starting compiler/encoders/arm7/proofs
Jul 19 05:59:54 Finished compiler/encoders/arm7/proofs                        13m52s   3GB
Jul 19 05:59:54 Starting compiler/encoders/arm8/proofs
Jul 19 06:06:51 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Jul 19 06:06:52 Starting compiler/encoders/arm8_asl/proofs
Jul 19 06:22:41 Finished compiler/encoders/arm8_asl/proofs                    15m49s   2GB
Jul 19 06:22:42 Starting compiler/encoders/mips/proofs
Jul 19 06:33:19 Finished compiler/encoders/mips/proofs                        10m37s   2GB
Jul 19 06:33:19 Starting compiler/encoders/riscv/proofs
Jul 19 06:42:09 Finished compiler/encoders/riscv/proofs                        8m49s   2GB
Jul 19 06:42:09 Starting compiler/encoders/ag32/proofs
Jul 19 06:44:43 Finished compiler/encoders/ag32/proofs                         2m33s   1GB
Jul 19 06:44:43 Starting compiler/backend/x64/proofs
Jul 19 06:45:16 Finished compiler/backend/x64/proofs                             32s   1GB
Jul 19 06:45:16 Starting compiler/backend/arm7/proofs
Jul 19 06:45:52 Finished compiler/backend/arm7/proofs                            36s   2GB
Jul 19 06:45:52 Starting compiler/backend/arm8/proofs
Jul 19 06:46:25 Finished compiler/backend/arm8/proofs                            32s   1GB
Jul 19 06:46:25 Starting compiler/backend/arm8_asl
Jul 19 06:46:50 Finished compiler/backend/arm8_asl                               25s   2GB
Jul 19 06:46:50 Starting compiler/backend/mips/proofs
Jul 19 06:47:24 Finished compiler/backend/mips/proofs                            33s   2GB
Jul 19 06:47:24 Starting compiler/backend/riscv/proofs
Jul 19 06:48:01 Finished compiler/backend/riscv/proofs                           36s   3GB
Jul 19 06:48:01 Starting compiler/backend/ag32/proofs
Jul 19 07:02:36 Finished compiler/backend/ag32/proofs                         14m34s   4GB
Jul 19 07:02:36 Starting compiler/backend/cv_compute
Jul 19 07:03:55 Finished compiler/backend/cv_compute                           1m19s   2GB
Jul 19 07:03:56 Starting cv_translator
Jul 19 07:24:21 Finished cv_translator                                        20m25s   8GB
Jul 19 07:24:21 Starting candle/set-theory
Jul 19 07:25:05 Finished candle/set-theory                                       42s   1GB
Jul 19 07:25:05 Starting candle/syntax-lib
Jul 19 07:25:06 Finished candle/syntax-lib                                        1s  20MB
Jul 19 07:25:06 Starting candle/standard/syntax
Jul 19 07:25:19 Finished candle/standard/syntax                                  12s 793MB
Jul 19 07:25:19 Starting candle/standard/semantics
Jul 19 07:27:27 Finished candle/standard/semantics                             2m08s   1GB
Jul 19 07:27:27 Starting candle/standard/monadic
Jul 19 07:27:29 Finished candle/standard/monadic                                  1s  22MB
Jul 19 07:27:30 Starting candle/standard/ml_kernel
Jul 19 07:29:15 Finished candle/standard/ml_kernel                             1m45s   3GB
Jul 19 07:29:15 Starting candle/overloading/syntax
Jul 19 07:32:49 Finished candle/overloading/syntax                             3m33s   1GB
Jul 19 07:32:49 Starting candle/overloading/semantics
Jul 19 07:45:18 Finished candle/overloading/semantics                         12m29s   3GB
Jul 19 07:45:18 Starting candle/overloading/monadic
Jul 19 07:48:09 Finished candle/overloading/monadic                            2m50s   1GB
Jul 19 07:48:09 Starting candle/overloading/ml_kernel
Jul 19 07:56:14 Finished candle/overloading/ml_kernel                          8m05s   3GB
Jul 19 07:56:15 Starting candle/overloading/ml_checker
Jul 19 07:58:55 Finished candle/overloading/ml_checker                         2m40s   3GB
Jul 19 07:58:55 Starting candle/prover
Jul 19 08:09:03 Finished candle/prover                                        10m07s   3GB
Jul 19 08:09:04 Starting pancake
Jul 19 08:09:55 Finished pancake                                                 51s   1GB
Jul 19 08:09:56 Starting pancake/ffi
Jul 19 08:09:56 Finished pancake/ffi                                              0s  13MB
Jul 19 08:09:56 Starting pancake/semantics
Jul 19 08:12:58 Finished pancake/semantics                                     3m01s   1GB
Jul 19 08:12:58 Starting pancake/parser
Jul 19 08:13:28 Finished pancake/parser                                          29s   1GB
Jul 19 08:13:28 Starting pancake/proofs
Jul 19 08:48:25 Finished pancake/proofs                                       34m57s   5GB
Jul 19 08:48:25 Starting characteristic/examples
Jul 19 08:50:01 Finished characteristic/examples                               1m35s   3GB
Jul 19 08:50:02 Starting tutorial/solutions
Jul 19 08:52:39 Finished tutorial/solutions                                    2m37s   3GB
Jul 19 08:52:39 Starting translator/monadic/examples
Jul 19 08:56:59 Finished translator/monadic/examples                           4m19s   2GB
Jul 19 08:56:59 Starting examples
Jul 19 09:13:03 Finished examples                                             16m04s   5GB
Jul 19 09:13:03 Starting examples/compilation/x64
Jul 19 09:21:44 Finished examples/compilation/x64                              8m40s   5GB
Jul 19 09:21:44 Starting examples/compilation/x64/proofs
Jul 19 09:24:38 Finished examples/compilation/x64/proofs                       2m54s   4GB
Jul 19 09:24:38 Starting examples/compilation/ag32
Jul 19 09:26:49 Finished examples/compilation/ag32                             2m10s   3GB
Jul 19 09:26:50 Starting examples/compilation/ag32/proofs
Jul 19 09:28:02 Finished examples/compilation/ag32/proofs                      1m12s   5GB
Jul 19 09:28:02 Starting examples/compilation/to_word
Jul 19 09:31:34 Finished examples/compilation/to_word                          3m31s   6GB
Jul 19 09:31:34 Starting examples/lpr_checker
Jul 19 09:32:45 Finished examples/lpr_checker                                  1m10s   1GB
Jul 19 09:32:45 Starting examples/lpr_checker/array
Jul 19 10:03:05 Finished examples/lpr_checker/array                           30m19s   8GB
Jul 19 10:03:05 Starting examples/lpr_checker/array/compilation
Jul 19 10:05:46 Finished examples/lpr_checker/array/compilation                2m40s   8GB
Jul 19 10:05:46 Starting examples/lpr_checker/array/compilation/proofs
Jul 19 10:07:05 Finished examples/lpr_checker/array/compilation/proofs         1m19s   6GB
Jul 19 10:07:05 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 19 10:08:19 Finished examples/lpr_checker/array/compilation/proofsARM8     1m13s   6GB
Jul 19 10:08:19 Starting examples/xlrup_checker
Jul 19 10:09:22 Finished examples/xlrup_checker                                1m03s   1GB
Jul 19 10:09:22 Starting examples/xlrup_checker/array
Jul 19 10:14:50 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                                                                                                                                                                                   (260s)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-2465/examples/xlrup_checker/array/xlrup_arrayProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-2465/examples/xlrup_checker/array/xlrup_arrayProgScript : Fail "Static Errors"
 Saved definition ____ "tn_to_string_def"
 /home/cug/hk324/cml-regression/cakeml-2465/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"