pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
[pkgsrc/trunk]: pkgsrc/math/yices2 Initial import of Yices 2, version 2.6.1.
details: https://anonhg.NetBSD.org/pkgsrc/rev/eb174c755593
branches: trunk
changeset: 338438:eb174c755593
user: alnsn <alnsn%pkgsrc.org@localhost>
date: Sat Aug 24 22:09:16 2019 +0000
description:
Initial import of Yices 2, version 2.6.1.
Yices 2 is an SMT solver that decides the satisfiability of formulas
containing uninterpreted function symbols with equality, real and
integer arithmetic, bitvectors, scalar types, and tuples. Yices 2
supports both linear and nonlinear arithmetic.
Yices 2 can process input written in the SMT-LIB notation (both
versions 2.0 and 1.2 are supported). Alternatively, you can write
specifications using Yices 2's own specification language, which
includes tuples and scalar types. You can also use Yices 2 as a
library in your software.
diffstat:
math/yices2/DESCR | 10 ++
math/yices2/Makefile | 30 ++++++
math/yices2/PLIST | 11 ++
math/yices2/buildlink3.mk | 15 +++
math/yices2/distinfo | 11 ++
math/yices2/patches/patch-Makefile.build | 42 ++++++++
math/yices2/patches/patch-autoconf_os | 15 +++
math/yices2/patches/patch-configure.ac | 103 ++++++++++++++++++++++
math/yices2/patches/patch-src_Makefile | 42 ++++++++
math/yices2/patches/patch-src_utils_bit__tricks.h | 82 +++++++++++++++++
10 files changed, 361 insertions(+), 0 deletions(-)
diffs (truncated from 401 to 300 lines):
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/DESCR
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/DESCR Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,10 @@
+Yices 2 is an SMT solver that decides the satisfiability of formulas
+containing uninterpreted function symbols with equality, real and
+integer arithmetic, bitvectors, scalar types, and tuples. Yices 2
+supports both linear and nonlinear arithmetic.
+
+Yices 2 can process input written in the SMT-LIB notation (both
+versions 2.0 and 1.2 are supported). Alternatively, you can write
+specifications using Yices 2's own specification language, which
+includes tuples and scalar types. You can also use Yices 2 as a
+library in your software.
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/Makefile
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/Makefile Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,30 @@
+# $NetBSD: Makefile,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+PKGNAME= yices2-2.6.1
+DISTNAME= Yices-${PKGVERSION}
+GITHUB_TAG= ${DISTNAME}
+CATEGORIES= math
+MASTER_SITES= ${MASTER_SITE_GITHUB:=SRI-CSL/}
+
+MAINTAINER= alnsn%NetBSD.org@localhost
+HOMEPAGE= https://yices.csl.sri.com/
+COMMENT= Yices 2 SMT solver
+LICENSE= gnu-gpl-v3
+
+BUILD_DEPENDS+= gperf-[0-9]*:../../devel/gperf
+
+USE_TOOLS+= autoconf gmake
+USE_LANGUAGES= c
+GNU_CONFIGURE= yes
+USE_GNU_CONFIGURE_HOST= no
+
+WRKSRC= ${WRKDIR}/yices2-${DISTNAME}
+
+pre-configure:
+ cd ${WRKSRC} && autoconf
+
+pre-install:
+ cd ${WRKSRC} && make dist
+
+.include "../../devel/gmp/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/PLIST
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/PLIST Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,11 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+bin/yices
+bin/yices-sat
+bin/yices-smt
+bin/yices-smt2
+include/yices.h
+include/yices_exit_codes.h
+include/yices_limits.h
+include/yices_types.h
+lib/libyices.so
+lib/libyices.so.${PKGVERSION}
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/buildlink3.mk
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/buildlink3.mk Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,15 @@
+# $NetBSD: buildlink3.mk,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+BUILDLINK_TREE+= yices2
+
+.if !defined(YICES2_BUILDLINK3_MK)
+YICES2_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.yices2+= yices2>=2.6.1
+BUILDLINK_ABI_DEPENDS.yices2+= yices2>=2.6.1
+BUILDLINK_PKGSRCDIR.yices2?= ../../math/yices2
+.endif # YICES2_BUILDLINK3_MK
+
+.include "../../devel/gmp/buildlink3.mk"
+
+BUILDLINK_TREE+= -yices2
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/distinfo
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/distinfo Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,11 @@
+$NetBSD: distinfo,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+SHA1 (Yices-2.6.1.tar.gz) = 472c4eb7dadc3e8de30495389f50ad3aa09baa08
+RMD160 (Yices-2.6.1.tar.gz) = 337faea5f2963998a93645f5b1abb4830f5dc1b8
+SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2
+Size (Yices-2.6.1.tar.gz) = 8903749 bytes
+SHA1 (patch-Makefile.build) = 64c6ae7101c6dd20f455e7575ce8c59fd518152a
+SHA1 (patch-autoconf_os) = fd055ab19f49921aece028df67668613ae089b3c
+SHA1 (patch-configure.ac) = 5c4579cfd0e6cc1d6f9a1315f0b4db28048febb0
+SHA1 (patch-src_Makefile) = 38bb8236d9eacd919c8afc3ed5ae0c9ea1b0233a
+SHA1 (patch-src_utils_bit__tricks.h) = 0abcd0244cb55e7889aab3550af6c25ae3c88850
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/patches/patch-Makefile.build
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/patches/patch-Makefile.build Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,42 @@
+$NetBSD: patch-Makefile.build,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD targets, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- Makefile.build.orig 2018-10-26 21:33:09.000000000 +0000
++++ Makefile.build
+@@ -213,14 +213,14 @@ build_subdirs: $(build_dir) $(dyn_objsub
+
+ static_build_subdirs-mingw static_build_subdirs-cygwin: $(static_dll_objsubdirs)
+
+-static_build_subdirs-darwin static_build_subdirs-linux static_build_subdirs-unix static_build_subdirs-freebsd:
++static_build_subdirs-darwin static_build_subdirs-linux static_build_subdirs-unix static_build_subdirs-freebsd static_build_subdirs-netbsd:
+
+ static_build_subdirs: $(build_dir) $(static_objsubdirs) $(static_libdir) $(static_bindir) \
+ static_build_subdirs-$(POSIXOS)
+
+ .PHONY: build_subdirs static_build_subdirs static_build_subdirs-darwin static-build_subdirs-cygwin \
+ static_build_subdirs-mingw static_build_subdirs-linux static_build_subdirs-unix \
+- static_build_subdirs-freebsd
++ static_build_subdirs-freebsd static_build_subdirs-netbsd
+
+ #
+ # Compilation
+@@ -485,6 +485,9 @@ install-linux install-unix: install-defa
+ install-freebsd: install-default
+ $(LDCONFIG) -m $(DESTDIR)$(libdir) && (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(MAJOR).$(MINOR) libyices.so)
+
++install-netbsd: install-default
++ (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(YICES_VERSION) libyices.so)
++
+ #
+ # cygwin and mingw install: copy the DLLs in $(bindir)
+ #
+@@ -500,7 +503,7 @@ install-mingw: install-cygwin
+
+
+ .PHONY: install install-default install-darwin install-solaris \
+- install-linux install-freebsd install-unix \
++ install-linux install-freebsd install-netbsd install-unix \
+ install-cygwin install-mingw
+
+
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/patches/patch-autoconf_os
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/patches/patch-autoconf_os Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,15 @@
+$NetBSD: patch-autoconf_os,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- autoconf/os.orig 2018-10-26 21:33:09.000000000 +0000
++++ autoconf/os
+@@ -13,6 +13,8 @@ if eval 'uname > /dev/null 2> /dev/null'
+ echo "mingw";;
+ FreeBSD*)
+ echo "freebsd";;
++ NetBSD*)
++ echo "netbsd";;
+ *)
+ echo "unix";;
+ esac
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/patches/patch-configure.ac
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/patches/patch-configure.ac Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,103 @@
+$NetBSD: patch-configure.ac,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Fix "=" comparisons, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- configure.ac.orig 2018-10-26 21:33:09.000000000 +0000
++++ configure.ac
+@@ -191,7 +191,7 @@ dnl
+ static_libgmp=""
+ AC_ARG_WITH([static-gmp],
+ [AS_HELP_STRING([--with-static-gmp=<path>],[Full path to a static GMP library (e.g., libgmp.a)])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-gmp was used but no path was given. Using defaults])
+ else
+ static_libgmp=$withval
+@@ -203,7 +203,7 @@ static_includegmp=""
+ AC_ARG_WITH([static-gmp-include-dir],
+ [AS_HELP_STRING([--with-static-gmp-include-dir=<directory>],
+ [Directory of include file "gmp.h" compatible with static GMP library])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-gmp-include-dir was used but no directory was given. Using defaults])
+ else
+ static_includegmp=$withval
+@@ -215,7 +215,7 @@ AC_ARG_WITH([static-gmp-include-dir],
+ pic_libgmp=""
+ AC_ARG_WITH([pic-gmp],
+ [AS_HELP_STRING([--with-pic-gmp=<path>],[Full path to a relocatable GMP library (e.g., libgmp.a)])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-gmp was used but no path was given. Using defaults])
+ else
+ pic_libgmp=$withval
+@@ -227,7 +227,7 @@ pic_includegmp=""
+ AC_ARG_WITH([pic-gmp-include-dir],
+ [AS_HELP_STRING([--with-pic-gmp-include-dir=<directory>],
+ [Directory of include file "gmp.h" compatible with relocatable GMP library])],
+- [if test "x$withval" == x; then
++ [if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-gmp-include-dir was used but no directory was given. Using defaults])
+ else
+ pic_includegmp=$withval
+@@ -257,10 +257,10 @@ AC_ARG_ENABLE([mcsat],
+ static_lpoly=""
+ AC_ARG_WITH([static-libpoly],
+ [AS_HELP_STRING([--with-static-libpoly=<path>],[Full path to libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-static-libpoly since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-poly was used but no path was given. Using defaults])
+ else
+ static_lpoly=$withval
+@@ -273,10 +273,10 @@ static_includelpoly=""
+ AC_ARG_WITH([static-libpoly-include-dir],
+ [AS_HELP_STRING([--with-static-libpoly-include-dir=<directory>],
+ [Path to include files compatible with libpoly.a (e.g., /usr/local/include)])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-static-libpoly-include-dir since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-static-libpoly-include-dir was used but no directory was given. Using defaults])
+ else
+ static_includelpoly=$withval
+@@ -289,10 +289,10 @@ AC_ARG_WITH([static-libpoly-include-dir]
+ pic_lpoly=""
+ AC_ARG_WITH([pic-libpoly],
+ [AS_HELP_STRING([--with-pic-libpoly=<path>],[Full path to a relocatable libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-pic-libpoly since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-libpoly was used but no path was given. Using defaults])
+ else
+ pic_lpoly=$withval
+@@ -305,10 +305,10 @@ pic_includelpoly=""
+ AC_ARG_WITH([pic-libpoly-include-dir],
+ [AS_HELP_STRING([--with-pic-libpoly-include-dir=<directory>],
+ [Path to include files compatible with the relocatable libpoly.a])],
+- [if test $use_mcsat == "no" ; then
++ [if test $use_mcsat = "no" ; then
+ AC_MSG_WARN([Ignoring option --with-pic-libpoly-include-dir since MCSAT support is disabled])
+ else
+- if test "x$withval" == x; then
++ if test "x$withval" = x; then
+ AC_MSG_WARN([--with-pic-libpoly-include-dir was used but no directory was given. Using defaults])
+ else
+ pic_includelpoly=$withval
+@@ -811,7 +811,7 @@ if test ! -d configs ; then
+ AS_MKDIR_P([configs])
+ fi
+
+-if test "x$host" == x ; then
++if test "x$host" = x ; then
+ AC_MSG_NOTICE([Moving make.include to configs/make.include.$build])
+ mv make.include "configs/make.include.$build"
+ else
diff -r 5d4d248dc87d -r eb174c755593 math/yices2/patches/patch-src_Makefile
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/math/yices2/patches/patch-src_Makefile Sat Aug 24 22:09:16 2019 +0000
@@ -0,0 +1,42 @@
+$NetBSD: patch-src_Makefile,v 1.1.1.1 2019/08/24 22:09:16 alnsn Exp $
+
+Add NetBSD targets, do not invoke static_libyices_dynamic, pull request https://github.com/SRI-CSL/yices2/pull/134
+
+--- src/Makefile.orig 2018-10-26 21:33:09.000000000 +0000
++++ src/Makefile
+@@ -624,6 +624,18 @@ ifeq ($(POSIXOS),freebsd)
+ static_libyices_dynamic=$(static_libdir)/$(libyices_so)
+
+ else
++ifeq ($(POSIXOS),netbsd)
++ PIC=-fPIC
++ STATIC=-static
++ CPPFLAGS := $(CPPFLAGS) -DNETBSD
++ CFLAGS += -fvisibility=hidden
++ BIN_LDFLAGS=
++ libyices_dynamic=$(libdir)/$(libyices_so)
++ # Dynamic library can't be built from .a files because
++ # they aren't normally built with -fPIC.
++ static_libyices_dynamic=
++
++else
+ ifeq ($(POSIXOS),unix)
+ PIC=-fPIC
+ STATIC=-static
+@@ -641,6 +653,7 @@ endif
+ endif
Home |
Main Index |
Thread Index |
Old Index