diff options
author | Juan M. Lasca <juanmlasca@gmail.com> | 2013-03-11 21:13:19 -0400 |
---|---|---|
committer | dsomero <xgizzmo@slackbuilds.org> | 2013-03-22 07:16:40 -0400 |
commit | 17ef36e40eb0d9183fcd7a29e9ddda3d1a96950a (patch) | |
tree | 2298a88258830f60812a9814568c8563e4bea06d | |
parent | d30c249588095443f15225c70d35f8099efff699 (diff) | |
download | slackbuilds-17ef36e40eb0d9183fcd7a29e9ddda3d1a96950a.tar.gz |
academic/aris: Added (sequential proof program)
Signed-off-by: dsomero <xgizzmo@slackbuilds.org>
-rw-r--r-- | academic/aris/README | 6 | ||||
-rw-r--r-- | academic/aris/aris.SlackBuild | 85 | ||||
-rw-r--r-- | academic/aris/aris.info | 10 | ||||
-rw-r--r-- | academic/aris/slack-desc | 19 |
4 files changed, 120 insertions, 0 deletions
diff --git a/academic/aris/README b/academic/aris/README new file mode 100644 index 0000000000..65cf47df47 --- /dev/null +++ b/academic/aris/README @@ -0,0 +1,6 @@ +GNU Aris is a sequential proof program, designed to assist anyone interested +in solving logical proofs. Aris supports both propositional and predicate +logic, as well as Boolean algebra and arithmetical logic in the form of +abstract sequences. It uses a predefined set of both inference and equivalence +rules, however gives the user options to use older proofs as lemmas, including +Isabelle's Isar proofs. diff --git a/academic/aris/aris.SlackBuild b/academic/aris/aris.SlackBuild new file mode 100644 index 0000000000..ce7cf5c010 --- /dev/null +++ b/academic/aris/aris.SlackBuild @@ -0,0 +1,85 @@ +#!/bin/sh + +# Slackware build script for GNU aris + +# Written by Juan M. Lasca <juanmlasca@gmail.com> + +PRGNAM=aris +VERSION=${VERSION:-2.0} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i486 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +CWD=$(pwd) +TMP=${TMP:-/tmp/SBo} +PKG=$TMP/package-$PRGNAM +OUTPUT=${OUTPUT:-/tmp} + +if [ "$ARCH" = "i486" ]; then + SLKCFLAGS="-O2 -march=i486 -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 $PRGNAM-$VERSION +tar xvf $CWD/$PRGNAM-$VERSION.tar.bz2 +cd $PRGNAM-$VERSION +chown -R root:root . +find . \ + \( -perm 777 -o -perm 775 -o -perm 711 -o -perm 555 -o -perm 511 \) \ + -exec chmod 755 {} \; -o \ + \( -perm 666 -o -perm 664 -o -perm 600 -o -perm 444 -o -perm 440 -o -perm 400 \) \ + -exec chmod 644 {} \; + + +CFLAGS="$SLKCFLAGS" \ +CXXFLAGS="$SLKCFLAGS" \ +./configure \ + --prefix=/usr \ + --libdir=/usr/lib${LIBDIRSUFFIX} \ + --sysconfdir=/etc \ + --localstatedir=/var \ + --docdir=/usr/doc/$PRGNAM \ + --build=$ARCH-slackware-linux + +make +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 + +# "make install" won't locate the aris.info file in DESTDIR. +# Workaround: +mkdir -p $PKG/usr/info +cp -a doc/$PRGNAM.info $PKG/usr/info/ +gzip -9 $PKG/usr/info/$PRGNAM.info + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a README $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/aris/aris.info b/academic/aris/aris.info new file mode 100644 index 0000000000..d618e540cf --- /dev/null +++ b/academic/aris/aris.info @@ -0,0 +1,10 @@ +PRGNAM="aris" +VERSION="2.0" +HOMEPAGE="http://www.gnu.org/software/aris/" +DOWNLOAD="http://ftp.gnu.org/gnu/aris/aris-2.0.tar.bz2" +MD5SUM="696523a812cbe19223482b8f27d04fc0" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +REQUIRES="" +MAINTAINER="Juan M. Lasca" +EMAIL="juanmlasca@gmail.com" diff --git a/academic/aris/slack-desc b/academic/aris/slack-desc new file mode 100644 index 0000000000..218444d055 --- /dev/null +++ b/academic/aris/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------------------------------------------------------| +aris: aris (sequential proof program) +aris: +aris: GNU Aris is a sequential proof program, designed to assist anyone +aris: interested in solving logical proofs. Aris supports both propositional +aris: and predicate logic, as well as Boolean algebra and arithmetical logic +aris: in the form of abstract sequences. It uses a predefined set of both +aris: inference and equivalence rules, however gives the user options to use +aris: older proofs as lemmas, including Isabelle's Isar proofs. +aris: +aris: Home page: http://www.gnu.org/software/aris/ +aris: |