diff options
| -rw-r--r-- | licenses/MSR-LA | 104 | ||||
| -rw-r--r-- | sci-mathematics/z3/ChangeLog | 10 | ||||
| -rw-r--r-- | sci-mathematics/z3/Manifest | 1 | ||||
| -rw-r--r-- | sci-mathematics/z3/metadata.xml | 5 | ||||
| -rw-r--r-- | sci-mathematics/z3/z3-4.3.1.ebuild | 75 | ||||
| -rw-r--r-- | sci-mathematics/z3/z3-9999.ebuild | 81 |
6 files changed, 276 insertions, 0 deletions
diff --git a/licenses/MSR-LA b/licenses/MSR-LA new file mode 100644 index 000000000..2b25654cf --- /dev/null +++ b/licenses/MSR-LA @@ -0,0 +1,104 @@ +Microsoft Research License Agreement +Non-Commercial Use Only +Z3 +_____________________________________________________________________ +This Microsoft Research License Agreement, including all exhibits ("MSR-LA") is +a legal agreement between you and Microsoft Corporation ("Microsoft" or "we") +for the data identified above, which may include associated materials, text or +speech files, associated media and "online" or electronic documentation and any +updates we provide in our discretion (together, the "Software"). + +By installing, copying, or otherwise using this Software, you agree to be bound +by the terms of this MSR-LA. If you do not agree, do not install copy or use the +Software. The Software is protected by copyright and other intellectual property +laws and is licensed, not sold. + +SCOPE OF RIGHTS: +You may use, copy, reproduce, and distribute this Software for any +non-commercial purpose, subject to the restrictions in this MSR-LA. Some +purposes which can be non-commercial are teaching, academic research, public +demonstrations and personal experimentation. You may also distribute this +Software with books or other teaching materials, or publish the Software on +Websites, that are intended to teach the use of the Software for academic or +other non-commercial purposes. + +You may not use or distribute this Software or any derivative works in any form +for commercial purposes. Examples of commercial purposes would be running +business operations, licensing, leasing, or selling the Software, distributing +the Software for use with commercial products, using the Software in the +creation or use of commercial products or any other activity which purpose is +to procure a commercial gain to you or others. + +You may create derivative works of the Software source code and distribute the +modified Software solely for non-commercial academic purposes, as provided +herein. If you distribute the Software or any derivative works of the Software, +you will distribute them under the same terms and conditions as in this +license, and you will not grant other rights to the Software or derivative +works that are different from those provided by this MSR-LA. + +If you have created derivative works of the Software, and distribute such +derivative works, you will cause the modified files to carry prominent notices +so that recipients know that they are not receiving the original Software. Such +notices must state: (i) that you have changed the Software; and (ii) the date +of any changes. +In return, we simply require that you agree: + +1. That you will not remove any copyright or other notices from the Software. + +2. That if any of the Software is in binary format, you will not attempt to +modify such portions of the Software, or to reverse engineer or decompile them, +except and only to the extent authorized by applicable law. + +3. That Microsoft is granted back, without any restrictions or limitations, a +non-exclusive, perpetual, irrevocable, royalty-free, assignable and +sub-licensable license, to reproduce, publicly perform or display, install, +use, modify, post, distribute, make and have made, sell and transfer your +modifications to and/or derivative works of the Software source code or data, +for any purpose. + +4. That any feedback about the Software provided by you to us is voluntarily +given, and Microsoft shall be free to use the feedback as it sees fit without +obligation or restriction of any kind, even if the feedback is designated by +you as confidential. + +5. THAT THE SOFTWARE COMES "AS IS", WITH NO WARRANTIES. THIS MEANS NO EXPRESS, +IMPLIED OR STATUTORY WARRANTY, INCLUDING WITHOUT LIMITATION, WARRANTIES OF +MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE, ANY WARRANTY AGAINST +INTERFERENCE WITH YOUR ENJOYMENT OF THE SOFTWARE OR ANY WARRANTY OF TITLE OR +NON-INFRINGEMENT. THERE IS NO WARRANTY THAT THIS SOFTWARE WILL FULFILL ANY OF +YOUR PARTICULAR PURPOSES OR NEEDS. ALSO, YOU MUST PASS THIS DISCLAIMER ON +WHENEVER YOU DISTRIBUTE THE SOFTWARE OR DERIVATIVE WORKS. + +6. THAT NEITHER MICROSOFT NOR ANY CONTRIBUTOR TO THE SOFTWARE WILL BE LIABLE +FOR ANY DAMAGES RELATED TO THE SOFTWARE OR THIS MSR-LA, INCLUDING DIRECT, +INDIRECT, SPECIAL, CONSEQUENTIAL OR INCIDENTAL DAMAGES, TO THE MAXIMUM EXTENT +THE LAW PERMITS, NO MATTER WHAT LEGAL THEORY IT IS BASED ON. ALSO, YOU MUST +PASS THIS LIMITATION OF LIABILITY ON WHENEVER YOU DISTRIBUTE THE SOFTWARE OR +DERIVATIVE WORKS. + +7. That we have no duty of reasonable care or lack of negligence, and we are +not obligated to (and will not) provide technical support for the Software. + +8. That if you breach this MSR-LA or if you sue anyone over patents that you +think may apply to or read on the Software or anyone's use of the Software, +this MSR-LA (and your license and rights obtained herein) terminate +automatically. Upon any such termination, you shall destroy all of your copies +of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this +MSR-LA shall survive any termination of this MSR-LA. + +9. That the patent rights, if any, granted to you in this MSR-LA only apply to +the Software, not to any derivative works you make. + +10. That the Software may be subject to U.S. export jurisdiction at the time it +is licensed to you, and it may be subject to additional export or import laws +in other places. You agree to comply with all such laws and regulations that +may apply to the Software after delivery of the Software to you. + +11. That all rights not expressly granted to you in this MSR-LA are reserved. + +12. That this MSR-LA shall be construed and controlled by the laws of the State +of Washington, USA, without regard to conflicts of law. If any provision of +this MSR-LA shall be deemed unenforceable or contrary to law, the rest of this +MSR-LA shall remain in full effect and interpreted in an enforceable manner +that most nearly captures the intent of the original language. + diff --git a/sci-mathematics/z3/ChangeLog b/sci-mathematics/z3/ChangeLog new file mode 100644 index 000000000..a078c2ad6 --- /dev/null +++ b/sci-mathematics/z3/ChangeLog @@ -0,0 +1,10 @@ +# ChangeLog for sci-mathematics/z3 +# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2 +# $Header: $ + + 02 Dec 2013; Justin Lecher <jlec@gentoo.org> z3-4.3.1.ebuild, z3-9999.ebuild, + +metadata.xml: + Make build verbose; respect CXX, CXXFLAGS, LDFLAGS; use EPYTHON instead of a + direct python call; check for openmp compatibility of the c++ compiler; add + USE=gmp; drop unnecessary eclass; add missing metadata.xml + diff --git a/sci-mathematics/z3/Manifest b/sci-mathematics/z3/Manifest new file mode 100644 index 000000000..109db81fd --- /dev/null +++ b/sci-mathematics/z3/Manifest @@ -0,0 +1 @@ +DIST z3-4.3.1.tar.xz 1841796 SHA256 db36d7c96e506a08c3a7967340983edb298dcb0d33be5dab064c36f4e9cf6ee8 SHA512 ccffb07c6468911685db28030e012a6504c2ce5d50b33163cfac0f12bdbd25b5365b39e61ad514ede01bc138cbc7004de6a9efa6264bc5d2f9fc8db63c989c91 WHIRLPOOL 30fac04a772a5fee2d8d468f7620d858374578561da0aba5971e09f95713fb275c6695b8c1bb5a8c01c3781d7db65423d3d194a52ea398b423e90198a4ce22b5 diff --git a/sci-mathematics/z3/metadata.xml b/sci-mathematics/z3/metadata.xml new file mode 100644 index 000000000..897aa2e6b --- /dev/null +++ b/sci-mathematics/z3/metadata.xml @@ -0,0 +1,5 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> +<pkgmetadata> + <herd>sci</herd> +</pkgmetadata> diff --git a/sci-mathematics/z3/z3-4.3.1.ebuild b/sci-mathematics/z3/z3-4.3.1.ebuild new file mode 100644 index 000000000..adf4f6eda --- /dev/null +++ b/sci-mathematics/z3/z3-4.3.1.ebuild @@ -0,0 +1,75 @@ +# Copyright 1999-2013 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +EAPI=5 + +PYTHON_COMPAT=( python2_7 ) + +inherit autotools flag-o-matic python-r1 toolchain-funcs vcs-snapshot + +DESCRIPTION="An efficient theorem prover" +HOMEPAGE="http://z3.codeplex.com/" +SRC_URI="http://dev.gentoo.org/~jlec/distfiles/${P}.tar.xz" + +SLOT="0" +LICENSE="MSR-LA" +KEYWORDS="~amd64 ~x86" +IUSE="gmp" + +REQUIRED_USE="${PYTHON_REQUIRED_USE}" + +RDEPEND="${PYTHON_DEPS} + gmp? ( dev-libs/gmp )" +DEPEND="${RDEPEND}" + +pkg_setup() { + if [[ ${MERGE_TYPE} != binary ]]; then + if [[ $(tc-getCXX)$ == *g++* ]] && ! tc-has-openmp; then + ewarn "Please use an openmp compatible compiler" + ewarn "like >gcc-4.2 with USE=openmp" + die "Openmp support missing in compiler" + fi + fi +} + +src_prepare() { + sed \ + -e 's:-O3::g' \ + -e 's:-fomit-frame-pointer::' \ + -e 's:-msse2::g' \ + -e 's:-msse::g' \ + -e "/LINK_EXTRA_FLAGS/s:@LDFLAGS@:-lrt $(usex gmp -lgmp):g" \ + -e 's:t@\$:t\$:g' \ + -i scripts/*mk* || die + + append-ldflags -fopenmp + + eautoreconf +} + +src_configure() { + python_export_best + econf \ + --host="" \ + --with-python="${PYTHON}" \ + $(use_with gmp) \ + SLIBFLAGS=" -Wl,-soname,lib${PN}.so.0.1 " + ${EPYTHON} scripts/mk_make.py || die +} + +src_compile() { + emake \ + --directory="build" \ + CXX=$(tc-getCXX) \ + LINK="$(tc-getCXX) ${LDFLAGS}" \ + LINK_FLAGS="${LDFLAGS}" +} + +src_install() { + doheader src/api/z3*.h src/api/c++/z3*.h + dolib.so build/*.so + dobin build/z3 + + python_foreach_impl python_domodule src/api/python/*.py +} diff --git a/sci-mathematics/z3/z3-9999.ebuild b/sci-mathematics/z3/z3-9999.ebuild new file mode 100644 index 000000000..15c338b4f --- /dev/null +++ b/sci-mathematics/z3/z3-9999.ebuild @@ -0,0 +1,81 @@ +# Copyright 1999-2013 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +EAPI=5 + +PYTHON_COMPAT=( python2_7 ) + +inherit autotools flag-o-matic git-r3 python-r1 toolchain-funcs + +DESCRIPTION="An efficient theorem prover" +HOMEPAGE="http://z3.codeplex.com/" +SRC_URI="" +EGIT_REPO_URI="https://git01.codeplex.com/z3" + +SLOT="0" +LICENSE="MSR-LA" +KEYWORDS="" +IUSE="gmp" + +REQUIRED_USE="${PYTHON_REQUIRED_USE}" + +RDEPEND="${PYTHON_DEPS} + gmp? ( dev-libs/gmp )" +# A new curl is needed because codeplex has a bug and early version of libcurl +# will cause a failed git clone. +DEPEND="${RDEPEND} + >=net-misc/curl-7.33" + +EGIT_NONSHALLOW=1 + +pkg_setup() { + if [[ ${MERGE_TYPE} != binary ]]; then + if [[ $(tc-getCXX)$ == *g++* ]] && ! tc-has-openmp; then + ewarn "Please use an openmp compatible compiler" + ewarn "like >gcc-4.2 with USE=openmp" + die "Openmp support missing in compiler" + fi + fi +} + +src_prepare() { + sed \ + -e 's:-O3::g' \ + -e 's:-fomit-frame-pointer::' \ + -e 's:-msse2::g' \ + -e 's:-msse::g' \ + -e "/LINK_EXTRA_FLAGS/s:@LDFLAGS@:-lrt $(usex gmp -lgmp):g" \ + -e 's:t@\$:t\$:g' \ + -i scripts/*mk* || die + + append-ldflags -fopenmp + + eautoreconf +} + +src_configure() { + python_export_best + econf \ + --host="" \ + --with-python="${PYTHON}" \ + $(use_with gmp) \ + SLIBFLAGS=" -Wl,-soname,lib${PN}.so.0.1 " + ${EPYTHON} scripts/mk_make.py || die +} + +src_compile() { + emake \ + --directory="build" \ + CXX=$(tc-getCXX) \ + LINK="$(tc-getCXX) ${LDFLAGS}" \ + LINK_FLAGS="${LDFLAGS}" +} + +src_install() { + doheader src/api/z3*.h src/api/c++/z3*.h + dolib.so build/*.so + dobin build/z3 + + python_foreach_impl python_domodule src/api/python/*.py +} |