added community/z3

This commit is contained in:
Kevin Mihelich 2018-11-06 20:20:32 +00:00
parent 84318708c7
commit 8e5e9f6fdf
2 changed files with 124 additions and 0 deletions

75
community/z3/PKGBUILD Normal file
View file

@ -0,0 +1,75 @@
# Maintainer: Felix Yan <felixonmars@archlinux.org>
# Maintainer: Levente Polyak <anthraxx[at]archlinux[dot]org>
# Contributor: rudy.matela
# ALARM: Kevin Mihelich <kevin@archlinuxarm.org>
# - patch from Fedora to fix ARM FTBFS
pkgbase=z3
pkgname=('z3' 'python-z3' 'python2-z3')
pkgver=4.8.1
pkgrel=1
pkgdesc='High-performance theorem prover'
url='https://github.com/Z3Prover/z3'
arch=('x86_64')
license=('MIT')
# 'java-environment-common' 'mono' 'ocaml' 'ocaml-findlib'
makedepends=('cmake' 'python2' 'python2-setuptools' 'python' 'python-setuptools' 'gcc-libs' 'gmp')
optdepends=('python2-setuptools: bindings for python2')
source=(https://github.com/Z3Prover/z3/archive/${pkgbase}-${pkgver}.tar.gz
z3-no-sse.patch)
sha512sums=('f3311d07f6375d3d294d9c495b0ce4022258dd95b1f6bec93bdf5a60d074c75fd13daf1da7b67753acb4084e33395088513dfd85fe5c2cf76913ba0107e5782b'
'd172454a024eae2ac2246de481349ac61d9d9fdf41b5b0bb8b9343f74c5232c5f74458e30e16d745af9ad99e9aa4444627248bdb29b86d437471fd97bbba96b3')
prepare() {
cd ${pkgbase}-${pkgbase}-${pkgver}
mkdir -p build
patch -p0 -i ../z3-no-sse.patch
}
build() {
cd ${pkgbase}-${pkgbase}-${pkgver}/build
cmake .. \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_INSTALL_PREFIX=/usr \
-DCMAKE_INSTALL_LIBDIR=lib \
-DBUILD_PYTHON_BINDINGS=1 \
-DPYTHON_EXECUTABLE=/usr/bin/python \
-DUSE_LIB_GMP=1
make
}
package_z3() {
depends=('gcc-libs' 'gmp')
provides=('libz3' 'libz3.so')
cd ${pkgbase}-${pkgbase}-${pkgver}/build
make DESTDIR="${pkgdir}" install
install -Dm 644 ../LICENSE.txt -t "${pkgdir}/usr/share/licenses/${pkgname}"
rm -r "${pkgdir}"/usr/lib/python*
}
package_python-z3() {
depends=('python' 'libz3')
cd ${pkgbase}-${pkgbase}-${pkgver}/build
make DESTDIR="${pkgdir}" install
install -Dm 644 ../LICENSE.txt -t "${pkgdir}/usr/share/licenses/${pkgname}"
cd "${pkgdir}"
rm -r usr/include usr/bin usr/lib/cmake usr/lib/lib*
python -m compileall .
python -O -m compileall .
}
package_python2-z3() {
depends=('python2' 'libz3')
cd ${pkgbase}-${pkgbase}-${pkgver}/build
make DESTDIR="${pkgdir}" install
install -Dm 644 ../LICENSE.txt -t "${pkgdir}/usr/share/licenses/${pkgname}"
cd "${pkgdir}"
rm -r usr/include usr/bin usr/lib/cmake usr/lib/lib*
mv usr/lib/python* usr/lib/python2.7
[ -n "${SOURCE_DATE_EPOCH}" ] && find . -exec touch -h -d @$SOURCE_DATE_EPOCH {} +
python2 -m compileall .
python2 -O -m compileall .
}
# vim: ts=2 sw=2 et:

View file

@ -0,0 +1,49 @@
--- scripts/mk_util.py.orig 2018-10-15 13:52:38.000000000 -0600
+++ scripts/mk_util.py 2018-10-31 19:27:59.067093823 -0600
@@ -112,7 +112,7 @@ GUARD_CF=False
ALWAYS_DYNAMIC_BASE=False
FPMATH="Default"
-FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
+FPMATH_FLAGS=""
def check_output(cmd):
@@ -294,10 +294,10 @@ def test_fpmath(cc):
t = TempFile('tstsse.cpp')
t.add('int main() { return 42; }\n')
t.commit()
- if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
+ if None:
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
return "SSE2-GCC"
- elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
+ elif None:
FPMATH_FLAGS="-msse -msse2"
return "SSE2-CLANG"
elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
--- src/util/hwf.cpp.orig 2018-10-15 13:52:38.000000000 -0600
+++ src/util/hwf.cpp 2018-10-31 19:28:42.528890124 -0600
@@ -46,9 +46,9 @@ Revision History:
// clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
// the x87 FPU, even when /arch:SSE2 is on.
// Luckily, these are kind of standardized, at least for Windows/Linux/macOS.
-#ifdef __clang__
+//#ifdef __clang__
#undef USE_INTRINSICS
-#endif
+//#endif
#ifdef USE_INTRINSICS
#include <emmintrin.h>
--- src/util/mpz.cpp.orig 2018-10-15 13:52:38.000000000 -0600
+++ src/util/mpz.cpp 2018-10-31 19:40:55.519174699 -0600
@@ -30,7 +30,7 @@ Revision History:
#else
#error No multi-precision library selected.
#endif
-#include <immintrin.h>
+
// Available GCD algorithms
// #define EUCLID_GCD