CakeML:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
Merge pull request #847 from CakeML/clos-smart-op
HOL:86eeab3f584f296e0bb80aaadfd332b3ec1f8af8
Avoid register_frag calls for every invocation of ARITH_DP_FILTER_ss
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 132MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 8s 222MB
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Starting work on locationTheory
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 byteTheory
locationTheory examples/formal-languages/context-free (1s) OK
Starting work on grammarTheory
lprefix_lubTheory examples/fun-op-sem/lprefix_lub (2s) OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1] (2.930s)
Starting work on README.md
README.md semantics (0s) OK
Starting work on fpSemTheory
byteTheory misc (2s) OK
Starting work on namespaceTheory
set_sepTheory examples/machine-code/hoare-triple (3s) OK
Starting work on progTheory
grammarTheory examples/formal-languages/context-free (2s) OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 2] (4.081s)
Starting work on tokensTheory
namespaceTheory semantics (2s) OK
progTheory examples/machine-code/hoare-triple (2s) OK
Starting work on addressTheory
fpSemTheory semantics (2s) OK
Starting work on astTheory
tokensTheory semantics (4s) OK
Starting work on gramTheory
addressTheory examples/machine-code/hoare-triple (5s) OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4] (12.197s)
Starting work on miscTheory
astTheory semantics (8s) OK
Starting work on semanticPrimitivesTheory
miscTheory misc (5s)FAIL<1>
error in quse /home/cug/hk324/cml-regression/cakeml-1677/misc/miscScript.sml : HOL_ERR {message = "\"exp\" not found in theory \"transc\"", origin_function = "prim_mk_const", origin_structure = "Term"}
error in load /home/cug/hk324/cml-regression/cakeml-1677/misc/miscScript : HOL_ERR {message = "\"exp\" not found in theory \"transc\"", origin_function = "prim_mk_const", origin_structure = "Term"}
<<HOL message: Created theory "misc">>
Uncaught exception: HOL_ERR {message = "\"exp\" not found in theory \"transc\"", origin_function = "prim_mk_const", origin_structure = "Term"}
gramTheory semantics (9s)MKILLED
semanticPrimitivesTheory semantics (3s)MKILLED