diff options
author | Will Dietz <w@wdtz.org> | 2019-05-31 21:59:36 -0500 |
---|---|---|
committer | Austin Seipp <aseipp@pobox.com> | 2019-06-10 17:55:26 -0700 |
commit | e397f4716c603e6d5b76bfc80b2c14b0ddedf106 (patch) | |
tree | cbd60cd7061970e78ff4e75b613235b55bc396e6 /pkgs/applications/science | |
parent | 4c4afb3cb97ee8ab4a4505241fa99e8992b547e8 (diff) |
z3: 4.8.4 -> 4.8.5
* drop included patch * pname-ify
Diffstat (limited to 'pkgs/applications/science')
-rw-r--r-- | pkgs/applications/science/logic/z3/0001-fix-2131.patch | 66 | ||||
-rw-r--r-- | pkgs/applications/science/logic/z3/default.nix | 14 |
2 files changed, 5 insertions, 75 deletions
diff --git a/pkgs/applications/science/logic/z3/0001-fix-2131.patch b/pkgs/applications/science/logic/z3/0001-fix-2131.patch deleted file mode 100644 index 0b21b8fffd40f..0000000000000 --- a/pkgs/applications/science/logic/z3/0001-fix-2131.patch +++ /dev/null @@ -1,66 +0,0 @@ -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/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 8c1c0ca23024a..14f75fb68b5e1 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -1,20 +1,16 @@ { stdenv, fetchFromGitHub, python, fixDarwinDylibNames }: stdenv.mkDerivation rec { - name = "z3-${version}"; - version = "4.8.4"; + pname = "z3"; + version = "4.8.5"; src = fetchFromGitHub { owner = "Z3Prover"; - repo = "z3"; - rev = name; - sha256 = "014igqm5vwswz0yhz0cdxsj3a6dh7i79hvhgc3jmmmz3z0xm1gyn"; + repo = pname; + rev = "Z3-${version}"; + sha256 = "11sy98clv7ln0a5vqxzvh6wwqbswsjbik2084hav5kfws4xvklfa"; }; - patches = [ - ./0001-fix-2131.patch - ]; - buildInputs = [ python fixDarwinDylibNames ]; propagatedBuildInputs = [ python.pkgs.setuptools ]; enableParallelBuilding = true; |