diff options
Diffstat (limited to 'academic/cvc4')
| -rw-r--r-- | academic/cvc4/README | 6 | ||||
| -rw-r--r-- | academic/cvc4/cvc4.SlackBuild | 43 | ||||
| -rw-r--r-- | academic/cvc4/cvc4.info | 8 | ||||
| -rw-r--r-- | academic/cvc4/slack-desc | 2 |
4 files changed, 42 insertions, 17 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..0d2d843636 100644 --- a/academic/cvc4/cvc4.SlackBuild +++ b/academic/cvc4/cvc4.SlackBuild @@ -1,8 +1,8 @@ -#!/bin/sh +#!/bin/bash # 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,10 +22,17 @@ # 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?) + +cd $(dirname $0) ; CWD=$(pwd) + PRGNAM=cvc4 -VERSION=${VERSION:-1.7} +VERSION=${VERSION:-1.8} BUILD=${BUILD:-1} TAG=${TAG:-_SBo} +PKGTYPE=${PKGTYPE:-tgz} SRCNAM=CVC4 if [ -z "$ARCH" ]; then @@ -36,7 +43,14 @@ if [ -z "$ARCH" ]; then esac fi -CWD=$(pwd) +# If the variable PRINT_PACKAGE_NAME is set, then this script will report what +# the name of the created package would be, and then exit. This information +# could be useful to other scripts. +if [ ! -z "${PRINT_PACKAGE_NAME}" ]; then + echo "$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.$PKGTYPE" + exit 0 +fi + TMP=${TMP:-/tmp/SBo} PKG=$TMP/package-$PRGNAM OUTPUT=${OUTPUT:-/tmp} @@ -70,22 +84,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 {} \; @@ -101,4 +122,4 @@ mkdir -p $PKG/install cat $CWD/slack-desc > $PKG/install/slack-desc cd $PKG -/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.${PKGTYPE:-tgz} +/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.$PKGTYPE diff --git a/academic/cvc4/cvc4.info b/academic/cvc4/cvc4.info index 9058f04efd..379b15bffa 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://ponce.cc/slackware/sources/repo/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="zulu-openjdk8 libantlr3c python2-toml" MAINTAINER="Nick Smallbone" EMAIL="nick@smallbone.se" diff --git a/academic/cvc4/slack-desc b/academic/cvc4/slack-desc index d99cfab40f..7916878a78 100644 --- a/academic/cvc4/slack-desc +++ b/academic/cvc4/slack-desc @@ -13,7 +13,7 @@ cvc4: theories (SMT) solver. Given a formula in first-order logic, it cvc4: attempts to either prove the formula or find a counterexample. CVC4 cvc4: supports arithmetic, reasoning about arrays, and several other cvc4: built-in theories. Input problems are written in SMT-LIB format. -cvc4: +cvc4: cvc4: This package includes the cvc4 program as well as libraries. cvc4: cvc4: Homepage: https://cvc4.cs.stanford.edu/ |