Attachment 188102 Details for Bug 211903 – Modified Greg's eprover.patch

[patch] Modified Greg's eprover.patch

eprover.patch (text/plain), 5.47 KB, created by Yuri Victorovich on 2017-11-18 21:25:10 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Yuri Victorovich

Created: 2017-11-18 21:25:10 UTC

Size: 5.47 KB

patch

obsolete

>Index: math/eprover/Makefile
>===================================================================
>--- math/eprover/Makefile	(nonexistent)
>+++ math/eprover/Makefile	(working copy)
>@@ -0,0 +1,36 @@
>+# $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=	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 eprover epclextract e_deduction_server ekb_delete e_axfilter ekb_create e_ltb_runner eground ekb_ginsert checkproof ekb_insert
>+	@${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/${f}
>+.endfor
>+
>+.include <bsd.port.mk>
>
>Property changes on: math/eprover/Makefile
>___________________________________________________________________
>Added: svn:eol-style
>## -0,0 +1 ##
>+native
>\ No newline at end of property
>Added: svn:keywords
>## -0,0 +1 ##
>+FreeBSD=%H
>\ No newline at end of property
>Added: svn:mime-type
>## -0,0 +1 ##
>+text/plain
>\ No newline at end of property
>Index: math/eprover/distinfo
>===================================================================
>--- math/eprover/distinfo	(nonexistent)
>+++ math/eprover/distinfo	(working copy)
>@@ -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
>
>Property changes on: math/eprover/distinfo
>___________________________________________________________________
>Added: fbsd:nokeywords
>## -0,0 +1 ##
>+yes
>\ No newline at end of property
>Added: svn:eol-style
>## -0,0 +1 ##
>+native
>\ No newline at end of property
>Added: svn:mime-type
>## -0,0 +1 ##
>+text/plain
>\ No newline at end of property
>Index: math/eprover/files/patch-Makefile.vars
>===================================================================
>--- math/eprover/files/patch-Makefile.vars	(nonexistent)
>+++ math/eprover/files/patch-Makefile.vars	(working copy)
>@@ -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
>+ #
>
>Property changes on: math/eprover/files/patch-Makefile.vars
>___________________________________________________________________
>Added: fbsd:nokeywords
>## -0,0 +1 ##
>+yes
>\ No newline at end of property
>Added: svn:eol-style
>## -0,0 +1 ##
>+native
>\ No newline at end of property
>Added: svn:mime-type
>## -0,0 +1 ##
>+text/plain
>\ No newline at end of property
>Index: math/eprover/pkg-descr
>===================================================================
>--- math/eprover/pkg-descr	(nonexistent)
>+++ math/eprover/pkg-descr	(working copy)
>@@ -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
>
>Property changes on: math/eprover/pkg-descr
>___________________________________________________________________
>Added: fbsd:nokeywords
>## -0,0 +1 ##
>+yes
>\ No newline at end of property
>Added: svn:eol-style
>## -0,0 +1 ##
>+native
>\ No newline at end of property
>Added: svn:mime-type
>## -0,0 +1 ##
>+text/plain
>\ No newline at end of property
>Index: math/eprover/pkg-plist
>===================================================================
>--- math/eprover/pkg-plist	(nonexistent)
>+++ math/eprover/pkg-plist	(working copy)
>@@ -0,0 +1,25 @@
>+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_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
>
>Property changes on: math/eprover/pkg-plist
>___________________________________________________________________
>Added: fbsd:nokeywords
>## -0,0 +1 ##
>+yes
>\ No newline at end of property
>Added: svn:eol-style
>## -0,0 +1 ##
>+native
>\ No newline at end of property
>Added: svn:mime-type
>## -0,0 +1 ##
>+text/plain
>\ No newline at end of property

Actions: View | Diff

Attachments on bug 211903: 173738 | 174011 | 187373 | 188101 | 188102