smtcoq: fix cvc4 dependency

pkgs/development/coq-modules/smtcoq/cvc4.nix

@@ -0,0 +1,44 @@
+{ lib, stdenv, cln, fetchurl, gmp, swig, pkg-config
+, readline, libantlr3c, boost, jdk8, autoreconfHook
+, python3, antlr3_4
+}:
+
+stdenv.mkDerivation rec {
+  pname = "cvc4";
+  version = "1.6";
+
+  src = fetchurl {
+    url = "https://cvc4.cs.stanford.edu/downloads/builds/src/cvc4-${version}.tar.gz";
+    sha256 = "1iw793zsi48q91lxpf8xl8lnvv0jsj4whdad79rakywkm1gbs62w";
+  };
+
+  nativeBuildInputs = [ autoreconfHook pkg-config ];
+  buildInputs = [ gmp readline swig libantlr3c antlr3_4 boost jdk8 python3 ]
+    ++ lib.optionals stdenv.isLinux [ cln ];
+
+  configureFlags = [
+    "--enable-language-bindings=c,c++,java"
+    "--enable-gpl"
+    "--with-readline"
+    "--with-boost=${boost.dev}"
+  ] ++ lib.optionals stdenv.isLinux [ "--with-cln" ];
+
+  prePatch = ''
+    patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat
+    patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat
+  '';
+
+  preConfigure = ''
+    patchShebangs ./src/
+  '';
+
+  enableParallelBuilding = true;
+
+  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 ];
+  };
+}

pkgs/development/coq-modules/smtcoq/default.nix

@@ -1,4 +1,4 @@
-{ lib, stdenv, mkCoqDerivation, coq, trakt, cvc4, veriT, zchaff, fetchurl, version ? null }:
+{ lib, stdenv, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, version ? null }:
 with lib;
 
 let
@@ -10,6 +10,7 @@ let
     };
     meta.broken = false;
   });
+  cvc4 = pkgs.callPackage ./cvc4.nix {};
 in
 
 mkCoqDerivation {

pkgs/development/coq-modules/smtcoq/minisat-fenv.patch

@@ -0,0 +1,65 @@
+From 7f1016ceab9b0f57a935bd51ca6df3d18439b472 Mon Sep 17 00:00:00 2001
+From: Will Dietz <w@wdtz.org>
+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
+