From: Theodoros Foradis <theodoros.for@openmailbox.org>
To: julien lepiller <julien@lepiller.eu>
Cc: 27461@debbugs.gnu.org
Subject: [bug#27461] [PATCH] gnu: Add z3.
Date: Mon, 26 Jun 2017 19:31:15 +0300 [thread overview]
Message-ID: <87efu6r9s6.fsf@openmailbox.org> (raw)
In-Reply-To: <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu>
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
next prev parent reply other threads:[~2017-06-26 17:15 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-06-23 15:50 [bug#27461] [PATCH] gnu: Add z3 Theodoros Foradis
2017-06-25 8:19 ` julien lepiller
2017-06-26 16:31 ` Theodoros Foradis [this message]
2017-07-20 9:22 ` Ludovic Courtès
2017-07-25 16:11 ` [bug#27461] [PATCH v2 1/2] " Theodoros Foradis
2017-07-25 16:11 ` [bug#27461] [PATCH v2 2/2] gnu: Add python2-z3 Theodoros Foradis
2017-07-29 21:03 ` Ludovic Courtès
2017-07-29 20:59 ` [bug#27461] [PATCH v2 1/2] gnu: Add z3 Ludovic Courtès
2017-08-01 12:14 ` Danny Milosavljevic
2017-08-01 12:30 ` Ludovic Courtès
2017-08-02 10:04 ` Theodoros Foradis
2017-08-02 10:10 ` [bug#27461] [PATCH] gnu: Add python bindings to z3 Theodoros Foradis
2017-08-21 15:14 ` bug#27461: " Ludovic Courtès
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87efu6r9s6.fsf@openmailbox.org \
--to=theodoros.for@openmailbox.org \
--cc=27461@debbugs.gnu.org \
--cc=julien@lepiller.eu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.