From 2b773439ca57da44c85f3000b96203aea02782ae Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Wed, 24 Apr 2024 15:55:42 +0100 Subject: [PATCH 1/3] cvc5 not finding static libraries --- .gitmodules | 6 ++++++ dune | 22 ++++++++++++++++++---- vendor/cadical | 1 + vendor/libpoly | 1 + 4 files changed, 26 insertions(+), 4 deletions(-) create mode 160000 vendor/cadical create mode 160000 vendor/libpoly diff --git a/.gitmodules b/.gitmodules index ed2feeb..9df9db0 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,9 @@ [submodule "vendor/cvc5"] path = vendor/cvc5 url = https://github.com/cvc5/cvc5 +[submodule "vendor/cadical"] + path = vendor/cadical + url = https://github.com/arminbiere/cadical.git +[submodule "vendor/libpoly"] + path = vendor/libpoly + url = https://github.com/SRI-CSL/libpoly.git diff --git a/dune b/dune index 9b73b80..2684a5c 100644 --- a/dune +++ b/dune @@ -5,15 +5,29 @@ (action (no-infer (progn + (chdir + vendor/cadical + (progn + (run ./configure) + (run make -j 4))) + (copy vendor/cadical/build/libcadical.a libcadical.a) + (chdir + vendor/libpoly + (progn + (run cmake -B build -DCMAKE_BUILD_TYPE=$type -DCMAKE_INSTALL_PREFIX=$prefix) + (chdir build + (run make -j 4)))) + (copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) + (copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) (chdir vendor/cvc5 (progn - (run ./configure.sh --auto-download --static) + (run ./configure.sh --static) (run make -C build -j 4))) (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) - (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) - (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) - (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) + ;(copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) + ;(copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) + ;(copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) (subdir diff --git a/vendor/cadical b/vendor/cadical new file mode 160000 index 0000000..2df7b7f --- /dev/null +++ b/vendor/cadical @@ -0,0 +1 @@ +Subproject commit 2df7b7fed0f9c522fd4cdf6e88cecad4cac8a2df diff --git a/vendor/libpoly b/vendor/libpoly new file mode 160000 index 0000000..7a4dedc --- /dev/null +++ b/vendor/libpoly @@ -0,0 +1 @@ +Subproject commit 7a4dedcdc3446ac8fba5673faeb2e95bed9bb73a From 9a5c9fe0beef7957eaf69ddf3969f5122386fd87 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Thu, 25 Apr 2024 00:06:21 +0100 Subject: [PATCH 2/3] add env variables --- .gitmodules | 3 +++ api/dune | 2 +- dune | 37 +++++++++++++++++++++++-------------- vendor/symfpu | 1 + 4 files changed, 28 insertions(+), 15 deletions(-) create mode 160000 vendor/symfpu diff --git a/.gitmodules b/.gitmodules index 9df9db0..34fb972 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,3 +7,6 @@ [submodule "vendor/libpoly"] path = vendor/libpoly url = https://github.com/SRI-CSL/libpoly.git +[submodule "vendor/symfpu"] + path = vendor/symfpu + url = https://github.com/cvc5/symfpu.git diff --git a/api/dune b/api/dune index 37bd731..8362d0c 100644 --- a/api/dune +++ b/api/dune @@ -13,5 +13,5 @@ (extra_deps ../vendor/cvc5/include/cvc5/cvc5_export.h) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs ../vendor/cvc5/include)) - (foreign_archives ../cvc5 ../cadical ../picpoly ../picpolyxx) + (foreign_archives ../cvc5 ../cadical) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) diff --git a/dune b/dune index 2684a5c..8f9370e 100644 --- a/dune +++ b/dune @@ -1,7 +1,13 @@ +(env + (_ + (env-vars + (CMAKE_INCLUDE_PATH "../../cadical/src/:../../libpoly/include/:../../") + (CMAKE_LIBRARY_PATH "../../cadical/build/:../../libpoly/build/src/")))) + (rule (deps (source_tree vendor)) - (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a cvc5_export.h) + (targets libcadical.a libcvc5.a cvc5_export.h) (action (no-infer (progn @@ -11,23 +17,26 @@ (run ./configure) (run make -j 4))) (copy vendor/cadical/build/libcadical.a libcadical.a) - (chdir - vendor/libpoly - (progn - (run cmake -B build -DCMAKE_BUILD_TYPE=$type -DCMAKE_INSTALL_PREFIX=$prefix) - (chdir build - (run make -j 4)))) - (copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) - (copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) + ;(chdir + ; vendor/libpoly + ; (progn + ; (run + ; cmake + ; -B + ; build + ; -DCMAKE_BUILD_TYPE=$type + ; -DCMAKE_INSTALL_PREFIX=$prefix) + ; (chdir + ; build + ; (run make -j 4)))) + ;(copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) + ;(copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) (chdir vendor/cvc5 (progn - (run ./configure.sh --static) + (run ./configure.sh --static --no-poly) (run make -C build -j 4))) (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) - ;(copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) - ;(copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) - ;(copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) (subdir @@ -48,7 +57,7 @@ (names cvc5_stubs) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) - (foreign_archives cvc5 cadical picpoly picpolyxx) + (foreign_archives cvc5 cadical) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) (rule diff --git a/vendor/symfpu b/vendor/symfpu new file mode 160000 index 0000000..c3acaf6 --- /dev/null +++ b/vendor/symfpu @@ -0,0 +1 @@ +Subproject commit c3acaf62b137c36aae5eb380f1d883bfa9095f60 From a3f3d56f30f88775fe01de3ce3651ed64354149f Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Thu, 25 Apr 2024 15:01:39 +0100 Subject: [PATCH 3/3] include LibPoly in build --- api/dune | 2 +- dune | 37 +++++++++++++++++++------------------ 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/api/dune b/api/dune index 8362d0c..37bd731 100644 --- a/api/dune +++ b/api/dune @@ -13,5 +13,5 @@ (extra_deps ../vendor/cvc5/include/cvc5/cvc5_export.h) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs ../vendor/cvc5/include)) - (foreign_archives ../cvc5 ../cadical) + (foreign_archives ../cvc5 ../cadical ../picpoly ../picpolyxx) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) diff --git a/dune b/dune index 8f9370e..34fd38e 100644 --- a/dune +++ b/dune @@ -1,13 +1,13 @@ (env (_ (env-vars - (CMAKE_INCLUDE_PATH "../../cadical/src/:../../libpoly/include/:../../") + (CMAKE_INCLUDE_PATH "../../cadical/src/:../../libpoly/:../../") (CMAKE_LIBRARY_PATH "../../cadical/build/:../../libpoly/build/src/")))) (rule (deps (source_tree vendor)) - (targets libcadical.a libcvc5.a cvc5_export.h) + (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a cvc5_export.h) (action (no-infer (progn @@ -17,24 +17,25 @@ (run ./configure) (run make -j 4))) (copy vendor/cadical/build/libcadical.a libcadical.a) - ;(chdir - ; vendor/libpoly - ; (progn - ; (run - ; cmake - ; -B - ; build - ; -DCMAKE_BUILD_TYPE=$type - ; -DCMAKE_INSTALL_PREFIX=$prefix) - ; (chdir - ; build - ; (run make -j 4)))) - ;(copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) - ;(copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) + (chdir + vendor/libpoly + (progn + (run + cmake + -B + build + -DCMAKE_BUILD_TYPE=$type + -DCMAKE_INSTALL_PREFIX=$prefix) + (chdir + build + (run make -j 4)) + (run mv include poly))) + (copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) + (copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) (chdir vendor/cvc5 (progn - (run ./configure.sh --static --no-poly) + (run ./configure.sh --static) (run make -C build -j 4))) (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) @@ -57,7 +58,7 @@ (names cvc5_stubs) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) - (foreign_archives cvc5 cadical) + (foreign_archives cvc5 cadical picpoly picpolyxx) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) (rule