From 5c87535b2ca5481412501ddd907e89962352ea89 Mon Sep 17 00:00:00 2001 From: Nick Smallbone Date: Sat, 23 Feb 2019 07:47:50 +0700 Subject: academic/eprover: Added (a first-order theorem prover). Signed-off-by: Willy Sudiarto Raharjo --- academic/eprover/README | 1 + academic/eprover/eprover.SlackBuild | 101 ++++++++++++++++++++++++++++++++++++ academic/eprover/eprover.info | 10 ++++ academic/eprover/slack-desc | 19 +++++++ 4 files changed, 131 insertions(+) create mode 100644 academic/eprover/README create mode 100644 academic/eprover/eprover.SlackBuild create mode 100644 academic/eprover/eprover.info create mode 100644 academic/eprover/slack-desc diff --git a/academic/eprover/README b/academic/eprover/README new file mode 100644 index 0000000000..f123407313 --- /dev/null +++ b/academic/eprover/README @@ -0,0 +1 @@ +E is an automated theorem prover for first-order and equational logic. diff --git a/academic/eprover/eprover.SlackBuild b/academic/eprover/eprover.SlackBuild new file mode 100644 index 0000000000..723e70713b --- /dev/null +++ b/academic/eprover/eprover.SlackBuild @@ -0,0 +1,101 @@ +#!/bin/sh + +# Slackware build script for eprover + +# Copyright 2019 Nick Smallbone, Gothenburg, Sweden +# All rights reserved. +# +# Redistribution and use of this script, with or without modification, is +# permitted provided that the following conditions are met: +# +# 1. Redistributions of this script must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# THIS SOFTWARE IS PROVIDED BY THE AUTHOR "AS IS" AND ANY EXPRESS OR IMPLIED +# WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO +# EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; +# OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, +# WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR +# OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF +# ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +PRGNAM=eprover +VERSION=${VERSION:-2.2} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i586 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +CWD=$(pwd) +TMP=${TMP:-/tmp/SBo} +PKG=$TMP/package-$PRGNAM +OUTPUT=${OUTPUT:-/tmp} + +if [ "$ARCH" = "i586" ]; then + SLKCFLAGS="-O2 -march=i586 -mtune=i686" + LIBDIRSUFFIX="" +elif [ "$ARCH" = "i686" ]; then + SLKCFLAGS="-O2 -march=i686 -mtune=i686" + LIBDIRSUFFIX="" +elif [ "$ARCH" = "x86_64" ]; then + SLKCFLAGS="-O2 -fPIC" + LIBDIRSUFFIX="64" +else + SLKCFLAGS="-O2" + LIBDIRSUFFIX="" +fi + +set -e + +rm -rf $PKG +mkdir -p $TMP $PKG $OUTPUT +cd $TMP +rm -rf E +tar xvf $CWD/E.tgz +cd E +chown -R root:root . +find -L . \ + \( -perm 777 -o -perm 775 -o -perm 750 -o -perm 711 -o -perm 555 \ + -o -perm 511 \) -exec chmod 755 {} \; -o \ + \( -perm 666 -o -perm 664 -o -perm 640 -o -perm 600 -o -perm 444 \ + -o -perm 440 -o -perm 400 \) -exec chmod 644 {} \; + +# The makefile doesn't support DESTDIR, but luckily it doesn't use the +# configured --bindir and --man-prefix until install time. +CFLAGS="$SLKCFLAGS" \ +CXXFLAGS="$SLKCFLAGS" \ +./configure \ + --bindir=$PKG/usr/bin \ + --man-prefix=$PKG/usr/man/man1 + +make +make install +# The picosat binary is not used by E but gets installed anyway. +rm $PKG/usr/bin/picosat + +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 + +find $PKG/usr/man -type f -exec gzip -9 {} \; +for i in $( find $PKG/usr/man -type l ) ; do ln -s $( readlink $i ).gz $i.gz ; rm $i ; done + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a \ + README COPYING DOC/CONTRIBUTORS DOC/eprover.pdf DOC/NEWS \ + $PKG/usr/doc/$PRGNAM-$VERSION +cat $CWD/$PRGNAM.SlackBuild > $PKG/usr/doc/$PRGNAM-$VERSION/$PRGNAM.SlackBuild + +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} diff --git a/academic/eprover/eprover.info b/academic/eprover/eprover.info new file mode 100644 index 0000000000..fee24f2a05 --- /dev/null +++ b/academic/eprover/eprover.info @@ -0,0 +1,10 @@ +PRGNAM="eprover" +VERSION="2.2" +HOMEPAGE="http://www.eprover.org" +DOWNLOAD="http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.2/E.tgz" +MD5SUM="62800b607d19e544856671318597aa3d" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +REQUIRES="" +MAINTAINER="Nick Smallbone" +EMAIL="nick@smallbone.se" diff --git a/academic/eprover/slack-desc b/academic/eprover/slack-desc new file mode 100644 index 0000000000..fa5448b269 --- /dev/null +++ b/academic/eprover/slack-desc @@ -0,0 +1,19 @@ +# HOW TO EDIT THIS FILE: +# The "handy ruler" below makes it easier to edit a package description. +# Line up the first '|' above the ':' following the base package name, and +# the '|' on the right side marks the last column you can put a character in. +# You must make exactly 11 lines for the formatting to be correct. It's also +# customary to leave one space after the ':' except on otherwise blank lines. + + |-----handy-ruler------------------------------------------------------| +eprover: eprover (a first-order theorem prover) +eprover: +eprover: E is an automated theorem prover for first-order and equational logic. +eprover: +eprover: Homepage: http://www.eprover.org/ +eprover: +eprover: +eprover: +eprover: +eprover: +eprover: -- cgit v1.2.3