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

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: bug#27461: closed (Re: [PATCH] gnu: Add python bindings to z3.)
Date: Mon, 21 Aug 2017 15:15:02 +0000

[Message part 1 (text/plain, inline)]

Your bug report

#27461: [PATCH] gnu: Add z3.

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 27461 <at> debbugs.gnu.org.

-- 
27461: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=27461
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

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’.

[Message part 3 (message/rfc822, inline)]

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

Previous Next

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