Merge staging and PR #35021

It's the last staging commit (mostly) built on Hydra,
and a minimal fix for Darwin regression in pysqlite.

7 files changed, 248 insertions, 2 deletions

diff --git a/pkgs/applications/science/logic/avy/default.nix b/pkgs/applications/science/logic/avy/default.nix
index 379224c73f89..218006e15d5c 100644
--- a/pkgs/applications/science/logic/avy/default.nix
+++ b/pkgs/applications/science/logic/avy/default.nix
@@ -12,7 +12,25 @@ stdenv.mkDerivation rec {
   };
 
   buildInputs = [ cmake zlib boost.out boost.dev ];
-  NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ];
+  NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ]
+    # Squelch endless stream of warnings on same few things
+    ++ stdenv.lib.optionals stdenv.cc.isClang [
+      "-Wno-empty-body"
+      "-Wno-tautological-compare"
+      "-Wc++11-compat-deprecated-writable-strings"
+      "-Wno-deprecated"
+    ];
+
+  prePatch = ''
+    sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h
+    substituteInPlace abc/src/bdd/dsd/dsd.h --replace \
+               '((Child = Dsd_NodeReadDec(Node,Index))>=0);' \
+               '((intptr_t)(Child = Dsd_NodeReadDec(Node,Index))>=0);'
+
+    patch -p1 -d minisat -i ${./minisat-fenv.patch}
+    patch -p1 -d glucose -i ${./glucose-fenv.patch}
+  '';
+
   patches =
     [ ./0001-no-static-boost-libs.patch
     ];
diff --git a/pkgs/applications/science/logic/avy/glucose-fenv.patch b/pkgs/applications/science/logic/avy/glucose-fenv.patch
new file mode 100644
index 000000000000..dd19f7ec80e7
--- /dev/null
+++ b/pkgs/applications/science/logic/avy/glucose-fenv.patch
@@ -0,0 +1,65 @@
+From d6e0cb60270e8653bda3f339e3a07ce2cd2d6eb0 Mon Sep 17 00:00:00 2001
+From: Will Dietz <w@wdtz.org>
+Date: Tue, 17 Oct 2017 23:01:36 -0500
+Subject: [PATCH] glucose: use fenv to set double precision
+
+---
+ 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 c96aadd..994132b 100644
+--- a/core/Main.cc
++++ b/core/Main.cc
+@@ -96,8 +96,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("c WARNING: for repeatability, setting FPU to use double precision\n");
+ #endif
+         // Extra options:
+diff --git a/simp/Main.cc b/simp/Main.cc
+index 4f4772d..70c2e4b 100644
+--- a/simp/Main.cc
++++ b/simp/Main.cc
+@@ -97,8 +97,12 @@ int main(int argc, char** argv)
+         
+         
+ #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 004d498..a768e99 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 Glucose_System_h
+ 
+ #if defined(__linux__)
+-#include <fpu_control.h>
++#include <fenv.h>
+ #endif
+ 
+ #include "glucose/mtl/IntTypes.h"
+-- 
+2.14.2
+
diff --git a/pkgs/applications/science/logic/avy/minisat-fenv.patch b/pkgs/applications/science/logic/avy/minisat-fenv.patch
new file mode 100644
index 000000000000..686d5a1c5b49
--- /dev/null
+++ b/pkgs/applications/science/logic/avy/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
+
diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix
index 2b40995b7433..aa815e48db41 100644
--- a/pkgs/applications/science/logic/boolector/default.nix
+++ b/pkgs/applications/science/logic/boolector/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl }:
+{ stdenv, fetchurl, writeShellScriptBin }:
 
 stdenv.mkDerivation rec {
   name    = "boolector-${version}";
@@ -8,6 +8,24 @@ stdenv.mkDerivation rec {
     sha256 = "0mdf7hwix237pvknvrpazcx6s3ininj5k7vhysqjqgxa7lxgq045";
   };
 
+  prePatch =
+    let
+      lingelingPatch = writeShellScriptBin "lingeling-patch" ''
+        sed -i -e "1i#include <stdint.h>" lingeling/lglib.h
+
+        ${crossFix}/bin/crossFix lingeling
+      '';
+      crossFix = writeShellScriptBin "crossFix" ''
+        # substituteInPlace not available here
+        sed -i $1/makefile.in \
+          -e 's@ar rc@$(AR) rc@' \
+          -e 's@ranlib@$(RANLIB)@'
+      '';
+    in ''
+    sed -i -e 's@mv lingeling\* lingeling@\0 \&\& ${lingelingPatch}/bin/lingeling-patch@' makefile
+    sed -i -e 's@mv boolector\* boolector@\0 \&\& ${crossFix}/bin/crossFix boolector@' makefile
+  '';
+
   installPhase = ''
     mkdir $out
     mv boolector/bin $out
diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix
index 6b213226635d..403eff216f53 100644
--- a/pkgs/applications/science/logic/cvc4/default.nix
+++ b/pkgs/applications/science/logic/cvc4/default.nix
@@ -22,10 +22,17 @@ stdenv.mkDerivation rec {
     "--with-boost=${boost.dev}"
   ];
 
+  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 stdenv.lib; {
     description = "A high-performance theorem prover and SMT solver";
     homepage    = http://cvc4.cs.nyu.edu/web/;
diff --git a/pkgs/applications/science/logic/cvc4/minisat-fenv.patch b/pkgs/applications/science/logic/cvc4/minisat-fenv.patch
new file mode 100644
index 000000000000..686d5a1c5b49
--- /dev/null
+++ b/pkgs/applications/science/logic/cvc4/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
+
diff --git a/pkgs/applications/science/logic/picosat/default.nix b/pkgs/applications/science/logic/picosat/default.nix
index e026cfad218e..db252f97916a 100644
--- a/pkgs/applications/science/logic/picosat/default.nix
+++ b/pkgs/applications/science/logic/picosat/default.nix
@@ -9,6 +9,14 @@ stdenv.mkDerivation rec {
     sha256 = "0m578rpa5rdn08d10kr4lbsdwp4402hpavrz6n7n53xs517rn5hm";
   };
 
+  prePatch = ''
+    substituteInPlace picosat.c --replace "sys/unistd.h" "unistd.h"
+
+    substituteInPlace makefile.in \
+      --replace 'ar rc' '$(AR) rc' \
+      --replace 'ranlib' '$(RANLIB)'
+  '';
+
   configurePhase = "./configure.sh --shared --trace";
 
   installPhase = ''