From owner-svn-ports-all@freebsd.org Sat Jul 21 08:11:48 2018 Return-Path: Delivered-To: svn-ports-all@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id B836A10408F8; Sat, 21 Jul 2018 08:11:48 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mxrelay.nyi.freebsd.org", Issuer "Let's Encrypt Authority X3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 6D07A813F6; Sat, 21 Jul 2018 08:11:48 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org (repo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4F6491C725; Sat, 21 Jul 2018 08:11:48 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org ([127.0.1.37]) by repo.freebsd.org (8.15.2/8.15.2) with ESMTP id w6L8BmRW049018; Sat, 21 Jul 2018 08:11:48 GMT (envelope-from yuri@FreeBSD.org) Received: (from yuri@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id w6L8Bleh049013; Sat, 21 Jul 2018 08:11:47 GMT (envelope-from yuri@FreeBSD.org) Message-Id: <201807210811.w6L8Bleh049013@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: yuri set sender to yuri@FreeBSD.org using -f From: Yuri Victorovich Date: Sat, 21 Jul 2018 08:11:47 +0000 (UTC) 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 X-SVN-Group: ports-head X-SVN-Commit-Author: yuri X-SVN-Commit-Paths: in head/math: . yices yices/files X-SVN-Commit-Revision: 475051 X-SVN-Commit-Repository: ports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-all@freebsd.org X-Mailman-Version: 2.1.27 Precedence: list List-Id: SVN commit messages for the ports tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 21 Jul 2018 08:11:49 -0000 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 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