Job 2065

CakeML:0bce440f6d4554db482cc8a868f63aa1d2484f79
  Remove readmePrefix dependency for subdirs in dandelion [Dec 08 15:13:42]
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:afad7a71de91823e350636ff17ada17e208032bf
  Fix Unicode violation in previous [Dec 06 00:49:44]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Dec 08 15:17:58 Claimed job
Dec 08 15:18:00 Reusing HOL
Dec 08 15:18:39 Starting developers
Dec 08 15:18:44 Finished developers                                               5s  97MB
Dec 08 15:18:45 Starting developers/bin
Dec 08 15:18:51 Finished developers/bin                                           5s   1GB
Dec 08 15:18:51 Starting floatingPoint/tools/dandelion
Dec 08 15:29:06 Finished floatingPoint/tools/dandelion                        10m15s   1GB
Dec 08 15:29:07 Starting floatingPoint/icing/
Dec 08 18:09:11 Finished floatingPoint/icing/                               2h40m03s  18GB
Dec 08 18:09:12 Starting floatingPoint/icing/examples
Dec 08 18:11:15 Finished floatingPoint/icing/examples                          2m03s   2GB
Dec 08 18:11:16 Starting floatingPoint/libmGen/
Dec 08 18:14:41 FAILED: floatingPoint/libmGen/
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)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(HOLDIR)/examples/algebra/lib[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/examples/algebra/monoid[0m
Scanning [1m$(HOLDIR)/examples/algebra/group[0m
Scanning [1m$(HOLDIR)/examples/algebra/ring[0m
Scanning [1m$(HOLDIR)/examples/algebra/field[0m
Scanning [1m$(HOLDIR)/examples/algebra/polynomial[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/dandelion[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 41 directories
Finished $(CAKEMLDIR)/floatingPoint/tools/flover/semantics                                                                                                                         (0.000s) 
Starting work on IEEE_reverseTheory
Starting work on FloVerToCakeMLTheory
Starting work on README.md
README.md                                                                                                                                                floatingPoint/libmGen  (0s)     OK
FloVerToCakeMLTheory                                                                                                                                     floatingPoint/libmGen (10s)     OK
IEEE_reverseTheory                                                                                                                                  floatingPoint/tools/flover(180s)     OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover [#theories: 1]                                                                                                                  (180.260s) 
Starting work on FloVerToCakeMLProofsTheory
FloVerToCakeMLProofsTheory                                                                                                                               floatingPoint/libmGen (19s)FAIL<1>
 error in quse /home/cug/hk324/cml-regression/cakeml-2065/floatingPoint/libmGen/FloVerToCakeMLProofsScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-2065/floatingPoint/libmGen/FloVerToCakeMLProofsScript : Fail "Static Errors"
 /home/cug/hk324/cml-regression/cakeml-2065/floatingPoint/libmGen/FloVerToCakeMLProofsScript.sml:11: error: Structure (floatToRealTheory) has not been declared
 Found near
   open floatToRealTheory FloVerToCakeMLTheory CakeMLtoFloVerProofsTheory
 /home/cug/hk324/cml-regression/cakeml-2065/floatingPoint/libmGen/FloVerToCakeMLProofsScript.sml:11: error: Structure (CakeMLtoFloVerProofsTheory) has not been declared
 Found near
   open floatToRealTheory FloVerToCakeMLTheory CakeMLtoFloVerProofsTheory
 Uncaught exception: Fail "Static Errors"