svn commit: r454506 - in head/math: . eprover eprover/files

Yuri Victorovich yuri at FreeBSD.org
Sun Nov 19 21:59:34 UTC 2017 

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

More information about the svn-ports-head mailing list