[nix] vendor prover derivations

default.nix

@@ -2,26 +2,23 @@
 
 with import <nixpkgs> {};
 
-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 = <nixpkgs>; };
+in
+
+let cvc4-pin = callPackage scripts/nix/cvc4/default.nix { nixpkgs = <nixpkgs>; };
 in
 
-let cvc4-pin = cvc4; in
+let cvc5-pin = callPackage scripts/nix/cvc5/default.nix { nixpkgs = <nixpkgs>; };
+in
 
-let z3-pin = z3_4_12; in
+let z3-pin = callPackage scripts/nix/z3/default.nix { nixpkgs = <nixpkgs>; };
+in
 
 let provers =
   if withProvers then [
     alt-ergo-pin
     cvc4-pin
+    cvc5-pin
     z3-pin
   ] else []; in
 

scripts/nix/alt-ergo/default.nix

@@ -0,0 +1,54 @@
+{ nixpkgs ? <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 ];
+  };
+}

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 <<EOF
+ /*********************                                                        */

scripts/nix/cvc4/default.nix

@@ -0,0 +1,49 @@
+{ nixpkgs ? <nixpkgs> }:
+
+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 ];
+  };
+}

scripts/nix/cvc4/minisat-fenv.patch

@@ -0,0 +1,65 @@
+From 7f1016ceab9b0f57a935bd51ca6df3d18439b472 Mon Sep 17 00:00:00 2001
+From: Will Dietz <[email protected]>
+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 <fpu_control.h>
++#include <fenv.h>
+ #endif
+
+ #include "mtl/IntTypes.h"
+-- 
+2.14.2
+

scripts/nix/cvc5/default.nix

@@ -0,0 +1,39 @@
+{ nixpkgs ? <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 ];
+  };
+}

scripts/nix/z3/default.nix

@@ -0,0 +1,49 @@
+{ nixpkgs ? <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 ];
+  };
+}