Job 2522

CakeML:c61ffae7522febb39764768caec3eb99d9af977c
  Avoid storing decode_encode twice [Aug 02 16:37:11]
#1032 (new-double-ffi)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 03 09:30:46 Claimed job
Aug 03 09:30:48 Reusing HOL
Aug 03 09:31:33 Starting developers
Aug 03 09:31:39 Finished developers                                               5s  88MB
Aug 03 09:31:39 Starting developers/bin
Aug 03 09:31:45 Finished developers/bin                                           6s   1GB
Aug 03 09:31:45 Starting compiler/proofs
Aug 03 11:34:35 Finished compiler/proofs                                    2h02m49s  22GB
Aug 03 11:34:35 Starting compiler/bootstrap/translation
Aug 03 20:06:49 Finished compiler/bootstrap/translation                     8h32m13s  34GB
Aug 03 20:06:49 Starting semantics/ffi
Aug 03 20:06:55 Finished semantics/ffi                                            6s 221MB
Aug 03 20:06:56 Starting semantics
Aug 03 20:06:57 Finished semantics                                                1s  18MB
Aug 03 20:06:57 Starting semantics/proofs
Aug 03 20:07:31 Finished semantics/proofs                                        33s   1GB
Aug 03 20:07:31 Starting semantics/alt_semantics
Aug 03 20:08:04 Finished semantics/alt_semantics                                 32s 772MB
Aug 03 20:08:04 Starting semantics/alt_semantics/proofs
Aug 03 20:20:07 Finished semantics/alt_semantics/proofs                       12m02s   1GB
Aug 03 20:20:07 Starting basis/pure
Aug 03 20:20:08 Finished basis/pure                                               1s  21MB
Aug 03 20:20:08 Starting translator
Aug 03 20:22:02 Finished translator                                            1m53s   1GB
Aug 03 20:22:02 Starting compiler/parsing
Aug 03 20:22:04 Finished compiler/parsing                                         1s  21MB
Aug 03 20:22:04 Starting characteristic
Aug 03 20:22:06 Finished characteristic                                           1s  21MB
Aug 03 20:22:06 Starting translator/monadic
Aug 03 20:22:08 Finished translator/monadic                                       1s  20MB
Aug 03 20:22:08 Starting basis
Aug 03 20:23:17 FAILED: basis
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/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
Scanned 28 directories
Starting work on DoubleFFITheory
Starting work on HashtableProofTheory
Starting work on README.md
Starting work on UnsafeProgTheory
README.md                                                                                                   (0s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                 (0s)     OK
DoubleFFITheory                                                                                            (22s)     OK
Starting work on DoubleProofTheory
UnsafeProgTheory                                                                                           (45s)     OK
Starting work on UnsafeProofTheory
DoubleProofTheory                                                                                          (39s)FAIL<1>
 Saved definition ____ "DoubleIO_def"
 Saved theorem _______ "one_one_eq"
 Saved theorem _______ "MAP_CHR_w2n_n2w_ORD_id"
 Saved theorem _______ "into_bytes_len"
 Saved theorem _______ "concat_all_into_bytes_id"
 Saved definition ____ "string2Double_def"
 Saved theorem _______ "double_fromWord_spec"
 error in quse /home/cug/hk324/cml-regression/cakeml-2522/basis/DoubleProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/cug/hk324/cml-regression/cakeml-2522/basis/DoubleProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
HashtableProofTheory                                                                                       (64s)MKILLED
UnsafeProofTheory                                                                                          (17s)MKILLED