CakeML:821c40a8d7939d7e951e716a31cbb6e69cc8db13
Explain infix scheme
#695 (ocaml-infixes)
Merging into:dc73bd8f21601e06bdc92eb303865a3992673970
Merge pull request #694 from CakeML/remove-oom
HOL:4f67f38e1314dcb1488b3925ddbbc4bbd80795bf
Use new syntax for some theorems in examples/lambda/basics/term
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Building HOL
Starting developers
Finished developers 6s 74MB
Starting developers/bin
Finished developers/bin 13s 973MB
Starting semantics/ffi
Finished semantics/ffi 1m24s 643MB
Starting semantics
FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression/HOL-4f67f38e1314dcb1488b3925ddbbc4bbd80795bf/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-4f67f38e1314dcb1488b3925ddbbc4bbd80795bf/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Starting work on lprefix_lubTheory
lprefix_lubTheory real: 6s user: 5s OK
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1056/developers]0;Holmake: ~/regression/cakeml-1056/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1056/misc]0;Holmake: ~/regression/HOL-4f67f38e1314dcb1488b3925ddbbc4bbd80795bf/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-4f67f38e1314dcb1488b3925ddbbc4bbd80795bf/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory real: 2s user: 1s OK
set_sepTheory real: 8s user: 7s OK
Starting work on progTheory
progTheory real: 5s user: 5s OK
Starting work on addressTheory
Starting work on temporalTheory
temporalTheory real: 5s user: 5s OK
addressTheory real: 15s user: 14s OK
]0;Holmake: ~/regression/cakeml-1056/misc]0;Holmake: ~/regression/cakeml-1056/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1056/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1056/misc]0;Holmake: ~/regression/cakeml-1056/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on byteTheory
Starting work on README.md
README.md real: 0s user: 0s OK
byteTheory real: 6s user: 5s OK
Starting work on miscTheory
miscTheory real: 50s user: 47s OK
]0;Holmake: .]0;Holmake: ffi]0;Holmake: ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics[0m
Starting work on addancs
Starting work on fpSemScript
Starting work on README.md
fpSemScript real: 0s user: 0s OK
Starting work on fpSemTheory
README.md real: 0s user: 0s OK
addancs real: 0s user: 0s OK
Starting work on astScript
Starting work on namespaceScript
Starting work on tokensScript
astScript real: 0s user: 0s OK
namespaceScript real: 0s user: 0s OK
tokensScript real: 0s user: 0s OK
Starting work on namespaceTheory
Starting work on tokensTheory
namespaceTheory real: 4s user: 4s OK
fpSemTheory real: 6s user: 5s OK
Starting work on astTheory
tokensTheory real: 8s user: 7s OK
Starting work on gramTheory
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
astTheory real: 9s user: 8s OK
Starting work on semanticPrimitivesTheory
gramTheory real: 12s user: 10sFAIL<1>
Saved theorem _____ "datatype_MMLnonT"
Saved theorem _____ "MMLnonT_nchotomy"
Saved theorem _____ "MMLnonT_Axiom"
Saved theorem _____ "MMLnonT_induction"
Saved theorem _____ "MMLnonT_case_cong"
Saved theorem _____ "MMLnonT_case_eq"
<<HOL message: Defined type: "MMLnonT">>
error in quse /root/regression/cakeml-1056/semantics/gramScript.sml : HOL_ERR {message = "Can't handle form of antiquoted term {AlphaT \"div\"; AlphaT \"mod\"; StarT} \226\136\170 {SymbolT s | validMultSym s}", origin_function = "mk_grammar_def", origin_structure = "grammarLib"}
error in load gramScript : HOL_ERR {message = "Can't handle form of antiquoted term {AlphaT \"div\"; AlphaT \"mod\"; StarT} \226\136\170 {SymbolT s | validMultSym s}", origin_function = "mk_grammar_def", origin_structure = "grammarLib"}
Uncaught exception: HOL_ERR {message = "Can't handle form of antiquoted term {AlphaT \"div\"; AlphaT \"mod\"; StarT} \226\136\170 {SymbolT s | validMultSym s}", origin_function = "mk_grammar_def", origin_structure = "grammarLib"}
tokenUtilsTheory M-KILLED
lexer_funTheory M-KILLED
semanticPrimitivesTheory M-KILLED