From owner-svn-ports-head@freebsd.org Sun Nov 19 21:59:34 2017 Return-Path: Delivered-To: svn-ports-head@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 9AC37DBF7A4; Sun, 19 Nov 2017 21:59:34 +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 mx1.freebsd.org (Postfix) with ESMTPS id 5A46B656AE; Sun, 19 Nov 2017 21:59:34 +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 vAJLxXcV080401; Sun, 19 Nov 2017 21:59:33 GMT (envelope-from yuri@FreeBSD.org) Received: (from yuri@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id vAJLxWrC080394; Sun, 19 Nov 2017 21:59:32 GMT (envelope-from yuri@FreeBSD.org) Message-Id: <201711192159.vAJLxWrC080394@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: yuri set sender to yuri@FreeBSD.org using -f From: Yuri Victorovich Date: Sun, 19 Nov 2017 21:59:32 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r454506 - in head/math: . eprover eprover/files X-SVN-Group: ports-head X-SVN-Commit-Author: yuri X-SVN-Commit-Paths: in head/math: . eprover eprover/files X-SVN-Commit-Revision: 454506 X-SVN-Commit-Repository: ports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-head@freebsd.org X-Mailman-Version: 2.1.25 Precedence: list List-Id: SVN commit messages for the ports tree for head List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 19 Nov 2017 21:59:34 -0000 Author: yuri Date: Sun Nov 19 21:59:32 2017 New Revision: 454506 URL: https://svnweb.freebsd.org/changeset/ports/454506 Log: New port: math/eprover : Theorem prover for full first-order logic with equality PR: 211903 Submitted by: Greg V Approved by: tcberner (mentor) Differential Revision: https://reviews.freebsd.org/D13150 Added: head/math/eprover/ head/math/eprover/Makefile (contents, props changed) head/math/eprover/distinfo (contents, props changed) head/math/eprover/files/ head/math/eprover/files/patch-Makefile (contents, props changed) head/math/eprover/files/patch-Makefile.vars (contents, props changed) head/math/eprover/pkg-descr (contents, props changed) head/math/eprover/pkg-plist (contents, props changed) Modified: head/math/Makefile Modified: head/math/Makefile ============================================================================== --- head/math/Makefile Sun Nov 19 21:55:20 2017 (r454505) +++ head/math/Makefile Sun Nov 19 21:59:32 2017 (r454506) @@ -166,6 +166,7 @@ SUBDIR += emc2 SUBDIR += ent SUBDIR += entropy + SUBDIR += eprover SUBDIR += ess SUBDIR += eukleides SUBDIR += eval Added: head/math/eprover/Makefile ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/Makefile Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,48 @@ +# $FreeBSD$ + +PORTNAME= eprover +DISTVERSIONPREFIX= E- +DISTVERSION= 2.0 +CATEGORIES= math + +MAINTAINER= greg@unrelenting.technology +COMMENT= Theorem prover for full first-order logic with equality + +LICENSE= LGPL20+ GPLv2+ +LICENSE_COMB= dual +LICENSE_FILE= ${WRKSRC}/COPYING + +BUILD_DEPENDS= bash:shells/bash \ + help2man:misc/help2man +RUN_DEPENDS= bash:shells/bash + +USES= shebangfix +USE_GITHUB= yes + +HAS_CONFIGURE= yes +CONFIGURE_ARGS= --bindir=${STAGEDIR}${PREFIX}/bin/ \ + --man-prefix=${STAGEDIR}${PREFIX}/man/man1/ +SHEBANG_FILES= PROVER/eproof PROVER/eproof_ram + +post-build: + @cd ${WRKSRC} && ${MAKE} man + @${REINPLACE_CMD} -e 's|EXECPATH=.|EXECPATH=${PREFIX}/bin|' \ + ${WRKSRC}/PROVER/eproof ${WRKSRC}/PROVER/eproof_ram + +post-install: +.for f in checkproof e_axfilter e_deduction_server e_ltb_runner eground \ + ekb_create ekb_delete ekb_ginsert ekb_insert epclextract eprover + @${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/${f} +.endfor + +.include + +.if ${OPSYS} == FreeBSD && ${OSVERSION} < 1100000 +# the default compiler hangs on 10 +BUILD_DEPENDS+= clang40:devel/llvm40 +RUN_DEPENDS+= clang40:devel/llvm40 +CC= clang40 +CXX= clang++40 +.endif + +.include Added: head/math/eprover/distinfo ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/distinfo Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,3 @@ +TIMESTAMP = 1508690062 +SHA256 (eprover-eprover-E-2.0_GH0.tar.gz) = 63986bcfa139381831c14af5ef83e350f8efb169b1d22d15cb92026259ea14d2 +SIZE (eprover-eprover-E-2.0_GH0.tar.gz) = 1315451 Added: head/math/eprover/files/patch-Makefile ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/files/patch-Makefile Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,10 @@ +--- Makefile.orig 2017-11-18 22:48:40 UTC ++++ Makefile +@@ -175,6 +175,7 @@ documentation: + + man: E + mkdir -p DOC/man ++ help2man -N -i DOC/bug_reporting PROVER/e_deduction_server > DOC/man/e_deduction_server.1 + help2man -N -i DOC/bug_reporting PROVER/eproof > DOC/man/eproof.1 + help2man -N -i DOC/bug_reporting PROVER/eproof_ram > DOC/man/eproof_ram.1 + help2man -N -i DOC/bug_reporting PROVER/eprover > DOC/man/eprover.1 Added: head/math/eprover/files/patch-Makefile.vars ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/files/patch-Makefile.vars Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,24 @@ +--- Makefile.vars.orig 2017-07-07 12:35:57 UTC ++++ Makefile.vars +@@ -134,17 +134,17 @@ PROFFLAGS = # -pg + DEBUGGER = # -g -ggdb + LTOFLAGS = # -flto + WFLAGS = -Wall +-OPTFLAGS = -O3 -fomit-frame-pointer -fno-common ++OPTFLAGS = + + + DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG) +-CFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include +-LDFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER) ++CFLAGS += $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include ++LDFLAGS += $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER) + LD = $(CC) $(LDFLAGS) + + # Generic + AR = ar rcs +- CC = gcc ++ CC ?= gcc + + # Builds with link time optimization + # Added: head/math/eprover/pkg-descr ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/pkg-descr Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,7 @@ +A saturating theorem prover for full first-order logic with equality. It accepts +a problem specification, typically consisting of a number of first-order clauses +or formulas, and a conjecture, again either in clausal or full first-order +form. The system will then try to find a formal proof for the conjecture, +assuming the axioms. + +WWW: http://www.eprover.org Added: head/math/eprover/pkg-plist ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/eprover/pkg-plist Sun Nov 19 21:59:32 2017 (r454506) @@ -0,0 +1,26 @@ +bin/checkproof +bin/e_axfilter +bin/e_deduction_server +bin/e_ltb_runner +bin/eground +bin/ekb_create +bin/ekb_delete +bin/ekb_ginsert +bin/ekb_insert +bin/epclextract +bin/eproof +bin/eproof_ram +bin/eprover +man/man1/checkproof.1.gz +man/man1/e_axfilter.1.gz +man/man1/e_deduction_server.1.gz +man/man1/e_ltb_runner.1.gz +man/man1/eground.1.gz +man/man1/ekb_create.1.gz +man/man1/ekb_delete.1.gz +man/man1/ekb_ginsert.1.gz +man/man1/ekb_insert.1.gz +man/man1/epclextract.1.gz +man/man1/eproof.1.gz +man/man1/eproof_ram.1.gz +man/man1/eprover.1.gz