CakeML:c36d82323bf7e92004229b5b0cccc16c57bf6428
Merge branch 'errorpegs' of github.com:CakeML/cakeml into errorpegs
#832 (errorpegs)
Merging into:a2713f8e8f8b719d4618f4be35c23419b5f4c348
Merge pull request #831 from CakeML/pancake
HOL:ef1d72d8d25c7691107eb1bf97d113b777f59997
Fix context-free selftest and add new failure examples
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 135MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 240MB
Starting semantics
FAILED: semantics
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Starting work on grammarTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory real: 1s user: 0s OK
Starting work on lem_listTheory
grammarTheory real: 3s user: 2s OK
Starting work on lem_list_extraTheory
lprefix_lubTheory real: 3s user: 2s OK
Starting work on lem_set_extraTheory
lem_set_extraTheory real: 0s user: 0s OK
Starting work on lem_stringTheory
set_sepTheory real: 4s user: 3s OK
Starting work on progTheory
lem_listTheory real: 3s user: 2s OK
Starting work on lem_string_extraTheory
lem_stringTheory real: 0s user: 0s OK
Starting work on byteTheory
lem_list_extraTheory real: 2s user: 2s 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
progTheory real: 2s user: 2s OK
Starting work on addressTheory
astScript real: 0s user: 0s OK
Starting work on fpSemScript
fpSemScript real: 0s user: 0s OK
Starting work on fpSemTheory
lem_string_extraTheory real: 3s user: 2s OK
Starting work on namespaceScript
namespaceScript real: 0s user: 0s OK
Starting work on namespaceTheory
byteTheory real: 2s user: 2s OK
Starting work on tokensScript
tokensScript real: 0s user: 0s OK
Starting work on tokensTheory
namespaceTheory real: 2s user: 2s OK
fpSemTheory real: 3s user: 2s OK
Starting work on astTheory
tokensTheory real: 4s user: 4s OK
Starting work on gramTheory
addressTheory real: 6s user: 5s OK
Starting work on miscTheory
astTheory real: 8s user: 8s OK
Starting work on semanticPrimitivesTheory
gramTheory real: 10s user: 9s OK
miscTheory real: 27s user: 26s OK
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory real: 21s user: 20sFAIL<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-1573/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-1573/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