[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Amin Bandali <bandali@gnu.org>]

[-- Attachment #1: Type: text/plain, Size: 623 bytes --]

Hello!

On 2018-12-21  9:40 PM, Marius Bakke wrote:
> Ludovic Courtès <ludo@gnu.org> writes:
>
>> Hello!
>>
>> [...]
>>
>> Marius, WDYT?
>
> Hello!
>
> I don't actually know z3 at all, I just updated it to fix the build on
> core-updates :-)
>
> In any case dropping python2 bindings seems sensible, seeing as Python 2
> is EOL in a year[1].  So please go ahead, thank you Amin!
>
> [1]: https://www.python.org/dev/peps/pep-0373/
>

Thanks for the reply, Marius.  I’ve attached a new version of the patch
with only Python 3 bindings and with Ludo’s feedback about ‘which’.

Best,
amin


[-- Attachment #2: 0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch --]
[-- Type: text/x-patch, Size: 3997 bytes --]

From ed80a156cd0aa3d7839e49bd6ebdd5e2911067ae Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Fri, 21 Dec 2018 18:27:11 -0500
Subject: [PATCH v2] gnu: z3: Update to 4.8.3 and provide python3 bindings

* gnu/packages/maths.scm (z3): Update to 4.8.3.
[build-system]: Switch from cmake to make, and use the current
scripts/mk_make.py build script instead of the now-deprecated
contrib/cmake/bootstrap.py.
---
 gnu/packages/maths.scm | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9fb02b738..f49b50c23 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -29,6 +29,7 @@
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -116,6 +117,7 @@
   #:use-module (gnu packages tex)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages version-control)
+  #:use-module (gnu packages which)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
   #:use-module (srfi srfi-1))
@@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.")
 (define-public z3
   (package
     (name "z3")
-    (version "4.8.1")
+    (version "4.8.3")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"))))
-    (build-system cmake-build-system)
+                "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar"))))
+    (build-system gnu-build-system)
     (arguments
-     `(#:configure-flags
-       (list "-DBUILD_PYTHON_BINDINGS=true"
-             "-DINSTALL_PYTHON_BINDINGS=true"
-             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
-                            %output
-                            "/lib/python2.7/site-packages"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
          (add-after 'unpack 'fix-compatability
            ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
@@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.")
          (add-before 'configure 'bootstrap
            (lambda _
              (zero?
-              (system* "python" "contrib/cmake/bootstrap.py" "create"))))
+              (system* "python" "scripts/mk_make.py"))))
+         ;; work around gnu-build-system's setting --enable-fast-install
+         ;; (z3's `configure' is a wrapper around the above python file,
+         ;; which fails when passed --enable-fast-install)
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (invoke "./configure"
+                     (string-append "--prefix=" (assoc-ref outputs "out")))))
+         (add-after 'configure 'change-directory
+           (lambda _
+             (chdir "build")
+             #t))
          (add-before 'check 'make-test-z3
            (lambda _
              ;; Build the test suite executable.
@@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.")
              ;; Run all the tests that don't require arguments.
              (zero? (system* "./test-z3" "/a")))))))
     (native-inputs
-     `(("python" ,python-2)))
+     `(("which" ,(@ (gnu packages base) which))
+       ("python" ,python-wrapper)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
-- 
2.20.1