Job 1678

CakeML:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
  Merge pull request #847 from CakeML/clos-smart-op [Nov 30 09:57:02]
HOL:4b673e6c8e4280f7a402e1de13be1b8d71a052e1
  Change iterate's _ .. _ notation to { _ .. _ } [Dec 07 05:44:32]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 08 22:21:53 Claimed job
Dec 08 22:22:00 Building HOL
Dec 08 22:32:11 Starting developers
Dec 08 22:32:16 Finished developers                                               4s 130MB
Dec 08 22:32:16 Starting developers/bin
Dec 08 22:32:23 Finished developers/bin                                           6s   1GB
Dec 08 22:32:23 Starting semantics/ffi
Dec 08 22:32:32 Finished semantics/ffi                                            8s 213MB
Dec 08 22:32:32 Starting semantics
Dec 08 22:32:54 FAILED: semantics
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
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
Scanning $(CAKEMLDIR)/semantics/ffi
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  (3s)     OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1]      (3.267s) 
Starting work on README.md
set_sepTheory                   examples/machine-code/hoare-triple  (3s)     OK
Starting work on progTheory
README.md                                                semantics  (0s)     OK
Starting work on fpSemTheory
byteTheory                                                    misc  (2s)     OK
Starting work on namespaceTheory
grammarTheory               examples/formal-languages/context-free  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 2] (4.417s) 
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.634s) 
Starting work on miscTheory
astTheory                                                semantics  (9s)     OK
Starting work on semanticPrimitivesTheory
miscTheory                                                    misc  (5s)FAIL<1>
 error in quse /home/cake/oven/regression/cakeml-1678/misc/miscScript.sml : HOL_ERR {message = "\"exp\" not found in theory \"transc\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 error in load /home/cake/oven/regression/cakeml-1678/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