CakeML Regression Test

Job 2066

CakeML:66344cbdf6ddefc00f57fc31549a438871574945
  Merge branch 'libm_gen' of github.com:CakeML/cakeml into libm_gen [Dec 09 07:42:22]
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:7a7ef58e684a9ee1a7fef81e009c2b3da204add1
  Get examples/dev/inlineCompile to compile again [Dec 08 04:15:59]
Machine:oven3

Dec 09 07:43:27 Claimed job
Dec 09 07:43:36 Building HOL
Dec 09 08:06:41 Starting developers
Dec 09 08:06:50 Finished developers                                               9s 130MB
Dec 09 08:06:51 Starting developers/bin
Dec 09 08:07:05 Finished developers/bin                                          14s   1GB
Dec 09 08:07:06 Starting floatingPoint/tools/dandelion
Dec 09 08:28:12 Finished floatingPoint/tools/dandelion                        21m06s   1GB
Dec 09 08:28:12 Starting floatingPoint/icing/
Dec 09 13:58:41 Finished floatingPoint/icing/                               5h30m27s  12GB
Dec 09 13:58:41 Starting floatingPoint/icing/examples
Dec 09 14:01:57 Finished floatingPoint/icing/examples                          3m15s   3GB
Dec 09 14:01:57 Starting floatingPoint/libmGen/
Dec 09 14:17:30 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$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[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)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/icing[0m
Scanning [1m$(HOLDIR)/examples/algebra/lib[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/dandelion[0m
Scanned 91 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 (22s)     OK
IEEE_reverseTheory                                                                                                                                                        floatingPoint/tools/flover(435s)     OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover [#theories: 1]                                                                                                                                        (435.680s) 
Starting work on FloVerToCakeMLProofsTheory
FloVerToCakeMLProofsTheory                                                                                                                                                     floatingPoint/libmGen (91s)     OK
Starting work on libmTheory
libmTheory                                                                                                                                                                     floatingPoint/libmGen(227s)     OK
Starting work on atnDeg3Theory
atnDeg3Theory                                                                                                                                                                  floatingPoint/libmGen(139s)FAIL<1>
 Loading translation: basisProg ... done.
 <<HOL message: Created theory "atnDeg3">>
 Saved definition ____ "cos_example_def"
 error in quse /local/regression_new/cakeml-2066/floatingPoint/libmGen/atnDeg3Script.sml : ZeroLibErr ""
 error in load /local/regression_new/cakeml-2066/floatingPoint/libmGen/atnDeg3Script : ZeroLibErr ""
 Testing sollya
 Could not run Sollya at /local/regression_new/cakeml-2066/floatingPoint/libmGen/sollya-8.0/sollya
 Uncaught exception: ZeroLibErr ""
Finished $(CAKEMLDIR)/floatingPoint/libmGen [#theories: 3; #fails: 1]                                                                                                                                  (481.243s)