CakeML:3204c37b5121d91837f3218fc3facf0353dec7b2
Fix merge detritus
#832 (errorpegs)
Merging into:a2713f8e8f8b719d4618f4be35c23419b5f4c348
Merge pull request #831 from CakeML/pancake
HOL:ef1d72d8d25c7691107eb1bf97d113b777f59997
Fix context-free selftest and add new failure examples
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Building HOL
Starting developers
Finished developers 7s 89MB
Starting developers/bin
Finished developers/bin 12s 1GB
Starting semantics/ffi
Finished semantics/ffi 24s 258MB
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 grammarTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory real: 1s user: 1s OK
Starting work on lem_listTheory
grammarTheory real: 6s user: 5s OK
Starting work on lem_list_extraTheory
lprefix_lubTheory real: 7s user: 6s OK
Starting work on lem_set_extraTheory
set_sepTheory real: 8s user: 7s OK
Starting work on progTheory
lem_set_extraTheory real: 0s user: 0s OK
Starting work on lem_stringTheory
lem_listTheory real: 6s user: 5s OK
Starting work on lem_string_extraTheory
lem_stringTheory real: 1s user: 0s OK
Starting work on byteTheory
lem_list_extraTheory real: 6s user: 5s OK
Starting work on README.md
README.md real: 0s user: 0s OK
Starting work on addancs
addancs real: 0s user: 0s OK
Starting work on astScript
astScript real: 0s user: 0s OK
Starting work on fpSemScript
fpSemScript real: 0s user: 0s OK
Starting work on fpSemTheory
progTheory real: 6s user: 5s OK
Starting work on addressTheory
lem_string_extraTheory real: 6s user: 5s OK
Starting work on namespaceScript
namespaceScript real: 0s user: 0s OK
Starting work on namespaceTheory
byteTheory real: 6s user: 5s OK
Starting work on tokensScript
tokensScript real: 0s user: 0s OK
Starting work on tokensTheory
namespaceTheory real: 5s user: 4s OK
fpSemTheory real: 6s user: 5s OK
Starting work on astTheory
addressTheory real: 12s user: 11s OK
Starting work on miscTheory
tokensTheory real: 11s user: 10s OK
Starting work on gramTheory
astTheory real: 22s user: 21s OK
Starting work on semanticPrimitivesTheory
gramTheory real: 22s user: 20s OK
miscTheory real: 53s user: 51s OK
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory real: 40s user: 37sFAIL<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 /root/regression/cakeml-1574/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 /root/regression/cakeml-1574/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 M-KILLED
lexer_funTheory M-KILLED