svn commit: r510141 - in head/math/vampire: . files
Yuri Victorovich
yuri at FreeBSD.org
Thu Aug 29 05:30:58 UTC 2019
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 at 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/
More information about the svn-ports-all
mailing list