Fix some bugs in build process, move build earlier in sequence

developers/build-sequence

@@ -4,6 +4,14 @@
 developers
 developers/bin
 
+# Floating-Point optimizer & codegen
+floatingPoint/tools/dandelion
+floatingPoint/icing/
+floatingPoint/icing/examples
+
+# Floating-Point codegen
+floatingPoint/libmGen/
+
 # build many things in parallel at the start
 compiler/proofs
 compiler/bootstrap/translation
@@ -127,15 +135,6 @@ compiler/parsing/tests
 compiler/inference/tests
 compiler/printing/test
 
-# Floating-Point optimizer
-floatingPoint/tools/flover
-floatingPoint/icing/
-floatingPoint/icing/examples
-
-# Floating-Point codegen
-floatingPoint/tools/dandelion
-floatingPoint/libmGen/
-
 # compiler translation
 compiler/repl
 

floatingPoint/tools/dandelion/.hol_preexec

@@ -0,0 +1,8 @@
+tar -xf sollya-8.0.tar.gz sollya-8.0 &&\
+cd sollya-8.0 &&\
+cp ../../../icing/examples/output/Holmakefile ./ &&\
+./configure &&\
+make &&\
+rm -rf ./build-aux doc m4 tests-lib tests-tool &&\
+rm -rf ./*.c ./*.h &&\
+cd ../

floatingPoint/tools/dandelion/Holmakefile

@@ -10,19 +10,4 @@ DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
 
-sollya:
-	tar -xf sollya-8.0.tar.gz &&\
-	cd sollya-8.0 &&\
-	cp ../../../icing/examples/output/Holmakefile ./ &&\
-	echo "Dependency to generate unverified guesses" > README.md &&\
-	echo "Dependency to generate unverified guesses" > readmePrefix &&\
-	./configure &&\
-	make &&\
-	rm -rf ./build-aux doc m4 tests-lib tests-tool &&\
-	rm -rf ./*.c ./*.h &&\
-	cd ../
-.PHONY: sollya
-
-realPolyTheory.sml: sollya
-
-EXTRA_CLEANS = sollya-8.0/
+EXTRA_CLEANS = sollya-8.0/*

floatingPoint/tools/dandelion/realZeroLib.sml

@@ -138,7 +138,7 @@ 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 = OS.FileSys.getDir() ^ "/sollya/sollya-8.0/sollya"
+    val sollyaPath = OS.FileSys.getDir() ^ "/sollya-8.0/sollya"
         (* case Process.getEnv "SOLLYADIR" of
         SOME p => p ^ "/sollya"
         | NONE =>
@@ -357,7 +357,7 @@ struct
     val fileStr = TextIO.openOut ("/tmp/sollya_input.sollya")
     val _ = (TextIO.output (fileStr, sollyaInput); TextIO.closeOut fileStr)
     val _ = print "Testing sollya\n"
-    val sollyaPath = OS.FileSys.getDir() ^ "/sollya/sollya-8.0/sollya"
+    val sollyaPath = OS.FileSys.getDir() ^ "/sollya-8.0/sollya"
     (* val sollyaPath =
         case Process.getEnv "SOLLYADIR" of
         SOME p => p ^ "/sollya"