Date: Sun, 19 Nov 2017 21:59:32 +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: r454506 - in head/math: . eprover eprover/files Message-ID: <201711192159.vAJLxWrC080394@repo.freebsd.org>
next in thread | raw e-mail | index | archive | help
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 <greg@unrelenting.technology> 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 <bsd.port.pre.mk> + +.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 <bsd.port.post.mk> 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201711192159.vAJLxWrC080394>