GNU bug report logs - #27461
[PATCH] gnu: Add z3.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 27461 in the body.
You can then email your comments to 27461 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: guix-patches <at> gnu.org
Cc: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: [PATCH] gnu: Add z3.
Date: Fri, 23 Jun 2017 18:50:22 +0300

* gnu/packages/maths.scm (z3): New variable.
* gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs.
---
 gnu/packages/fpga.scm  |  5 ++++-
 gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm
index 420d0aff2..220877577 100644
--- a/gnu/packages/fpga.scm
+++ b/gnu/packages/fpga.scm
@@ -1,6 +1,6 @@
 ;;; GNU Guix --- Functional package management for GNU
 ;;; Copyright © 2016 Danny Milosavljevic <dannym <at> scratchpost.org>
-;;; Copyright © 2016 Theodoros Foradis <theodoros.for <at> openmailbox.org>
+;;; Copyright © 2016, 2017 Theodoros Foradis <theodoros.for <at> openmailbox.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -36,6 +36,7 @@
   #:use-module (gnu packages graphviz)
   #:use-module (gnu packages libffi)
   #:use-module (gnu packages linux)
+  #:use-module (gnu packages maths)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages ghostscript)
   #:use-module (gnu packages gperf)
@@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in the desired format.")
        ("psmisc" ,psmisc)
        ("xdot" ,xdot)
        ("abc" ,abc)))
+    (propagated-inputs
+     `(("z3" ,z3))) ; should be in path for yosys-smtbmc
     (home-page "http://www.clifford.at/yosys/")
     (synopsis "FPGA Verilog RTL synthesizer")
     (description "Yosys synthesizes Verilog-2005.")
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1115cef59..3ee0beeef 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -18,6 +18,7 @@
 ;;; Copyright © 2017 Paul Garlick <pgarlick <at> tourbillion-technology.com>
 ;;; Copyright © 2017 ng0 <contact.ng0 <at> cryptolab.net>
 ;;; Copyright © 2017 Ben Woodcroft <donttrustben <at> gmail.com>
+;;; Copyright © 2017 Theodoros Foradis <theodoros.for <at> openmailbox.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -3129,3 +3130,36 @@ as equations, scalars, vectors, and matrices.")
     (home-page "https://www.gnu.org/software/jacal/")
     (license license:gpl3+)))
 
+(define-public z3
+  (package
+    (name "z3")
+    (version "4.5.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/Z3Prover/z3/archive/z3-"
+                    version ".tar.gz"))
+              (sha256
+               (base32
+                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (zero?
+              (system* "python" "scripts/mk_make.py"
+                       (string-append "--prefix="
+                                      (assoc-ref outputs "out"))))))
+         (add-after 'configure 'change-dir
+           (lambda _
+             (chdir "build")
+             #t)))))
+    (native-inputs
+     `(("python" ,python-2)))
+    (synopsis "Theorem prover")
+    (description "@code{z3} is a theorem prover.")
+    (home-page "https://github.com/Z3Prover/z3")
+    (license license:expat) ))
-- 
2.13.1

Message #8 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: julien lepiller <julien <at> lepiller.eu>
To: 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH] gnu: Add z3.
Date: Sun, 25 Jun 2017 10:19:44 +0200

Hi,

I don't have a patch for this yet, but I was working on z3 as a 
dependency of angr. So here is what I got.

As you can see, I separated the package in two: the library itself, and 
the python module that uses that library. I'm doing this because there 
are other languages than python. What do you think?

(define-public z3-solver
  (package
    (name "z3-solver")
    (version "4.5.0")
    (source (origin
              (method url-fetch)
              (uri (string-append 
"https://github.com/Z3Prover/z3/archive/z3-"
                                  version ".tar.gz"))
              (sha256
               (base32
                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))
              (file-name (string-append name "-" version ".tar.gz"))))
    (build-system gnu-build-system)
    (arguments
     `(#:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (add-before 'build 'generate-make
           (lambda _
             (system* "python" "scripts/mk_make.py")
             (chdir "build"))))
       #:test-target "test"
       #:make-flags
       (list (string-append "PREFIX=" (assoc-ref %outputs "out")))))
    (native-inputs
     `(("python" ,python-2)))
    (home-page "https://github.com/Z3Prover/z3")
    (synopsis "SMT solver library")
    (description "Z3 is a theorem prover from Microsoft Research.")
    (license license:expat)))

(define-public python2-z3-solver
  (package
    (inherit z3-solver)
    (name "python2-z3-solver")
    (build-system python-build-system)
    (propagated-inputs
     `(("z3" ,z3-solver)))
    (arguments
     `(#:python ,python-2
       #:phases
       (modify-phases %standard-phases
         (add-before 'build 'prepare
           (lambda* (#:key inputs #:allow-other-keys)
             (system* "python" "scripts/mk_make.py")
             (copy-file "build/python/z3/z3core.py" 
"src/api/python/z3/z3core.py")
             (copy-file "build/python/z3/z3consts.py" 
"src/api/python/z3/z3consts.py")
             (chdir "src/api/python")
             (substitute* "z3/z3core.py"
               (("_dirs = \\[")
                (string-append "_dirs = ['" (assoc-ref inputs "z3")
                                            "/lib', ")))
             (substitute* "MANIFEST.in"
               ((".*") ""))
             (substitute* "setup.py"
               (("self.execute\\(.*") "\n")
               (("scripts=.*") "\n")))))))))

Le 2017-06-23 17:50, Theodoros Foradis a écrit :
> * gnu/packages/maths.scm (z3): New variable.
> * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs.
> ---
>  gnu/packages/fpga.scm  |  5 ++++-
>  gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++
>  2 files changed, 38 insertions(+), 1 deletion(-)
> 
> diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm
> index 420d0aff2..220877577 100644
> --- a/gnu/packages/fpga.scm
> +++ b/gnu/packages/fpga.scm
> @@ -1,6 +1,6 @@
>  ;;; GNU Guix --- Functional package management for GNU
>  ;;; Copyright © 2016 Danny Milosavljevic <dannym <at> scratchpost.org>
> -;;; Copyright © 2016 Theodoros Foradis <theodoros.for <at> openmailbox.org>
> +;;; Copyright © 2016, 2017 Theodoros Foradis 
> <theodoros.for <at> openmailbox.org>
>  ;;;
>  ;;; This file is part of GNU Guix.
>  ;;;
> @@ -36,6 +36,7 @@
>    #:use-module (gnu packages graphviz)
>    #:use-module (gnu packages libffi)
>    #:use-module (gnu packages linux)
> +  #:use-module (gnu packages maths)
>    #:use-module (gnu packages perl)
>    #:use-module (gnu packages ghostscript)
>    #:use-module (gnu packages gperf)
> @@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in
> the desired format.")
>         ("psmisc" ,psmisc)
>         ("xdot" ,xdot)
>         ("abc" ,abc)))
> +    (propagated-inputs
> +     `(("z3" ,z3))) ; should be in path for yosys-smtbmc
>      (home-page "http://www.clifford.at/yosys/")
>      (synopsis "FPGA Verilog RTL synthesizer")
>      (description "Yosys synthesizes Verilog-2005.")
> diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
> index 1115cef59..3ee0beeef 100644
> --- a/gnu/packages/maths.scm
> +++ b/gnu/packages/maths.scm
> @@ -18,6 +18,7 @@
>  ;;; Copyright © 2017 Paul Garlick 
> <pgarlick <at> tourbillion-technology.com>
>  ;;; Copyright © 2017 ng0 <contact.ng0 <at> cryptolab.net>
>  ;;; Copyright © 2017 Ben Woodcroft <donttrustben <at> gmail.com>
> +;;; Copyright © 2017 Theodoros Foradis <theodoros.for <at> openmailbox.org>
>  ;;;
>  ;;; This file is part of GNU Guix.
>  ;;;
> @@ -3129,3 +3130,36 @@ as equations, scalars, vectors, and matrices.")
>      (home-page "https://www.gnu.org/software/jacal/")
>      (license license:gpl3+)))
> 
> +(define-public z3
> +  (package
> +    (name "z3")
> +    (version "4.5.0")
> +    (source (origin
> +              (method url-fetch)
> +              (uri (string-append
> +                    "https://github.com/Z3Prover/z3/archive/z3-"
> +                    version ".tar.gz"))
> +              (sha256
> +               (base32
> +                
> "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
> +    (build-system gnu-build-system)
> +    (arguments
> +     `(#:test-target "test"
> +       #:phases
> +       (modify-phases %standard-phases
> +         (replace 'configure
> +           (lambda* (#:key inputs outputs #:allow-other-keys)
> +             (zero?
> +              (system* "python" "scripts/mk_make.py"
> +                       (string-append "--prefix="
> +                                      (assoc-ref outputs "out"))))))
> +         (add-after 'configure 'change-dir
> +           (lambda _
> +             (chdir "build")
> +             #t)))))
> +    (native-inputs
> +     `(("python" ,python-2)))
> +    (synopsis "Theorem prover")
> +    (description "@code{z3} is a theorem prover.")
> +    (home-page "https://github.com/Z3Prover/z3")
> +    (license license:expat) ))

Message #11 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: julien lepiller <julien <at> lepiller.eu>
Cc: Theodoros Foradis <theodoros.for <at> openmailbox.org>, 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH] gnu: Add z3.
Date: Mon, 26 Jun 2017 19:31:15 +0300

Hello,

> Hi,
>
> I don't have a patch for this yet, but I was working on z3 as a 
> dependency of angr. So here is what I got.
>
> As you can see, I separated the package in two: the library itself, and 
> the python module that uses that library. I'm doing this because there 
> are other languages than python. What do you think?
>
> (define-public z3-solver
>    (package
>      (name "z3-solver")
>      (version "4.5.0")
>      (source (origin
>                (method url-fetch)
>                (uri (string-append 
> "https://github.com/Z3Prover/z3/archive/z3-"
>                                    version ".tar.gz"))
>                (sha256
>                 (base32
>                  "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))
>                (file-name (string-append name "-" version ".tar.gz"))))
>      (build-system gnu-build-system)
>      (arguments
>       `(#:phases
>         (modify-phases %standard-phases
>           (delete 'configure)
>           (add-before 'build 'generate-make
>             (lambda _
>               (system* "python" "scripts/mk_make.py")
>               (chdir "build"))))
>         #:test-target "test"
>         #:make-flags
>         (list (string-append "PREFIX=" (assoc-ref %outputs "out")))))
>      (native-inputs
>       `(("python" ,python-2)))
>      (home-page "https://github.com/Z3Prover/z3")
>      (synopsis "SMT solver library")
>      (description "Z3 is a theorem prover from Microsoft Research.")
>      (license license:expat)))
>

This is very similar to my package. The minor difference is that I only
pass the prefix once during configure (running the "scripts/mk_make.py),
instead of both incovations of make.

Also, if it's more correct, I can merge the 2 phases (configure and
change-dir) into one, as you do.

> (define-public python2-z3-solver
>    (package
>      (inherit z3-solver)
>      (name "python2-z3-solver")
>      (build-system python-build-system)
>      (propagated-inputs
>       `(("z3" ,z3-solver)))
>      (arguments
>       `(#:python ,python-2
>         #:phases
>         (modify-phases %standard-phases
>           (add-before 'build 'prepare
>             (lambda* (#:key inputs #:allow-other-keys)
>               (system* "python" "scripts/mk_make.py")
>               (copy-file "build/python/z3/z3core.py" 
> "src/api/python/z3/z3core.py")
>               (copy-file "build/python/z3/z3consts.py" 
> "src/api/python/z3/z3consts.py")
>               (chdir "src/api/python")
>               (substitute* "z3/z3core.py"
>                 (("_dirs = \\[")
>                  (string-append "_dirs = ['" (assoc-ref inputs "z3")
>                                              "/lib', ")))
>               (substitute* "MANIFEST.in"
>                 ((".*") ""))
>               (substitute* "setup.py"
>                 (("self.execute\\(.*") "\n")
>                 (("scripts=.*") "\n")))))))))

This builds correctly for me, though I'm no expert in python
packaging. Since this will likely be in a different file (python.scm?),
maybe we can proceed with just z3 if others are ok with it, and then you
only add python2-z3 later, in the patch-set with angr?

Or maybe it would be preferable to have just one z3 package also
providing the python bindings? I think seperate packages are better,
though.

Regards,
-- 
Theodoros Foradis

Message #14 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Cc: julien lepiller <julien <at> lepiller.eu>, 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH] gnu: Add z3.
Date: Thu, 20 Jul 2017 11:22:43 +0200

Hello,

Theodoros, Julien: could one of you submit an updated patch/patch set
that incorporates what both of you did?

If there are still fine points to discuss, that can always happen at a
later stage.

Thanks,
Ludo’.

Message #17 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: 27461 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, julien <at> lepiller.eu,
 Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: [PATCH v2 1/2] gnu: Add z3.
Date: Tue, 25 Jul 2017 19:11:12 +0300

* gnu/packages/maths.scm (z3): New variable.
* gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs.
---
 gnu/packages/fpga.scm  |  5 ++++-
 gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm
index 420d0aff2..220877577 100644
--- a/gnu/packages/fpga.scm
+++ b/gnu/packages/fpga.scm
@@ -1,6 +1,6 @@
 ;;; GNU Guix --- Functional package management for GNU
 ;;; Copyright © 2016 Danny Milosavljevic <dannym <at> scratchpost.org>
-;;; Copyright © 2016 Theodoros Foradis <theodoros.for <at> openmailbox.org>
+;;; Copyright © 2016, 2017 Theodoros Foradis <theodoros.for <at> openmailbox.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -36,6 +36,7 @@
   #:use-module (gnu packages graphviz)
   #:use-module (gnu packages libffi)
   #:use-module (gnu packages linux)
+  #:use-module (gnu packages maths)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages ghostscript)
   #:use-module (gnu packages gperf)
@@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in the desired format.")
        ("psmisc" ,psmisc)
        ("xdot" ,xdot)
        ("abc" ,abc)))
+    (propagated-inputs
+     `(("z3" ,z3))) ; should be in path for yosys-smtbmc
     (home-page "http://www.clifford.at/yosys/")
     (synopsis "FPGA Verilog RTL synthesizer")
     (description "Yosys synthesizes Verilog-2005.")
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5e4cd8586..536fb9bed 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -18,6 +18,7 @@
 ;;; Copyright © 2017 Paul Garlick <pgarlick <at> tourbillion-technology.com>
 ;;; Copyright © 2017 ng0 <contact.ng0 <at> cryptolab.net>
 ;;; Copyright © 2017 Ben Woodcroft <donttrustben <at> gmail.com>
+;;; Copyright © 2017 Theodoros Foradis <theodoros.for <at> openmailbox.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -3141,3 +3142,36 @@ as equations, scalars, vectors, and matrices.")
     (home-page "https://www.gnu.org/software/jacal/")
     (license license:gpl3+)))
 
+(define-public z3
+  (package
+    (name "z3")
+    (version "4.5.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/Z3Prover/z3/archive/z3-"
+                    version ".tar.gz"))
+              (sha256
+               (base32
+                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (zero?
+              (system* "python" "scripts/mk_make.py"
+                       (string-append "--prefix="
+                                      (assoc-ref outputs "out"))))))
+         (add-after 'configure 'change-dir
+           (lambda _
+             (chdir "build")
+             #t)))))
+    (native-inputs
+     `(("python" ,python-2)))
+    (synopsis "Theorem prover")
+    (description "@code{z3} is a theorem prover.")
+    (home-page "https://github.com/Z3Prover/z3")
+    (license license:expat)))
-- 
2.13.2

Message #20 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: 27461 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, julien <at> lepiller.eu
Subject: [PATCH v2 2/2] gnu: Add python2-z3.
Date: Tue, 25 Jul 2017 19:11:13 +0300

From: Julien Lepiller <julien <at> lepiller.eu>

* gnu/packages/python.scm (python2-z3): New variable.
---
 gnu/packages/python.scm | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/gnu/packages/python.scm b/gnu/packages/python.scm
index 6e1e289e9..b06cbd218 100644
--- a/gnu/packages/python.scm
+++ b/gnu/packages/python.scm
@@ -15512,3 +15512,33 @@ pure Python module.")
 
 (define-public python2-rencode
   (package-with-python2 python-rencode))
+
+(define-public python2-z3
+  (package
+    (inherit z3)
+    (name "python2-z3")
+    (build-system python-build-system)
+    (propagated-inputs
+     `(("z3" ,z3)))
+     (arguments
+      `(#:python ,python-2
+        #:phases
+        (modify-phases %standard-phases
+          (add-before 'build 'prepare
+            (lambda* (#:key inputs #:allow-other-keys)
+              (system* "python" "scripts/mk_make.py")
+              (copy-file "build/python/z3/z3core.py"
+                         "src/api/python/z3/z3core.py")
+              (copy-file "build/python/z3/z3consts.py"
+                         "src/api/python/z3/z3consts.py")
+              (chdir "src/api/python")
+              (substitute* "z3/z3core.py"
+                (("_dirs = \\[")
+                 (string-append "_dirs = ['" (assoc-ref inputs "z3")
+                                "/lib', ")))
+              (substitute* "MANIFEST.in"
+                ((".*") ""))
+              (substitute* "setup.py"
+                (("self.execute\\(.*") "\n")
+                (("scripts=.*") "\n"))
+              #t)))))))
-- 
2.13.2

Message #23 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Cc: julien <at> lepiller.eu, 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3.
Date: Sat, 29 Jul 2017 22:59:56 +0200

Hi Theodoros,

Theodoros Foradis <theodoros.for <at> openmailbox.org> skribis:

> * gnu/packages/maths.scm (z3): New variable.
> * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs.

I splitted it into two patches (because these two things are unrelated),
slightly expounded the z3 description, and committed.

Thanks,
Ludo’.

Message #26 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Cc: julien <at> lepiller.eu, 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH v2 2/2] gnu: Add python2-z3.
Date: Sat, 29 Jul 2017 23:03:14 +0200

Hi,

Theodoros Foradis <theodoros.for <at> openmailbox.org> skribis:

> From: Julien Lepiller <julien <at> lepiller.eu>
>
> * gnu/packages/python.scm (python2-z3): New variable.

[...]

> +(define-public python2-z3
> +  (package
> +    (inherit z3)
> +    (name "python2-z3")

Please add (synopsis "Python bindings to the Z3 theorem prover").

> +    (build-system python-build-system)
> +    (propagated-inputs
> +     `(("z3" ,z3)))

Can we avoid propagating it?

> +     (arguments
> +      `(#:python ,python-2
> +        #:phases
> +        (modify-phases %standard-phases
> +          (add-before 'build 'prepare
> +            (lambda* (#:key inputs #:allow-other-keys)

It would be nice to have comments in this procedure to help understand
what’s going on.

> +              (system* "python" "scripts/mk_make.py")
> +              (copy-file "build/python/z3/z3core.py"
> +                         "src/api/python/z3/z3core.py")
> +              (copy-file "build/python/z3/z3consts.py"
> +                         "src/api/python/z3/z3consts.py")

You can use (install-file "build/python/z3/z3consts.py" "src/api/python/z3").

> +              (chdir "src/api/python")
> +              (substitute* "z3/z3core.py"
> +                (("_dirs = \\[")
> +                 (string-append "_dirs = ['" (assoc-ref inputs "z3")
> +                                "/lib', ")))
> +              (substitute* "MANIFEST.in"
> +                ((".*") ""))
> +              (substitute* "setup.py"
> +                (("self.execute\\(.*") "\n")
> +                (("scripts=.*") "\n"))
> +              #t)))))))

Also, since Z3 already depends on Python, would it make sense to have a
single package?

Thanks,
Ludo’.

Message #29 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Danny Milosavljevic <dannym <at> scratchpost.org>
To: ludo <at> gnu.org (Ludovic Courtès)
Cc: 27461 <at> debbugs.gnu.org, Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3.
Date: Tue, 1 Aug 2017 14:14:25 +0200

z3 fails to build on ARMHF, see <http://hydra.gnu.org/build/2204789/nixlog/1>.

>ld: api/dll/mem_initializer.o: relocation R_ARM_THM_MOVW_ABS_NC against `a local symbol' can not be used when making a shared object; recompile with -fPIC.

There's https://github.com/Z3Prover/z3/issues/585 which says essentially that one should use "cmake", then the problem doesn't appear.

Message #32 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Danny Milosavljevic <dannym <at> scratchpost.org>
Cc: 27461 <at> debbugs.gnu.org, Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3.
Date: Tue, 01 Aug 2017 14:30:18 +0200

Hello,

Danny Milosavljevic <dannym <at> scratchpost.org> skribis:

> z3 fails to build on ARMHF, see <http://hydra.gnu.org/build/2204789/nixlog/1>.
>
>>ld: api/dll/mem_initializer.o: relocation R_ARM_THM_MOVW_ABS_NC against `a local symbol' can not be used when making a shared object; recompile with -fPIC.
>
> There's https://github.com/Z3Prover/z3/issues/585 which says essentially that one should use "cmake", then the problem doesn't appear.

Oh, thanks for the heads-up.

Theodoros, would you consider writing a patch switching from
‘gnu-build-system’ to ‘cmake-build-system’?

Thanks,
Ludo’.

Message #35 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3.
Date: Wed, 02 Aug 2017 13:04:14 +0300

Hello,

> Theodoros, would you consider writing a patch switching from
> ‘gnu-build-system’ to ‘cmake-build-system’?

I am replying with a patch, changing the build system to cmake, and
adding the python bindings in the same package.

The package does not propagate python. I need someone to test the python
bindings, because I am not a python user myself.

Regards,
-- 
Theodoros Foradis

Message #38 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: 27461 <at> debbugs.gnu.org
Cc: dannym <at> scratchpost.org, ludo <at> gnu.org,
 Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: [PATCH] gnu: Add python bindings to z3.
Date: Wed,  2 Aug 2017 13:10:12 +0300

* gnu/packages/maths.scm (z3): Add python bindings.
[build-system]: Change to cmake-build-system.
[arguments]<phases>: Remove "changedir" phase.
                     Add "bootstrap" phase.
[arguments]<configure-flags>: Add them.
[arguments]<tests>: Disable tests.
---
 gnu/packages/maths.scm | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 6566d750b..dfa06b852 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -3174,25 +3174,28 @@ as equations, scalars, vectors, and matrices.")
               (sha256
                (base32
                 "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
-    (build-system gnu-build-system)
+    (build-system cmake-build-system)
     (arguments
-     `(#:test-target "test"
+     `(#:tests? #f ; no tests with cmake
+       #:configure-flags
+       (list "-DBUILD_PYTHON_BINDINGS=true"
+             "-DINSTALL_PYTHON_BINDINGS=true"
+             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+                            %output
+                            "/lib/python2.7/site-packages")
+             (string-append "-DCMAKE_INSTALL_LIBDIR="
+                            %output
+                            "/lib"))
        #:phases
        (modify-phases %standard-phases
-         (replace 'configure
-           (lambda* (#:key inputs outputs #:allow-other-keys)
-             (zero?
-              (system* "python" "scripts/mk_make.py"
-                       (string-append "--prefix="
-                                      (assoc-ref outputs "out"))))))
-         (add-after 'configure 'change-dir
+         (add-before 'configure 'bootstrap
            (lambda _
-             (chdir "build")
-             #t)))))
+             (zero?
+              (system* "python" "contrib/cmake/bootstrap.py" "create")))))))
     (native-inputs
      `(("python" ,python-2)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
-theories} (SMT) solver.  It provides a C/C++ API.")
+theories} (SMT) solver.  It provides a C/C++ API, as well as python bindings.")
     (home-page "https://github.com/Z3Prover/z3")
     (license license:expat)))
-- 
2.13.2

Message #43 received at 27461-done <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Cc: 27461-done <at> debbugs.gnu.org, dannym <at> scratchpost.org
Subject: Re: [PATCH] gnu: Add python bindings to z3.
Date: Mon, 21 Aug 2017 17:14:00 +0200

Hi Theodoros,

And sorry for the long delay!

Theodoros Foradis <theodoros.for <at> openmailbox.org> skribis:

> * gnu/packages/maths.scm (z3): Add python bindings.
> [build-system]: Change to cmake-build-system.
> [arguments]<phases>: Remove "changedir" phase.
>                      Add "bootstrap" phase.
> [arguments]<configure-flags>: Add them.
> [arguments]<tests>: Disable tests.

I’ve applied this patch with a few modifications, in particular
arranging to run the tests (disabling them altogether was not OK since
we knew there is a test suite):

  https://git.savannah.gnu.org/cgit/guix.git/commit/?id=cf684d87d7446ffe33ca4c73bf51dc24fa5a7129

Thanks,
Ludo’.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.