CakeML:ae3828093c420aaa931c0b6efc1e9be8be7e14bc
Ignore escaped newlines in string literals
#843 (newline-fix)
Merging into:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
Merge pull request #839 from CakeML/lpr_transform
HOL:56617180468ec5da8a1c0cfa582a16877f54a29b
Make Theorem/Definition syntax slightly more liberal
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 139MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 247MB
Starting semantics
FAILED: semantics
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/quotient/src[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$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Starting work on lem_listTheory
Starting work on lem_list_extraTheory
Starting work on lem_set_extraTheory
Starting work on lem_stringTheory
lem_set_extraTheory misc/lem_lib_stub (0s) OK
Starting work on lem_string_extraTheory
lem_stringTheory misc/lem_lib_stub (0s) OK
Starting work on byteTheory
lem_list_extraTheory misc/lem_lib_stub (2s) OK
Starting work on README.md
lem_listTheory misc/lem_lib_stub (2s) OK
Starting work on addancs
README.md semantics (0s) OK
Starting work on fpSemScript
addancs semantics (0s) OK
Starting work on astScript
lem_string_extraTheory misc/lem_lib_stub (2s) OK
Finished $(CAKEMLDIR)/misc/lem_lib_stub [#theories: 5] (7.247s)
Starting work on namespaceScript
byteTheory misc (2s) OK
Starting work on miscTheory
astScript semantics (2s) OK
Starting work on tokensScript
namespaceScript semantics (2s) OK
Starting work on namespaceTheory
fpSemScript semantics (3s) OK
Starting work on fpSemTheory
tokensScript semantics (2s) OK
Starting work on tokensTheory
namespaceTheory semantics (2s) OK
fpSemTheory semantics (2s) OK
Starting work on astTheory
tokensTheory semantics (4s) OK
Starting work on gramTheory
astTheory semantics (7s) OK
Starting work on semanticPrimitivesTheory
gramTheory semantics (9s) OK
miscTheory misc (26s) OK
Finished $(CAKEMLDIR)/misc [#theories: 2] (28.823s)
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory semantics (20s)FAIL<1>
Saved definition __ "enc_fp_cmp_def"
Saved definition __ "nat_to_v_def"
Saved definition __ "enc_op_def"
Exception raised at Parse_support.make_atom:
on line 972, characters 34-39:
Record field offset not registered
error in quse /home/cug/hk324/cml-regression/cakeml-1623/semantics/semanticPrimitivesScript.sml : HOL_ERR {message = "on line 972, characters 34-39:\nRecord field offset not registered", origin_function = "make_atom", origin_structure = "Parse_support"}
error in load /home/cug/hk324/cml-regression/cakeml-1623/semantics/semanticPrimitivesScript : HOL_ERR {message = "on line 972, characters 34-39:\nRecord field offset not registered", origin_function = "make_atom", origin_structure = "Parse_support"}
Uncaught exception: HOL_ERR {message = "on line 972, characters 34-39:\nRecord field offset not registered", origin_function = "make_atom", origin_structure = "Parse_support"}
tokenUtilsTheory semantics (8s)MKILLED
lexer_funTheory semantics (8s)MKILLED