math/vampire: Hook to the build
This commit is contained in:
Yuri Victorovich
parent
5ebdb5f462
commit
8cd1b55f0a
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=510760
7 changed files with 113 additions and 0 deletions
|
|
@ -876,6 +876,7 @@
|
|||
SUBDIR += ump
|
||||
SUBDIR += units
|
||||
SUBDIR += unuran
|
||||
SUBDIR += vampire
|
||||
SUBDIR += viennacl
|
||||
SUBDIR += visualpolylib
|
||||
SUBDIR += vowpal_wabbit
|
||||
|
|
|
|||
31
math/vampire/Makefile
Normal file
31
math/vampire/Makefile
Normal file
|
|
@ -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= compiler:c++11-lang 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>
|
||||
3
math/vampire/distinfo
Normal file
3
math/vampire/distinfo
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
TIMESTAMP = 1567051355
|
||||
SHA256 (vprover-vampire-4.4_GH0.tar.gz) = 43f09743a3a505ec8d8ac6fb60420915d56c4164be3caab728d7856a4f2ace8d
|
||||
SIZE (vprover-vampire-4.4_GH0.tar.gz) = 1748193
|
||||
16
math/vampire/files/patch-Lib_Portability.hpp
Normal file
16
math/vampire/files/patch-Lib_Portability.hpp
Normal file
|
|
@ -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
|
||||
|
||||
//////////////////////////////////////////////////////
|
||||
26
math/vampire/files/patch-Lib_System.cpp
Normal file
26
math/vampire/files/patch-Lib_System.cpp
Normal file
|
|
@ -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
|
||||
27
math/vampire/files/patch-Makefile
Normal file
27
math/vampire/files/patch-Makefile
Normal file
|
|
@ -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:
|
||||
9
math/vampire/pkg-descr
Normal file
9
math/vampire/pkg-descr
Normal file
|
|
@ -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/
|
||||
Loading…
Reference in a new issue