CakeML:d9f19ac9757f4f5fbdaf5055ed87a84c74ced52c
Fix typo in sollya filepath
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
Merge pull request #915 from CakeML/translator-fix
HOL:7a7ef58e684a9ee1a7fef81e009c2b3da204add1
Get examples/dev/inlineCompile to compile again
Machine:oven3
Claimed job
Reusing HOL
Starting developers
Finished developers 8s 121MB
Starting developers/bin
Finished developers/bin 13s 1GB
Starting floatingPoint/tools/dandelion
FAILED: floatingPoint/tools/dandelion
HOLORIG=/local/regression_new/cakeml-2070/floatingPoint/tools/dandelion tar -xf sollya-8.0.tar.gz sollya-8.0 &&\
cd sollya-8.0 &&\
#./configure &&\
#make &&\
rm -rf ./build-aux doc m4 tests-lib tests-tool &&\
rm -rf ./*.c ./*.h &&\
CURRDIR=$(pwd) &&\
FULLPATH="$CURRDIR/sollya"
cd ../
sed -i "s,FILLED_IN_BY_HOLPREEXEC,$FULLPATH,g" realZeroLib.sml
Scanning [1m$(HOLDIR)/examples/algebra/lib[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[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
Scanned 23 directories
Starting work on RealSimpsTheory
Starting work on ResultsTheory
Starting work on sqrtApproxTheory
Starting work on README.md
README.md floatingPoint/tools/dandelion (0s) OK
Starting work on moreRealTheory
ResultsTheory floatingPoint/tools/flover/Infra (14s) OK
Starting work on renameTheory
RealSimpsTheory floatingPoint/tools/flover/Infra (33s) OK
Starting work on MachineTypeTheory
renameTheory floatingPoint/tools/dandelion (30s) OK
Starting work on realPolyTheory
moreRealTheory floatingPoint/tools/dandelion (53s) OK
Starting work on sturmTheory
sqrtApproxTheory floatingPoint/tools/flover (55s) OK
realPolyTheory floatingPoint/tools/dandelion (38s) OK
Starting work on realPolyProofsTheory
Starting work on transcLangTheory
MachineTypeTheory floatingPoint/tools/flover/Infra (62s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover/Infra [#theories: 3] (109.623s)
Starting work on AbbrevsTheory
transcLangTheory floatingPoint/tools/dandelion (35s) OK
Starting work on checkerDefsTheory
realPolyProofsTheory floatingPoint/tools/dandelion (38s) OK
Starting work on mcLaurinApproxTheory
AbbrevsTheory floatingPoint/tools/flover/semantics (30s) OK
Starting work on ExpressionsTheory
sturmTheory floatingPoint/tools/dandelion (87s) OK
Starting work on drangTheory
checkerDefsTheory floatingPoint/tools/dandelion (31s) OK
Starting work on pointCheckerTheory
ExpressionsTheory floatingPoint/tools/flover/semantics (32s) OK
Starting work on FloverMapTheory
FloverMapTheory floatingPoint/tools/flover/semantics (14s) OK
Starting work on ExpressionAbbrevsTheory
drangTheory floatingPoint/tools/dandelion (36s) OK
Starting work on euclidDivTheory
pointCheckerTheory floatingPoint/tools/dandelion (29s) OK
Starting work on transcReflectTheory
ExpressionAbbrevsTheory floatingPoint/tools/flover/semantics (12s) OK
Starting work on ExpressionSemanticsTheory
euclidDivTheory floatingPoint/tools/dandelion (34s) OK
Starting work on sturmComputeTheory
transcReflectTheory floatingPoint/tools/dandelion (32s) OK
Starting work on pointCheckerProofsTheory
ExpressionSemanticsTheory floatingPoint/tools/flover/semantics (40s) OK
Starting work on CommandsTheory
sturmComputeTheory floatingPoint/tools/dandelion (30s) OK
Starting work on floverConnTheory
pointCheckerProofsTheory floatingPoint/tools/dandelion (29s) OK
mcLaurinApproxTheory floatingPoint/tools/dandelion(142s) OK
Starting work on approxPolyTheory
CommandsTheory floatingPoint/tools/flover/semantics (33s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover/semantics [#theories: 6] (165.006s)
Starting work on EnvironmentsTheory
Starting work on IntervalArithTheory
floverConnTheory floatingPoint/tools/dandelion (31s) OK
Starting work on TypeValidatorTheory
EnvironmentsTheory floatingPoint/tools/flover (33s) OK
Starting work on ErrorBoundsTheory
IntervalArithTheory floatingPoint/tools/flover (47s) OK
Starting work on ssaPrgsTheory
ssaPrgsTheory floatingPoint/tools/flover (15s) OK
approxPolyTheory floatingPoint/tools/dandelion (85s) OK
ErrorBoundsTheory floatingPoint/tools/flover (88s) OK
TypeValidatorTheory floatingPoint/tools/flover(138s) OK
Starting work on RealRangeArithTheory
RealRangeArithTheory floatingPoint/tools/flover (18s) OK
Starting work on IntervalValidationTheory
IntervalValidationTheory floatingPoint/tools/flover (63s) OK
Starting work on ErrorValidationTheory
Starting work on transcIntvSemTheory
transcIntvSemTheory floatingPoint/tools/dandelion (49s) OK
ErrorValidationTheory floatingPoint/tools/flover(180s) OK
Finished $(CAKEMLDIR)/floatingPoint/tools/flover [#theories: 9] (641.051s)
Starting work on approxCompErrTheory
approxCompErrTheory floatingPoint/tools/dandelion (58s) OK
Starting work on transcApproxSemTheory
transcApproxSemTheory floatingPoint/tools/dandelion (46s) OK
Starting work on checkerTheory
checkerTheory floatingPoint/tools/dandelion (42s) OK
Starting work on cosDeg3Theory
Starting work on sinDeg3Theory
sinDeg3Theory floatingPoint/tools/dandelion (33s)FAIL<1>
<<HOL message: Created theory "sinDeg3">>
Saved definition ____ "sin_example_def"
error in quse /local/regression_new/cakeml-2070/floatingPoint/tools/dandelion/sinDeg3Script.sml : ZeroLibErr ""
error in load /local/regression_new/cakeml-2070/floatingPoint/tools/dandelion/sinDeg3Script : ZeroLibErr ""
Testing sollya
Could not run Sollya at /local/regression_new/cakeml-2070/floatingPoint/tools/dandelion/sollya-8.0/sollya
Uncaught exception: ZeroLibErr ""
cosDeg3Theory floatingPoint/tools/dandelion (33s)MKILLED