From 623518ee1f3450e99fc3f11f115f9055b127907b Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Thu, 8 Dec 2022 12:05:35 +0100
Subject: [PATCH] Fix some bugs in build process, move build earlier in
 sequence

---
 developers/build-sequence                     | 17 ++++++++---------
 floatingPoint/tools/dandelion/.hol_preexec    |  8 ++++++++
 floatingPoint/tools/dandelion/Holmakefile     | 17 +----------------
 floatingPoint/tools/dandelion/realZeroLib.sml |  4 ++--
 4 files changed, 19 insertions(+), 27 deletions(-)
 create mode 100644 floatingPoint/tools/dandelion/.hol_preexec

diff --git a/developers/build-sequence b/developers/build-sequence
index 12039ab295..b98c8f9858 100644
--- a/developers/build-sequence
+++ b/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
 
diff --git a/floatingPoint/tools/dandelion/.hol_preexec b/floatingPoint/tools/dandelion/.hol_preexec
new file mode 100644
index 0000000000..cb8d4ee93f
--- /dev/null
+++ b/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 ../
diff --git a/floatingPoint/tools/dandelion/Holmakefile b/floatingPoint/tools/dandelion/Holmakefile
index b7728edef6..db4704fe24 100644
--- a/floatingPoint/tools/dandelion/Holmakefile
+++ b/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/*
diff --git a/floatingPoint/tools/dandelion/realZeroLib.sml b/floatingPoint/tools/dandelion/realZeroLib.sml
index 6c4bd07cd8..dd799e9b48 100644
--- a/floatingPoint/tools/dandelion/realZeroLib.sml
+++ b/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"