From 1d5621928c6f7566eaaf63f0a4597b44bbc22798 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 30 Aug 2023 16:12:52 +0100 Subject: [PATCH] [nix] vendor prover derivations --- default.nix | 21 +++--- scripts/nix/alt-ergo/default.nix | 54 +++++++++++++++ .../cvc4/cvc4-bash-patsub-replacement.patch | 39 +++++++++++ scripts/nix/cvc4/default.nix | 49 ++++++++++++++ scripts/nix/cvc4/minisat-fenv.patch | 65 +++++++++++++++++++ scripts/nix/cvc5/default.nix | 39 +++++++++++ scripts/nix/z3/default.nix | 49 ++++++++++++++ 7 files changed, 304 insertions(+), 12 deletions(-) create mode 100644 scripts/nix/alt-ergo/default.nix create mode 100644 scripts/nix/cvc4/cvc4-bash-patsub-replacement.patch create mode 100644 scripts/nix/cvc4/default.nix create mode 100644 scripts/nix/cvc4/minisat-fenv.patch create mode 100644 scripts/nix/cvc5/default.nix create mode 100644 scripts/nix/z3/default.nix diff --git a/default.nix b/default.nix index a6f64c9a0b..9403fa8c9d 100644 --- a/default.nix +++ b/default.nix @@ -2,26 +2,23 @@ with import {}; -let alt-ergo-pin = - alt-ergo.overrideAttrs (o : rec { - version = "2.4.2"; - src = fetchFromGitHub { - owner = "OCamlPro"; - repo = "alt-ergo"; - rev = version; - hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc="; - }; - }); +let alt-ergo-pin = callPackage scripts/nix/alt-ergo/default.nix { nixpkgs = ; }; +in + +let cvc4-pin = callPackage scripts/nix/cvc4/default.nix { nixpkgs = ; }; in -let cvc4-pin = cvc4; in +let cvc5-pin = callPackage scripts/nix/cvc5/default.nix { nixpkgs = ; }; +in -let z3-pin = z3_4_12; in +let z3-pin = callPackage scripts/nix/z3/default.nix { nixpkgs = ; }; +in let provers = if withProvers then [ alt-ergo-pin cvc4-pin + cvc5-pin z3-pin ] else []; in diff --git a/scripts/nix/alt-ergo/default.nix b/scripts/nix/alt-ergo/default.nix new file mode 100644 index 0000000000..cd175f7f2f --- /dev/null +++ b/scripts/nix/alt-ergo/default.nix @@ -0,0 +1,54 @@ +{ nixpkgs ? }: + +with import nixpkgs { }; + +let + pname = "alt-ergo"; + version = "2.4.2"; + + configureScript = "ocaml unix.cma configure.ml"; + + src = fetchFromGitHub { + owner = "OCamlPro"; + repo = pname; + rev = version; + hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc="; + }; +in + +let alt-ergo-lib = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-lib"; + inherit version src configureScript; + configureFlags = [ pname ]; + nativeBuildInputs = [ which ]; + buildInputs = with ocamlPackages; [ dune-configurator ]; + propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ]; + preBuild = '' + substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"' + ''; +}; in + +let alt-ergo-parsers = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-parsers"; + inherit version src configureScript; + configureFlags = [ pname ]; + nativeBuildInputs = [ which ocamlPackages.menhir ]; + propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]); +}; in + +ocamlPackages.buildDunePackage { + + inherit pname version src configureScript; + + configureFlags = [ pname ]; + + nativeBuildInputs = [ which ocamlPackages.menhir ]; + buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ]; + + meta = { + description = "High-performance theorem prover and SMT solver"; + homepage = "https://alt-ergo.ocamlpro.com/"; + license = lib.licenses.ocamlpro_nc; + maintainers = [ lib.maintainers.thoughtpolice ]; + }; +} diff --git a/scripts/nix/cvc4/cvc4-bash-patsub-replacement.patch b/scripts/nix/cvc4/cvc4-bash-patsub-replacement.patch new file mode 100644 index 0000000000..a97665c2f8 --- /dev/null +++ b/scripts/nix/cvc4/cvc4-bash-patsub-replacement.patch @@ -0,0 +1,39 @@ +Per https://bodhi.fedoraproject.org/updates/FEDORA-2022-dc47174c36: + +This update fixes a failure to build with source with bash 5.2. Bash's +`patsub_replacement` feature makes ampersand a special character when doing +variable substitution, which was not previously the case. This update instructs +bash to turn off the new behavior. + +The patch itself is adapted from +https://src.fedoraproject.org/rpms/cvc4/blob/f7c24c6ad72a8812d244313f13032fa23d393315/f/cvc4-bash-patsub-replacement.patch. +--- a/src/expr/mkexpr 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkexpr 2022-10-11 14:28:31.120453409 -0600 +@@ -16,6 +16,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + filename=`basename "$1" | sed 's,_template,,'` + +--- a/src/expr/mkkind 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkkind 2022-10-11 14:34:17.008996126 -0600 +@@ -15,6 +15,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + filename=`basename "$1" | sed 's,_template,,'` + +--- a/src/expr/mkmetakind 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkmetakind 2022-10-11 14:34:32.248020036 -0600 +@@ -18,6 +18,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + cat < }: + +with import nixpkgs { }; + +stdenv.mkDerivation rec { + pname = "cvc4"; + version = "1.8"; + + src = fetchFromGitHub { + owner = "cvc4"; + repo = "cvc4"; + rev = version; + sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp"; + }; + + nativeBuildInputs = [ pkg-config cmake ]; + buildInputs = [ gmp git python3.pkgs.toml readline swig libantlr3c antlr3_4 boost jdk python3 ] + ++ lib.optionals (!stdenv.isDarwin) [ cln ]; + configureFlags = [ + "--enable-language-bindings=c,c++,java" + "--enable-gpl" + "--with-readline" + "--with-boost=${boost.dev}" + ] ++ lib.optionals (!stdenv.isDarwin) [ "--with-cln" ]; + + prePatch = '' + patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat + patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat + ''; + + patches = [ + ./cvc4-bash-patsub-replacement.patch + ]; + + preConfigure = '' + patchShebangs ./src/ + ''; + cmakeFlags = [ + "-DCMAKE_BUILD_TYPE=Production" + ]; + + meta = with lib; { + description = "A high-performance theorem prover and SMT solver"; + homepage = "http://cvc4.cs.stanford.edu/web/"; + license = licenses.gpl3; + platforms = platforms.unix; + maintainers = with maintainers; [ vbgl thoughtpolice gebner ]; + }; +} diff --git a/scripts/nix/cvc4/minisat-fenv.patch b/scripts/nix/cvc4/minisat-fenv.patch new file mode 100644 index 0000000000..686d5a1c5b --- /dev/null +++ b/scripts/nix/cvc4/minisat-fenv.patch @@ -0,0 +1,65 @@ +From 7f1016ceab9b0f57a935bd51ca6df3d18439b472 Mon Sep 17 00:00:00 2001 +From: Will Dietz +Date: Tue, 17 Oct 2017 22:57:02 -0500 +Subject: [PATCH] use fenv instead of non-standard fpu_control + +--- + core/Main.cc | 8 ++++++-- + simp/Main.cc | 8 ++++++-- + utils/System.h | 2 +- + 3 files changed, 13 insertions(+), 5 deletions(-) + +diff --git a/core/Main.cc b/core/Main.cc +index 2b0d97b..8ad95fb 100644 +--- a/core/Main.cc ++++ b/core/Main.cc +@@ -78,8 +78,12 @@ int main(int argc, char** argv) + // printf("This is MiniSat 2.0 beta\n"); + + #if defined(__linux__) +- fpu_control_t oldcw, newcw; +- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); ++ fenv_t fenv; ++ ++ fegetenv(&fenv); ++ fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */ ++ fenv.__control_word |= 0x200; /* _FPU_DOUBLE */ ++ fesetenv(&fenv); + printf("WARNING: for repeatability, setting FPU to use double precision\n"); + #endif + // Extra options: +diff --git a/simp/Main.cc b/simp/Main.cc +index 2804d7f..39bfb71 100644 +--- a/simp/Main.cc ++++ b/simp/Main.cc +@@ -79,8 +79,12 @@ int main(int argc, char** argv) + // printf("This is MiniSat 2.0 beta\n"); + + #if defined(__linux__) +- fpu_control_t oldcw, newcw; +- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); ++ fenv_t fenv; ++ ++ fegetenv(&fenv); ++ fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */ ++ fenv.__control_word |= 0x200; /* _FPU_DOUBLE */ ++ fesetenv(&fenv); + printf("WARNING: for repeatability, setting FPU to use double precision\n"); + #endif + // Extra options: +diff --git a/utils/System.h b/utils/System.h +index 1758192..c0ad13a 100644 +--- a/utils/System.h ++++ b/utils/System.h +@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA + #define Minisat_System_h + + #if defined(__linux__) +-#include ++#include + #endif + + #include "mtl/IntTypes.h" +-- +2.14.2 + diff --git a/scripts/nix/cvc5/default.nix b/scripts/nix/cvc5/default.nix new file mode 100644 index 0000000000..e847d14374 --- /dev/null +++ b/scripts/nix/cvc5/default.nix @@ -0,0 +1,39 @@ +{ nixpkgs ? }: + +with import nixpkgs { }; + +stdenv.mkDerivation rec { + pname = "cvc5"; + version = "1.0.6"; + + src = fetchFromGitHub { + owner = "cvc5"; + repo = "cvc5"; + rev = "cvc5-${version}"; + hash = "sha256-pZiXAO92cwnYtaVMDFBEmk+NzDf4eKdc0eY0RltofPA="; + }; + + nativeBuildInputs = [ pkg-config cmake flex ]; + buildInputs = [ + cadical.dev symfpu gmp gtest libantlr3c antlr3_4 boost jdk + (python3.withPackages (ps: with ps; [ pyparsing tomli ])) + ]; + + preConfigure = '' + patchShebangs ./src/ + ''; + + cmakeFlags = [ + "-DCMAKE_BUILD_TYPE=Production" + "-DBUILD_SHARED_LIBS=1" + "-DANTLR3_JAR=${antlr3_4}/lib/antlr/antlr-3.4-complete.jar" + ]; + + meta = with lib; { + description = "A high-performance theorem prover and SMT solver"; + homepage = "https://cvc5.github.io"; + license = licenses.gpl3Only; + platforms = platforms.unix; + maintainers = with maintainers; [ shadaj ]; + }; +} diff --git a/scripts/nix/z3/default.nix b/scripts/nix/z3/default.nix new file mode 100644 index 0000000000..eb73267fc2 --- /dev/null +++ b/scripts/nix/z3/default.nix @@ -0,0 +1,49 @@ +{ nixpkgs ? }: + +with import nixpkgs { }; + +let python = python3; in + +stdenv.mkDerivation rec { + pname = "z3"; + version = "4.12.2"; + sha256 = "sha256-DTgpKEG/LtCGZDnicYvbxG//JMLv25VHn/NaF307JYA="; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = pname; + rev = "-${version}"; + sha256 = sha256; + }; + + strictDeps = true; + + nativeBuildInputs = [ python ]; + propagatedBuildInputs = [ python.pkgs.setuptools ]; + enableParallelBuilding = true; + + configurePhase = "${python.pythonForBuild.interpreter} scripts/mk_make.py --prefix=$out\ncd build"; + + doCheck = true; + checkPhase = '' + make test + ./test-z3 -a + ''; + + postInstall = '' + mkdir -p $dev $lib + mv $out/lib $lib/lib + mv $out/include $dev/include + ''; + + outputs = [ "out" "lib" "dev" ]; + + meta = with lib; { + description = "A high-performance theorem prover and SMT solver"; + homepage = "https://github.com/Z3Prover/z3"; + changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${version}"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice ttuegel ]; + }; +}