CakeML:a2713f8e8f8b719d4618f4be35c23419b5f4c348
Merge pull request #831 from CakeML/pancake
HOL:ef1d72d8d25c7691107eb1bf97d113b777f59997
Fix context-free selftest and add new failure examples
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 36MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 309MB
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: 0s 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: 3s OK
Starting work on lem_set_extraTheory
lem_set_extraTheory real: 0s user: 0s OK
Starting work on lem_stringTheory
lem_stringTheory real: 0s user: 0s OK
Starting work on lem_string_extraTheory
lem_listTheory real: 3s user: 2s OK
Starting work on byteTheory
set_sepTheory real: 4s user: 3s OK
Starting work on progTheory
lem_list_extraTheory real: 3s user: 2s OK
Starting work on addancs
addancs real: 0s user: 0s OK
Starting work on astScript
astScript real: 0s user: 0s OK
Starting work on fpSemTheory
byteTheory real: 3s user: 2s OK
Starting work on namespaceScript
namespaceScript real: 0s user: 0s OK
Starting work on namespaceTheory
progTheory real: 3s user: 2s OK
Starting work on addressTheory
lem_string_extraTheory real: 3s user: 3s 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: 3s OK
Starting work on astTheory
tokensTheory real: 4s user: 4s OK
Starting work on gramTheory
addressTheory real: 6s user: 6s OK
Starting work on miscTheory
astTheory real: 8s user: 8s OK
Starting work on semanticPrimitivesTheory
gramTheory real: 10s user: 10s OK
semanticPrimitivesTheory real: 21s user: 19sFAIL<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/myreen/regression/cakeml-1575/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/myreen/regression/cakeml-1575/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"}
miscTheory M-KILLED