Skip site navigation (1)Skip section navigation (2)
Date:      Thu, 29 Aug 2019 05:30:57 +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: r510141 - in head/math/vampire: . files
Message-ID:  <201908290530.x7T5Uvtq092397@repo.freebsd.org>

next in thread | raw e-mail | index | archive | help
Author: yuri
Date: Thu Aug 29 05:30:57 2019
New Revision: 510141
URL: https://svnweb.freebsd.org/changeset/ports/510141

Log:
  New port: math/vampire: Automatic theorem prover

Added:
  head/math/vampire/
  head/math/vampire/Makefile   (contents, props changed)
  head/math/vampire/distinfo   (contents, props changed)
  head/math/vampire/files/
  head/math/vampire/files/patch-Lib_Portability.hpp   (contents, props changed)
  head/math/vampire/files/patch-Lib_System.cpp   (contents, props changed)
  head/math/vampire/files/patch-Makefile   (contents, props changed)
  head/math/vampire/pkg-descr   (contents, props changed)

Added: head/math/vampire/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/Makefile	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,31 @@
+# $FreeBSD$
+
+PORTNAME=	vampire
+DISTVERSION=	4.4
+CATEGORIES=	math
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Automatic theorem prover
+
+LICENSE=	BSD2CLAUSE
+xLICENSE_FILE=	${WRKSRC}/LICENSE
+
+USES=		gmake
+USE_GITHUB=	yes
+GH_ACCOUNT=	vprover
+
+ALL_TARGET=	vampire_rel # do we also need the z3 target?
+
+BINARY_ALIAS=	g++=${CXX}
+
+CXXFLAGS+=	-DCHECK_LEAKS=0
+MAKE_ARGS=	FREEBSD_VERSION_NUMBER="${PORTVERSION}"
+
+#MAKE_ARGS=	GNUMPF=1 # This causes compillation failure, additionally GitHub failed to create the issue for this project.
+
+PLIST_FILES=	bin/${PORTNAME}
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/${ALL_TARGET}* ${STAGEDIR}${PREFIX}/bin/${PORTNAME}
+
+.include <bsd.port.mk>

Added: head/math/vampire/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/distinfo	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1567051355
+SHA256 (vprover-vampire-4.4_GH0.tar.gz) = 43f09743a3a505ec8d8ac6fb60420915d56c4164be3caab728d7856a4f2ace8d
+SIZE (vprover-vampire-4.4_GH0.tar.gz) = 1748193

Added: head/math/vampire/files/patch-Lib_Portability.hpp
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/files/patch-Lib_Portability.hpp	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,16 @@
+--- Lib/Portability.hpp.orig	2018-12-01 20:14:14 UTC
++++ Lib/Portability.hpp
+@@ -25,11 +25,11 @@
+ // Detect compiler
+ 
+ #ifndef __APPLE__
+-# define __APPLE__ 0
++//# define __APPLE__ 0
+ #endif
+ 
+ #ifndef __CYGWIN__
+-# define __CYGWIN__ 0
++//# define __CYGWIN__ 0
+ #endif
+ 
+ //////////////////////////////////////////////////////

Added: head/math/vampire/files/patch-Lib_System.cpp
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/files/patch-Lib_System.cpp	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,26 @@
+--- Lib/System.cpp.orig	2018-12-01 20:15:38 UTC
++++ Lib/System.cpp
+@@ -27,9 +27,13 @@
+ #include <stdlib.h>
+ #  include <unistd.h>
+ #  if !__APPLE__ && !__CYGWIN__
+-#    include <sys/prctl.h>
++//#    include <sys/prctl.h>
+ #  endif
+ 
++#if defined (__FreeBSD__)
++#include <sys/wait.h>
++#endif
++
+ #include <dirent.h>
+ 
+ #include <cerrno>
+@@ -360,7 +364,7 @@ void System::terminateImmediately(int re
+  */
+ void System::registerForSIGHUPOnParentDeath()
+ {
+-#if __APPLE__ || __CYGWIN__
++#if __APPLE__ || __CYGWIN__ || __FreeBSD__
+   // cerr<<"Death of parent process not being handled on Mac and Windows"<<endl;
+   // NOT_IMPLEMENTED;
+ #else

Added: head/math/vampire/files/patch-Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/files/patch-Makefile	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,27 @@
+--- Makefile.orig	2019-08-23 07:50:16 UTC
++++ Makefile
+@@ -557,20 +557,17 @@ VERSION_NUMBER = 4.4.0
+ # The dependency on .git/HEAD tracks switching between branches,
+ # the dependency on .git/index tracks new commits.
+ 
+-.git/HEAD:
+-.git/index:
+-
+-version.cpp: .git/HEAD .git/index Makefile
++version.cpp: Makefile
+ 	@echo "//Automatically generated file, see Makefile for details" > $@
+-	@echo "const char* VERSION_STRING = \"Vampire $(VERSION_NUMBER) (commit $(shell git log -1 --format=%h\ on\ %ci || echo unknown))\";" >> $@
++	@echo "const char* VERSION_STRING = \"Vampire $(FREEBSD_VERSION_NUMBER)\";" >> $@
+ 
+ ################################################################
+ # separate directory for object files implementation
+ 
+ # different directory for each configuration, so there is no need for "make clean"
+ SED_CMD='s/^[(]HEAD$$/detached/'      #
+-BRANCH=$(shell git branch | grep "\*" | cut -d ' ' -f 2 | sed -e $(SED_CMD)  )
+-COM_CNT=$(shell git rev-list HEAD --count)
++BRANCH="master"
++COM_CNT="0"
+ CONF_ID := obj/$(shell echo -n "$(BRANCH) $(XFLAGS)"|sum|cut -d ' ' -f1)X
+ 
+ obj:

Added: head/math/vampire/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/vampire/pkg-descr	Thu Aug 29 05:30:57 2019	(r510141)
@@ -0,0 +1,9 @@
+Automatic theorem proving has a number of important applications, such as
+software verification, hardware verification, hardware design, knowledge
+representation and reasoning, the Semantic Web, algebra, and proving theorems
+in mathematics. Over 50 years of research in theorem proving have resulted in
+one of the most advanced and elegant theories in computer science. This area is
+an ideal target for scientific engineering: implementation techniques have to be
+developed to realise an advanced theory in practically valuable tools.
+
+WWW: https://vprover.github.io/



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201908290530.x7T5Uvtq092397>