Attachment #188101 for bug #211903

Lines 293-298 Link Here

(-)math/Makefile (+1 lines)
293	SUBDIR += lybniz	293	SUBDIR += lybniz
294	SUBDIR += mate-calc	294	SUBDIR += mate-calc
295	SUBDIR += math77	295	SUBDIR += math77
		296	SUBDIR += mathgl
296	SUBDIR += mathmod	297	SUBDIR += mathmod
297	SUBDIR += mathomatic	298	SUBDIR += mathomatic
298	SUBDIR += matio	299	SUBDIR += matio




# $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>

Line 0 Link Here

(-)math/eprover/distinfo (+3 lines)
	1	TIMESTAMP = 1508690062
	2	SHA256 (eprover-eprover-E-2.0_GH0.tar.gz) = 63986bcfa139381831c14af5ef83e350f8efb169b1d22d15cb92026259ea14d2
	3	SIZE (eprover-eprover-E-2.0_GH0.tar.gz) = 1315451




--- 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
 #

Line 0 Link Here

(-)math/eprover/pkg-descr (+7 lines)
	1	A saturating theorem prover for full first-order logic with equality. It accepts
	2	a problem specification, typically consisting of a number of first-order clauses
	3	or formulas, and a conjecture, again either in clausal or full first-order
	4	form. The system will then try to find a formal proof for the conjecture,
	5	assuming the axioms.
	6
	7	WWW: http://www.eprover.org




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

Return to bug 211903

Line 0 Link Here

(-)math/eprover/Makefile (+36 lines)
	1	# $FreeBSD$
	2
	3	PORTNAME= eprover
	4	DISTVERSIONPREFIX= E-
	5	DISTVERSION= 2.0
	6	CATEGORIES= math
	7
	8	MAINTAINER= greg@unrelenting.technology
	9	COMMENT= Theorem prover for full first-order logic with equality
	10
	11	LICENSE= LGPL20+ GPLv2+
	12	LICENSE_COMB= dual
	13	LICENSE_FILE= ${WRKSRC}/COPYING
	14
	15	BUILD_DEPENDS= help2man:misc/help2man
	16	RUN_DEPENDS= bash:shells/bash
	17
	18	USES= shebangfix
	19	USE_GITHUB= yes
	20
	21	HAS_CONFIGURE= yes
	22	CONFIGURE_ARGS= --bindir=${STAGEDIR}${PREFIX}/bin/ \
	23	--man-prefix=${STAGEDIR}${PREFIX}/man/man1/
	24	SHEBANG_FILES= PROVER/eproof PROVER/eproof_ram
	25
	26	post-build:
	27	@cd ${WRKSRC} && ${MAKE} man
	28	@${REINPLACE_CMD} -e 's\|EXECPATH=.\|EXECPATH=${PREFIX}/bin\|' \
	29	${WRKSRC}/PROVER/eproof ${WRKSRC}/PROVER/eproof_ram
	30
	31	post-install:
	32	.for f in eprover epclextract e_deduction_server ekb_delete e_axfilter ekb_create e_ltb_runner eground ekb_ginsert checkproof ekb_insert
	33	@${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/${f}
	34	.endfor
	35
	36	.include <bsd.port.mk>

Line 0 Link Here

(-)math/eprover/files/patch-Makefile.vars (+24 lines)
	1	--- Makefile.vars.orig 2017-07-07 12:35:57 UTC
	2	+++ Makefile.vars
	3	@@ -134,17 +134,17 @@ PROFFLAGS = # -pg
	4	DEBUGGER = # -g -ggdb
	5	LTOFLAGS = # -flto
	6	WFLAGS = -Wall
	7	-OPTFLAGS = -O3 -fomit-frame-pointer -fno-common
	8	+OPTFLAGS =
	9
	10
	11	DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG)
	12	-CFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include
	13	-LDFLAGS = $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER)
	14	+CFLAGS += $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include
	15	+LDFLAGS += $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER)
	16	LD = $(CC) $(LDFLAGS)
	17
	18	# Generic
	19	AR = ar rcs
	20	- CC = gcc
	21	+ CC ?= gcc
	22
	23	# Builds with link time optimization
	24	#

Line 0 Link Here

(-)math/eprover/pkg-plist (+25 lines)
	1	bin/checkproof
	2	bin/e_axfilter
	3	bin/e_deduction_server
	4	bin/e_ltb_runner
	5	bin/eground
	6	bin/ekb_create
	7	bin/ekb_delete
	8	bin/ekb_ginsert
	9	bin/ekb_insert
	10	bin/epclextract
	11	bin/eproof
	12	bin/eproof_ram
	13	bin/eprover
	14	man/man1/checkproof.1.gz
	15	man/man1/e_axfilter.1.gz
	16	man/man1/e_ltb_runner.1.gz
	17	man/man1/eground.1.gz
	18	man/man1/ekb_create.1.gz
	19	man/man1/ekb_delete.1.gz
	20	man/man1/ekb_ginsert.1.gz
	21	man/man1/ekb_insert.1.gz
	22	man/man1/epclextract.1.gz
	23	man/man1/eproof.1.gz
	24	man/man1/eproof_ram.1.gz
	25	man/man1/eprover.1.gz