Add sollya as a tool to the floating-point implementation for regress…

…ion testing

floatingPoint/tools/dandelion/Holmakefile

@@ -2,10 +2,18 @@ INCLUDES = $(HOLDIR)/examples/algebra/polynomial\
 	   $(CAKEMLDIR)/floatingPoint/tools/flover\
 	   $(CAKEMLDIR)/floatingPoint/tools/flover/semantics
 
-all: $(DEFAULT_TARGETS) README.md
+TARGETS = sollya $(DEFAULT_TARGETS) 
+
+all: $(TARGETS) README.md
 .PHONY: all
 
 README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+sollya:
+	cd ./sollya && Holmake
+.PHONY: sollya
+
+realPolyTheory.sml: sollya

floatingPoint/tools/dandelion/README.md

@@ -100,14 +100,18 @@ Some simple properties of polynomials on reals
 Definition of datatype for real-valued polynomials
 
 [realZeroLib.sml](realZeroLib.sml):
-Library automating Dandelion's certificate validation
+Library implementing the automatic computations
+done by Dandelion
 
 [renameScript.sml](renameScript.sml):
 renaming theory to unify naming of theorems
 
 [sinDeg3Script.sml](sinDeg3Script.sml):
 Simple approximation of sine of degree 3
 
+[sollya](sollya):
+The sollya tool from sollya.org to compute unverified guesses of Dandelion
+
 [sturmComputeScript.sml](sturmComputeScript.sml):
 Define a computable version of the sturm sequence and
 prove its equivalence with the non-computable version

floatingPoint/tools/dandelion/realZeroLib.sml

@@ -138,13 +138,13 @@ struct
     val sollyaInput = poly2Sollya polyAsString ("[" ^ cst2String lb ^"; " ^ cst2String ub ^"]")
     val fileStr = TextIO.openOut ("/tmp/sollya_input_"^Theory.current_theory()^".sollya")
     val _ = (TextIO.output (fileStr, sollyaInput); TextIO.closeOut fileStr)
-    val sollyaPath =
-        case Process.getEnv "SOLLYADIR" of
+    val sollyaPath = OS.FileSys.getDir() ^ "/sollya/sollya-8.0/sollya"
+        (* case Process.getEnv "SOLLYADIR" of
         SOME p => p ^ "/sollya"
         | NONE =>
           (let val (instr, outstr) = Unix.streamsOf(Unix.execute("/usr/bin/which", ["sollya"]))
           in TextIO.inputAll(instr) |> explode |> List.rev |> tl |> List.rev |> implode end)
-          handle SysErr _ => (print "Could not get path for Sollya\n"; "");
+          handle SysErr _ => (print "Could not get path for Sollya\n"; ""); *)
     val (instr, outStr) =
         (Unix.streamsOf(Unix.execute(sollyaPath, ["--warnonstderr",
                   "/tmp/sollya_input_"^Theory.current_theory()^".sollya"])))
@@ -357,13 +357,14 @@ struct
     val fileStr = TextIO.openOut ("/tmp/sollya_input.sollya")
     val _ = (TextIO.output (fileStr, sollyaInput); TextIO.closeOut fileStr)
     val _ = print "Testing sollya\n"
-    val sollyaPath =
+    val sollyaPath = OS.FileSys.getDir() ^ "/sollya/sollya-8.0/sollya"
+    (* val sollyaPath =
         case Process.getEnv "SOLLYADIR" of
         SOME p => p ^ "/sollya"
         | NONE =>
           (let val (instr, outstr) = Unix.streamsOf(Unix.execute("/usr/bin/which", ["sollya"]))
           in TextIO.inputAll(instr) |> explode |> List.rev |> tl |> List.rev |> implode end)
-          handle SysErr _ => (print "Could not get path for Sollya\n"; "");
+          handle SysErr _ => (print "Could not get path for Sollya\n"; ""); *)
     val (instr, outStr) =
         (Unix.streamsOf(Unix.execute(sollyaPath, ["--warnonstderr", "/tmp/sollya_input.sollya"])))
         handle SysErr _ => (print ("Could not run Sollya at "^sollyaPath ^ "\n"); raise ZeroLibErr "")

floatingPoint/tools/dandelion/sollya/Holmakefile

@@ -0,0 +1,16 @@
+SOLLYA_BIN = sollya/sollya-8.0/sollya
+
+$(SOLLYA_BIN):
+	tar -xf sollya-8.0.tar.gz &&\
+	cd sollya-8.0 &&\
+	./configure &&\
+	make &&\
+	export SOLLYADIR=./ &&\
+	cd ../
+
+realZeroLib.sm: $(SOLLYA_BIN)
+
+EXTRA_CLEANS = sollya-8.0/
+
+all: $(SOLLYA_BIN)
+.PHONY: all

floatingPoint/tools/dandelion/sollya/readmePrefix

@@ -0,0 +1 @@
+The sollya tool from sollya.org to compute unverified guesses of Dandelion