Page MenuHomeFreeBSD
Files F147992923

D13150.diff
No OneTemporary
Actions

D13150.diff
View Options

Index: head/math/Makefile
===================================================================
--- head/math/Makefile
+++ head/math/Makefile
@@ -166,6 +166,7 @@
SUBDIR += emc2
SUBDIR += ent
SUBDIR += entropy
+ SUBDIR += eprover
SUBDIR += ess
SUBDIR += eukleides
SUBDIR += eval
Index: head/math/eprover/Makefile
===================================================================
--- head/math/eprover/Makefile
+++ head/math/eprover/Makefile
@@ -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>
Index: head/math/eprover/distinfo
===================================================================
--- head/math/eprover/distinfo
+++ head/math/eprover/distinfo
@@ -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
Index: head/math/eprover/files/patch-Makefile
===================================================================
--- head/math/eprover/files/patch-Makefile
+++ head/math/eprover/files/patch-Makefile
@@ -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
Index: head/math/eprover/files/patch-Makefile.vars
===================================================================
--- head/math/eprover/files/patch-Makefile.vars
+++ head/math/eprover/files/patch-Makefile.vars
@@ -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
+ #
Index: head/math/eprover/pkg-descr
===================================================================
--- head/math/eprover/pkg-descr
+++ head/math/eprover/pkg-descr
@@ -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
Index: head/math/eprover/pkg-plist
===================================================================
--- head/math/eprover/pkg-plist
+++ head/math/eprover/pkg-plist
@@ -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

File Metadata

Mime Type
text/plain
Expires
Mon, Mar 16, 2:10 AM (7 h, 53 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
29747886
Default Alt Text
D13150.diff (4 KB)

Event Timeline