Merge commit '969cff2691a02b3d7e5468beda26c482d8986644'

5 files changed, 80 insertions, 7 deletions

diff --git a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
index 794430ebbe84..234b74749977 100644
--- a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -1,17 +1,20 @@
-{ fetchurl, stdenv, ocamlPackages }:
+{ fetchurl, stdenv, which, dune, ocamlPackages }:
 
 stdenv.mkDerivation rec {
   name = "alt-ergo-${version}";
-  version = "2.2.0";
+  version = "2.3.0";
 
   src = fetchurl {
     url    = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
     name   = "${name}.tar.gz";
-    sha256 = "106zfgisq6qxr7dlk8z7gi68ly7qff4frn8wab2g8z2nkkwla92w";
+    sha256 = "1ycr3ff0gacq1aqzs16n6swgfniwpim0m7rvhcam64kj0a80c6bz";
   };
 
-  buildInputs = with ocamlPackages;
-    [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex psmt2-frontend menhir num ];
+  buildInputs = [ dune which ] ++ (with ocamlPackages; [
+    ocaml findlib camlzip lablgtk menhir num ocplib-simplex psmt2-frontend seq zarith
+  ]);
+
+  preConfigure = "patchShebangs ./configure";
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
diff --git a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
index 91be7dca1173..ffd25b6238b7 100644
--- a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
@@ -11,7 +11,7 @@ let
 
   start_script =
     ''
-      #!/bin/sh
+      #!${stdenv.shell}
       cd $out/lib/hol_light
       exec ${ocaml}/bin/ocaml \
         -I \`${camlp5}/bin/camlp5 -where\` \
diff --git a/nixpkgs/pkgs/applications/science/logic/iprover/default.nix b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix
index d3950349711b..46b29e3dd271 100644
--- a/nixpkgs/pkgs/applications/science/logic/iprover/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix
@@ -19,7 +19,7 @@ stdenv.mkDerivation rec {
 
     mkdir -p "$out/share/${name}"
     cp *.p "$out/share/${name}"
-    echo -e "#! /bin/sh\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover
+    echo -e "#! ${stdenv.shell}\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover
     chmod a+x  "$out"/bin/iprover
   '';
 
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/0001-fix-2131.patch b/nixpkgs/pkgs/applications/science/logic/z3/0001-fix-2131.patch
new file mode 100644
index 000000000000..0b21b8fffd40
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/z3/0001-fix-2131.patch
@@ -0,0 +1,66 @@
+From c5df6ce96e068eceb77019e48634721c6a5bb607 Mon Sep 17 00:00:00 2001
+From: Nikolaj Bjorner <nbjorner@microsoft.com>
+Date: Sun, 10 Feb 2019 10:07:24 -0800
+Subject: [PATCH 1/1] fix #2131
+
+Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
+---
+ src/api/python/README.txt    | 10 +++-------
+ src/api/python/setup.py      |  2 +-
+ src/ast/recfun_decl_plugin.h |  2 +-
+ 3 files changed, 5 insertions(+), 9 deletions(-)
+
+diff --git a/src/api/python/README.txt b/src/api/python/README.txt
+index 9312b1119..561b8dedc 100644
+--- a/src/api/python/README.txt
++++ b/src/api/python/README.txt
+@@ -1,8 +1,4 @@
+-You can learn more about Z3Py at:
+-http://rise4fun.com/Z3Py/tutorial/guide
+-
+-On Windows, you must build Z3 before using Z3Py.
+-To build Z3, you should executed the following command
++On Windows, to build Z3, you should executed the following command
+ in the Z3 root directory at the Visual Studio Command Prompt
+ 
+        msbuild /p:configuration=external
+@@ -12,8 +8,8 @@ If you are using a 64-bit Python interpreter, you should use
+        msbuild /p:configuration=external /p:platform=x64
+ 
+ 
+-On Linux and macOS, you must install Z3Py, before trying example.py.
+-To install Z3Py on Linux and macOS, you should execute the following
++On Linux and macOS, you must install python bindings, before trying example.py.
++To install python on Linux and macOS, you should execute the following
+ command in the Z3 root directory
+ 
+         sudo make install-z3py
+diff --git a/src/api/python/setup.py b/src/api/python/setup.py
+index 2a750fee6..063680e2b 100644
+--- a/src/api/python/setup.py
++++ b/src/api/python/setup.py
+@@ -178,7 +178,7 @@ setup(
+     name='z3-solver',
+     version=_z3_version(),
+     description='an efficient SMT solver library',
+-    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3',
++    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/angr/angr-z3',
+     author="The Z3 Theorem Prover Project",
+     maintainer="Audrey Dutcher",
+     maintainer_email="audrey@rhelmot.io",
+diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
+index 0247335e8..b294cdfce 100644
+--- a/src/ast/recfun_decl_plugin.h
++++ b/src/ast/recfun_decl_plugin.h
+@@ -56,7 +56,7 @@ namespace recfun {
+         friend class def;
+         func_decl_ref       m_pred; //<! predicate used for this case
+         expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
+-        expr_ref            m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds
++        expr_ref            m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
+         def *               m_def; //<! definition this is a part of
+         bool                m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
+ 
+-- 
+2.19.2
+
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
index a4a55e3e8511..8c1c0ca23024 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
@@ -11,6 +11,10 @@ stdenv.mkDerivation rec {
     sha256 = "014igqm5vwswz0yhz0cdxsj3a6dh7i79hvhgc3jmmmz3z0xm1gyn";
   };
 
+  patches = [
+    ./0001-fix-2131.patch
+  ];
+
   buildInputs = [ python fixDarwinDylibNames ];
   propagatedBuildInputs = [ python.pkgs.setuptools ];
   enableParallelBuilding = true;