summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNick Smallbone <nick@smallbone.se>2020-09-04 03:58:10 +0100
committerWilly Sudiarto Raharjo <willysr@slackbuilds.org>2020-09-05 08:26:44 +0700
commit3d9cd787ede47bea334c6133d786e7245f0086af (patch)
treeb533b4b388ae14092ea897665ca1ee0315d08842
parentfed4d5c0254a4c51051696a840893cdb1df7f552 (diff)
downloadslackbuilds-3d9cd787ede47bea334c6133d786e7245f0086af.tar.gz
academic/cvc4: Updated for version 1.8.
Signed-off-by: Dave Woodfall <dave@slackbuilds.org> Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
-rw-r--r--academic/cvc4/README6
-rw-r--r--academic/cvc4/cvc4.SlackBuild27
-rw-r--r--academic/cvc4/cvc4.info8
3 files changed, 28 insertions, 13 deletions
diff --git a/academic/cvc4/README b/academic/cvc4/README
index 830c7394fb..ed00fa62b8 100644
--- a/academic/cvc4/README
+++ b/academic/cvc4/README
@@ -4,4 +4,8 @@ either prove the formula or find a counterexample. CVC4 supports
arithmetic, reasoning about arrays, and several other built-in
theories. Input problems are written in SMT-LIB format.
-This package includes the cvc4 program as well as libraries.
+This package includes the cvc4 program, libraries, and Python 2
+bindings.
+
+Note that this SlackBuild builds CVC4 with readline support, which means
+the resulting executable is licensed under the GPLv3.
diff --git a/academic/cvc4/cvc4.SlackBuild b/academic/cvc4/cvc4.SlackBuild
index ce4b43bebf..d3a964cf03 100644
--- a/academic/cvc4/cvc4.SlackBuild
+++ b/academic/cvc4/cvc4.SlackBuild
@@ -2,7 +2,7 @@
# Slackware build script for cvc4
-# Copyright 2019 Nick Smallbone, Gothenburg, Sweden
+# Copyright 2019-2020 Nick Smallbone, Gothenburg, Sweden
# All rights reserved.
#
# Redistribution and use of this script, with or without modification, is
@@ -22,8 +22,12 @@
# OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
# ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+# TO DO:
+# Add new Python bindings (requires a newer version of Cython?)
+# Add Java bindings (requires a newer version of CMake?)
+
PRGNAM=cvc4
-VERSION=${VERSION:-1.7}
+VERSION=${VERSION:-1.8}
BUILD=${BUILD:-1}
TAG=${TAG:-_SBo}
SRCNAM=CVC4
@@ -70,22 +74,29 @@ find -L . \
\( -perm 666 -o -perm 664 -o -perm 640 -o -perm 600 -o -perm 444 \
-o -perm 440 -o -perm 400 \) -exec chmod 644 {} \;
-sed -i "s/DESTINATION lib/DESTINATION lib${LIBDIRSUFFIX}/" src/CMakeLists.txt src/parser/CMakeLists.txt
-chmod +x $CWD/run-antlr
+sed -i "s/LIBRARY_INSTALL_DIR lib/&${LIBDIRSUFFIX}/" CMakeLists.txt
+install -m 755 $CWD/run-antlr .
+cp $CWD/antlr-3.4-complete.jar .
cmake \
-DCMAKE_C_FLAGS:STRING="$SLKCFLAGS" \
-DCMAKE_CXX_FLAGS:STRING="$SLKCFLAGS" \
-DCMAKE_INSTALL_PREFIX=/usr \
-DCMAKE_BUILD_TYPE=Production \
- -DENABLE_OPTIMIZED=ON \
-DANTLR_INCLUDE_DIR=/usr/include/antlr3 \
- -DANTLR_BINARY="$CWD/run-antlr" \
+ -DANTLR_BINARY="$TMP/$SRCNAM-$VERSION/run-antlr" \
+ -DUSE_READLINE=OFF \
+ -DBUILD_BINDINGS_PYTHON=OFF \
+ -DBUILD_SWIG_BINDINGS_PYTHON=ON \
+ -DBUILD_SWIG_BINDINGS_JAVA=OFF \
.
make
-make doc
-make install/strip DESTDIR=$PKG
+make install DESTDIR=$PKG
+
+find $PKG -print0 | xargs -0 file | grep -e "executable" -e "shared object" | grep ELF \
+ | cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null || true
+
mv $PKG/usr/share/man $PKG/usr/man
find $PKG/usr/man -type f -exec gzip -9 {} \;
diff --git a/academic/cvc4/cvc4.info b/academic/cvc4/cvc4.info
index 9058f04efd..4fc4ede8c6 100644
--- a/academic/cvc4/cvc4.info
+++ b/academic/cvc4/cvc4.info
@@ -1,12 +1,12 @@
PRGNAM="cvc4"
-VERSION="1.7"
+VERSION="1.8"
HOMEPAGE="https://cvc4.cs.stanford.edu/"
-DOWNLOAD="https://github.com/CVC4/CVC4/archive/1.7/CVC4-1.7.tar.gz \
+DOWNLOAD="https://github.com/CVC4/CVC4/archive/1.8/CVC4-1.8.tar.gz \
https://www.antlr3.org/download/antlr-3.4-complete.jar"
-MD5SUM="eadb05f5092c4310f3bbe52745f9b7b9 \
+MD5SUM="9f7657e21fec3c4042225b0b8f513c34 \
1b91dea1c7d480b3223f7c8a9aa0e172"
DOWNLOAD_x86_64=""
MD5SUM_x86_64=""
-REQUIRES="jdk libantlr3c"
+REQUIRES="jdk libantlr3c python-toml"
MAINTAINER="Nick Smallbone"
EMAIL="nick@smallbone.se"