Skip site navigation (1)Skip section navigation (2)
Date:      Sat, 21 Jul 2018 08:11:47 +0000 (UTC)
From:      Yuri Victorovich <yuri@FreeBSD.org>
To:        ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org
Subject:   svn commit: r475051 - in head/math: . yices yices/files
Message-ID:  <201807210811.w6L8Bleh049013@repo.freebsd.org>

next in thread | raw e-mail | index | archive | help
Author: yuri
Date: Sat Jul 21 08:11:46 2018
New Revision: 475051
URL: https://svnweb.freebsd.org/changeset/ports/475051

Log:
  New port: math/yices: SMT solver

Added:
  head/math/yices/
  head/math/yices/Makefile   (contents, props changed)
  head/math/yices/distinfo   (contents, props changed)
  head/math/yices/files/
  head/math/yices/files/patch-Makefile.build   (contents, props changed)
  head/math/yices/pkg-descr   (contents, props changed)
  head/math/yices/pkg-plist   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Sat Jul 21 06:58:42 2018	(r475050)
+++ head/math/Makefile	Sat Jul 21 08:11:46 2018	(r475051)
@@ -836,6 +836,7 @@
     SUBDIR += xspread
     SUBDIR += xtensor
     SUBDIR += yacas
+    SUBDIR += yices
     SUBDIR += z3
     SUBDIR += zimpl
 

Added: head/math/yices/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/yices/Makefile	Sat Jul 21 08:11:46 2018	(r475051)
@@ -0,0 +1,32 @@
+# $FreeBSD$
+
+PORTNAME=	yices
+DISTVERSION=	2.6.0
+CATEGORIES=	math
+MASTER_SITES=	http://yices.csl.sri.com/releases/${DISTVERSION}/
+DISTNAME=	${PORTNAME}-${DISTVERSION}-src
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	SMT solver
+
+LICENSE=	GPLv3
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+BUILD_DEPENDS=	gperf:devel/gperf
+LIB_DEPENDS=	libgmp.so:math/gmp
+
+USES=		gmake localbase
+GNU_CONFIGURE=	yes
+CONFIGURE_ARGS=	--with-pic-gmp=${LOCALBASE}/lib/libgmp.so
+USE_LDCONFIG=	yes
+
+MAKE_ARGS=	YICES_MAKE_INCLUDE=configs/make.include.${CONFIGURE_TARGET}
+CFLAGS+=	-fPIC
+
+WRKSRC=		${WRKDIR}/${PORTNAME}-${DISTVERSION}
+
+post-install:
+	@${RM} ${STAGEDIR}${PREFIX}/lib/*.a
+	@cd ${STAGEDIR}${PREFIX}/lib && ${LN} -s libyices.so.2.6 libyices.so && ${LN} -s libyices.so.2.6 libyices.so.2
+
+.include <bsd.port.mk>

Added: head/math/yices/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/yices/distinfo	Sat Jul 21 08:11:46 2018	(r475051)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1532156748
+SHA256 (yices-2.6.0-src.tar.gz) = 4712c5c4bd1d299418148c68851c023041dc16450907353bedd4c17c1e4713e4
+SIZE (yices-2.6.0-src.tar.gz) = 5539571

Added: head/math/yices/files/patch-Makefile.build
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/yices/files/patch-Makefile.build	Sat Jul 21 08:11:46 2018	(r475051)
@@ -0,0 +1,28 @@
+--- Makefile.build.orig	2018-06-29 04:11:11 UTC
++++ Makefile.build
+@@ -131,7 +131,7 @@ static_objsubdirs := $(srcsubdirs:%=$(st
+ # build_dir/dist: binaries + libraries with distribution not linked with GMP
+ # build_dir/static_dist: includes GMP (statically linked)
+ #
+-dist_dir = $(build_dir)/dist
++dist_dir = $(build_dir)
+ static_dist_dir = $(build_dir)/static_dist
+ 
+ 
+@@ -448,7 +448,7 @@ install-default:
+ 	$(MKDIR_P) $(DESTDIR)$(bindir)
+ 	$(MKDIR_P) $(DESTDIR)$(libdir)
+ 	$(MKDIR_P) $(DESTDIR)$(includedir)
+-	$(INSTALL) -m 664 $(dist_dir)/include/* $(DESTDIR)$(includedir)
++	$(INSTALL) -m 664 $(dist_dir)/../../src/include/* $(DESTDIR)$(includedir)
+ 	$(INSTALL) $(dist_dir)/bin/* $(DESTDIR)$(bindir)
+ 	$(INSTALL) $(dist_dir)/lib/* $(DESTDIR)$(libdir)
+ 
+@@ -467,7 +467,6 @@ install-linux install-unix: install-defa
+ # be added to the hints file.' In other words, ldconfig on FreeBSD doesn't create the symbolic link,
+ # as on Linux.
+ install-freebsd: install-default
+-	$(LDCONFIG) -m $(DESTDIR)$(libdir) && (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(MAJOR).$(MINOR) libyices.so)
+ 
+ #
+ # cygwin and mingw install: copy the DLLs in $(bindir)

Added: head/math/yices/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/yices/pkg-descr	Sat Jul 21 08:11:46 2018	(r475051)
@@ -0,0 +1,11 @@
+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.
+
+WWW: http://yices.csl.sri.com/

Added: head/math/yices/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/yices/pkg-plist	Sat Jul 21 08:11:46 2018	(r475051)
@@ -0,0 +1,13 @@
+bin/yices_main
+bin/yices_sat
+bin/yices_sat_new
+bin/yices_smt
+bin/yices_smt2
+bin/yices_smtcomp
+include/yices.h
+include/yices_exit_codes.h
+include/yices_limits.h
+include/yices_types.h
+lib/libyices.so
+lib/libyices.so.2
+lib/libyices.so.2.6



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201807210811.w6L8Bleh049013>