CakeML:11ce5f9be7a62a7a9d1e8fc232d385c48c16d833
Hook up decoder to bootstrap translation
#841 (eval)
Merging into:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
Merge pull request #839 from CakeML/lpr_transform
HOL:43aa237e8455efb9393a75bcbf2c720d7e5d39dc
Restore flat sum/pair sizes in TotalDefn.guessR
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 302MB
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 examples/machine-code/hoare-triple (0s) OK
Starting work on lem_listTheory
lprefix_lubTheory examples/fun-op-sem/lprefix_lub (3s) OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1] (3.060s)
Starting work on lem_list_extraTheory
grammarTheory examples/formal-languages/context-free (3s) OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1] (3.040s)
Starting work on lem_set_extraTheory
lem_set_extraTheory misc/lem_lib_stub (0s) OK
Starting work on lem_stringTheory
lem_stringTheory misc/lem_lib_stub (0s) OK
Starting work on lem_string_extraTheory
set_sepTheory examples/machine-code/hoare-triple (3s) OK
Starting work on progTheory
lem_listTheory misc/lem_lib_stub (3s) OK
Starting work on byteTheory
lem_list_extraTheory misc/lem_lib_stub (2s) OK
Starting work on addancs
addancs semantics (0s) OK
Starting work on astScript
astScript semantics (0s) OK
Starting work on fpSemTheory
progTheory examples/machine-code/hoare-triple (3s) OK
Starting work on addressTheory
byteTheory misc (2s) OK
Starting work on namespaceScript
namespaceScript semantics (0s) OK
Starting work on namespaceTheory
lem_string_extraTheory misc/lem_lib_stub (3s) OK
Finished $(CAKEMLDIR)/misc/lem_lib_stub [#theories: 5] (9.420s)
Starting work on tokensScript
tokensScript semantics (0s) OK
Starting work on tokensTheory
namespaceTheory semantics (2s) OK
fpSemTheory semantics (3s) OK
Starting work on astTheory
tokensTheory semantics (3s) OK
Starting work on gramTheory
addressTheory examples/machine-code/hoare-triple (6s) OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4] (13.610s)
Starting work on miscTheory
astTheory semantics (8s) OK
Starting work on semanticPrimitivesTheory
gramTheory semantics (9s) OK
miscTheory misc (27s) OK
Finished $(CAKEMLDIR)/misc [#theories: 2] (30.460s)
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory semantics (29s) OK
Starting work on evaluateTheory
Starting work on typeSystemTheory
evaluateTheory semantics (4s) OK
lexer_funTheory semantics (15s) OK
tokenUtilsTheory semantics (16s) OK
Starting work on cmlPtreeConversionTheory
typeSystemTheory semantics (14s) OK
Starting work on primTypesTheory
Starting work on terminationTheory
primTypesTheory semantics (3s) OK
terminationTheory semantics (11s) OK
cmlPtreeConversionTheory semantics (22s)FAIL<1>
between line 828, character 2 and line 1212, character 19:
at TotalDefn.defnDefine:
Unable to prove termination!
Try using "TotalDefn.tDefine <name> <quotation> <tac>".
error in quse /home/myreen/regression/cakeml-1607/semantics/cmlPtreeConversionScript.sml : HOL_ERR {message = "between line 828, character 2 and line 1212, character 19:\nat TotalDefn.defnDefine:\n\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "Define", origin_structure = "TotalDefn"}
error in load /home/myreen/regression/cakeml-1607/semantics/cmlPtreeConversionScript : HOL_ERR {message = "between line 828, character 2 and line 1212, character 19:\nat TotalDefn.defnDefine:\n\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "Define", origin_structure = "TotalDefn"}
Uncaught exception: HOL_ERR {message = "between line 828, character 2 and line 1212, character 19:\nat TotalDefn.defnDefine:\n\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "Define", origin_structure = "TotalDefn"}