diff --git a/default.nix b/default.nix index 9403fa8c9d..a180666d4f 100644 --- a/default.nix +++ b/default.nix @@ -2,24 +2,12 @@ with import {}; -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 cvc5-pin = callPackage scripts/nix/cvc5/default.nix { nixpkgs = ; }; -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 + alt-ergo + cvc4 + cvc5 + z3 ] else []; in let why3-pin = diff --git a/scripts/nix/LICENSE b/scripts/nix/LICENSE deleted file mode 100644 index 40599d1455..0000000000 --- a/scripts/nix/LICENSE +++ /dev/null @@ -1,21 +0,0 @@ -MIT License - -Copyright (c) 2019 angr - -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to deal -in the Software without restriction, including without limitation the rights -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all -copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE -SOFTWARE. diff --git a/scripts/nix/alt-ergo/default.nix b/scripts/nix/alt-ergo/default.nix deleted file mode 100644 index cd175f7f2f..0000000000 --- a/scripts/nix/alt-ergo/default.nix +++ /dev/null @@ -1,54 +0,0 @@ -{ 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 deleted file mode 100644 index a97665c2f8..0000000000 --- a/scripts/nix/cvc4/cvc4-bash-patsub-replacement.patch +++ /dev/null @@ -1,39 +0,0 @@ -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 deleted file mode 100644 index 686d5a1c5b..0000000000 --- a/scripts/nix/cvc4/minisat-fenv.patch +++ /dev/null @@ -1,65 +0,0 @@ -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 deleted file mode 100644 index e847d14374..0000000000 --- a/scripts/nix/cvc5/default.nix +++ /dev/null @@ -1,39 +0,0 @@ -{ 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 deleted file mode 100644 index eb73267fc2..0000000000 --- a/scripts/nix/z3/default.nix +++ /dev/null @@ -1,49 +0,0 @@ -{ 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 ]; - }; -}