Package Details: z3-git 4.5.0.r1325.g05c4ea82-1

Git Clone URL: https://aur.archlinux.org/z3-git.git (read-only)
Package Base: z3-git
Description: Z3 is a high-performance theorem prover being developed at Microsoft Research
Upstream URL: https://github.com/Z3Prover/z3
Licenses: MIT
Conflicts: z3, z3-bin, z3-codeplex
Provides: z3
Submitter: d.woffinden
Maintainer: d.woffinden
Last Packager: d.woffinden
Votes: 8
Popularity: 0.561946
First Submitted: 2014-03-02 03:55
Last Updated: 2017-08-06 00:15

Dependencies (4)

Required by (8)

Sources (1)

Latest Comments

wbthomason commented on 2017-10-30 22:29

@d.woffinden: Though I've modified the PKGBUILD to make the OCaml bindings for myself (at least, I think - it generates OCaml .cmx files, but I can't seem to open the Z3 module in the OCaml top level), it would be useful if this package generated OCaml bindings (in reference to your comment below).

d.woffinden commented on 2017-08-06 00:18

Seems to work for me now, probably just a bad upstream revision?

hans_jschmid commented on 2017-05-01 09:47

Getting compiler error:

src/ast/simplifier/seq_simplifier_plugin.cpp
In file included from ../src/util/trace.h:31:0,
from ../src/util/mpz.h:26,
from ../src/util/mpq.h:22,
from ../src/util/rational.h:22,
from ../src/ast/ast.h:26,
from ../src/ast/simplifier/simplifier_plugin.h:21,
from ../src/ast/simplifier/basic_simplifier_plugin.h:20,
from ../src/ast/simplifier/seq_simplifier_plugin.h:20,
from ../src/ast/simplifier/seq_simplifier_plugin.cpp:17:
/usr/include/c++/6.3.1/fstream: In Elementfunktion »bool std::basic_filebuf<_CharT, _Traits>::is_open() const«:
/usr/include/c++/6.3.1/fstream:253:16: interner Compiler-Fehler: Speicherzugriffsfehler
{ return _M_file.is_open(); }
^~~~~~~
Bitte senden Sie einen vollständigen Fehlerbericht auf Englisch ein;
inclusive vorverarbeitetem Quellcode, wenn es dienlich ist.
Siehe <https://bugs.archlinux.org/> für nähere Anweisungen.
make: *** [Makefile:1873: ast/simplifier/seq_simplifier_plugin.o] Fehler 1
==> FEHLER: Ein Fehler geschah in build().
Breche ab...
==> FEHLER:Makepkg konnte z3-git nicht erstellen.
==> Erstellen von z3-git neu starten?[j/N]
==> --------------------------------------

d.woffinden commented on 2016-05-23 21:03

Should be fixed now, thanks. Apologies for the delay.

FYI, the python bindings are now for python (3.5) rather than python2 (2.7). If anybody needs bindings for other languages (Java, .NET, OCaml) for this package, let me know.

mickael9 commented on 2016-05-22 21:54

Here is a working PKGBUILD: https://gist.github.com/mickael9/7c09e267e71cc259f21449dbdee015cf

kaptoxic commented on 2016-05-07 21:40

Same here (as bastelfreak).

bastelfreak commented on 2016-03-27 17:14

Hi,

the current pkgbuild doesnt, build:
mv: cannot stat '/build/z3-git/pkg/z3-git/usr/lib/python2.7/dist-packages': No such file or directory

https://ci.virtapi.org/view/Arch%20Package%20Continuous%20Delivery/job/Arch_Package_z3-git/1/console

Grollicus commented on 2015-12-10 20:54

use python2 scripts/mk_make.py --prefix="$pkgdir/usr" --pypkgdir="$pkgdir/usr/lib/python2.7/site-packages"

instead of python2 scripts/mk_make.py --prefix="$pkgdir/usr"

otherwise mk_make will skip python bindings. Also saves the mv from dist-packages to site-packages.

Also I did add
sed -i "s/return str(version_string).find('clang') != -1/return unicode(version_string).find('clang') != -1/g" "$srcdir/$pkgname/scripts/mk_util.py"
in build() because of strange locale issues: gcc --version prints umlauts in german. But thats just a note, maybe some other germans run into this strange problem.

d.woffinden commented on 2014-11-14 20:12

Fixed and updated, thanks mw0 :)

mw0 commented on 2014-11-14 12:09

Hey, I tried to build this package today, and generating the Makefile with autoconf+configure failed for me.

According to https://z3.codeplex.com/SourceControl/latest this has to be build just with:

python2 scripts/mk_make.py
cd "$srcdir/$pkgname/build
make

instead of

autoconf
./configure --with-python=/usr/bin/python2
python2 scripts/mk_make.py
cd "$srcdir/$pkgname/build
make

All comments