diff options
author | Yuri Victorovich <yuri@FreeBSD.org> | 2019-08-29 05:30:57 +0000 |
---|---|---|
committer | Yuri Victorovich <yuri@FreeBSD.org> | 2019-08-29 05:30:57 +0000 |
commit | 37a666afb9de63fe7f95e2afc74624e47e42a87f (patch) | |
tree | 494a5b1174d6091d32d321f844819a0e384d6841 /math/vampire | |
parent | c37af9770f485c1ae1bda503052910ea42e3cf38 (diff) | |
download | ports-37a666afb9de63fe7f95e2afc74624e47e42a87f.tar.gz ports-37a666afb9de63fe7f95e2afc74624e47e42a87f.zip |
New port: math/vampire: Automatic theorem prover
Notes
Notes:
svn path=/head/; revision=510141
Diffstat (limited to 'math/vampire')
-rw-r--r-- | math/vampire/Makefile | 31 | ||||
-rw-r--r-- | math/vampire/distinfo | 3 | ||||
-rw-r--r-- | math/vampire/files/patch-Lib_Portability.hpp | 16 | ||||
-rw-r--r-- | math/vampire/files/patch-Lib_System.cpp | 26 | ||||
-rw-r--r-- | math/vampire/files/patch-Makefile | 27 | ||||
-rw-r--r-- | math/vampire/pkg-descr | 9 |
6 files changed, 112 insertions, 0 deletions
diff --git a/math/vampire/Makefile b/math/vampire/Makefile new file mode 100644 index 000000000000..9cb3a994b954 --- /dev/null +++ b/math/vampire/Makefile @@ -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> diff --git a/math/vampire/distinfo b/math/vampire/distinfo new file mode 100644 index 000000000000..5debd66afb3d --- /dev/null +++ b/math/vampire/distinfo @@ -0,0 +1,3 @@ +TIMESTAMP = 1567051355 +SHA256 (vprover-vampire-4.4_GH0.tar.gz) = 43f09743a3a505ec8d8ac6fb60420915d56c4164be3caab728d7856a4f2ace8d +SIZE (vprover-vampire-4.4_GH0.tar.gz) = 1748193 diff --git a/math/vampire/files/patch-Lib_Portability.hpp b/math/vampire/files/patch-Lib_Portability.hpp new file mode 100644 index 000000000000..e82b0a05f6c8 --- /dev/null +++ b/math/vampire/files/patch-Lib_Portability.hpp @@ -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 + + ////////////////////////////////////////////////////// diff --git a/math/vampire/files/patch-Lib_System.cpp b/math/vampire/files/patch-Lib_System.cpp new file mode 100644 index 000000000000..1d054dcf2b31 --- /dev/null +++ b/math/vampire/files/patch-Lib_System.cpp @@ -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 diff --git a/math/vampire/files/patch-Makefile b/math/vampire/files/patch-Makefile new file mode 100644 index 000000000000..e4525c0022b1 --- /dev/null +++ b/math/vampire/files/patch-Makefile @@ -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: diff --git a/math/vampire/pkg-descr b/math/vampire/pkg-descr new file mode 100644 index 000000000000..90442288a95d --- /dev/null +++ b/math/vampire/pkg-descr @@ -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/ |