diff --git a/academic/abella/README b/academic/abella/README deleted file mode 100644 index 7954d1e751..0000000000 --- a/academic/abella/README +++ /dev/null @@ -1,33 +0,0 @@ -Abella is an interactive theorem prover based on lambda-tree syntax. - -This means that Abella is well-suited for reasoning about the -meta-theory of programming languages and other logical systems -which manipulate objects with binding. For example, the following -applications are included in the distribution of Abella. - -* Various results on the lambda calculus involving big-step - evaluation, small-step evaluation, and typing judgments -* Cut-admissibility for a sequent calculus -* Part 1a and Part 2a of the POPLmark challenge -* Takahashi's proof of the Church-Rosser theorem -* Tait's logical relations argument for weak normalization of the - simply-typed lambda calculus -* Girard's proof of strong normalization of the simply-typed lambda - calculus -* Some ?-calculus meta-theory -* Relation between ?-reduction and paths in A-calculus - -For Full List: -http://abella-prover.org/examples/index.html - -Abella uses a two-level logic approach to reasoning. Specifications -are made in the logic of second-order hereditary Harrop formulas using -lambda-tree syntax. This logic is executable and is a subset of the -AProlog language (see the Teyjus system for an implementation of this -language). - -The reasoning logic of Abella is the culmination of a series -of extensions to proof theory for the treatment of definitions, -lambda-tree syntax, and generic judgments. The reasoning logic of -Abella is able to encode the semantics of our specification logic as a -definition and thereby reason over specifications in that logic. diff --git a/academic/abella/abella.SlackBuild b/academic/abella/abella.SlackBuild deleted file mode 100644 index eb30ac337f..0000000000 --- a/academic/abella/abella.SlackBuild +++ /dev/null @@ -1,88 +0,0 @@ -#!/bin/bash -# Slackware build script for abella -# Copyright 2019 Jefferson Rocha -# 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. - -#==========================VARS -cd $(dirname $0) ; CWD=$(pwd) - -PRGNAM=abella -VERSION=${VERSION:-2.0.6} -BUILD=${BUILD:-1} -TAG=${TAG:-_SBo} -PKGTYPE=${PKGTYPE:-tgz} -ARCH=noarch -# 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} - -#Root? -[ "$UID" -ne '0' ] && { echo "Need root."; exit 1 ;} - -#=========================START -set -e - -rm -rf $PKG -mkdir -p $TMP $PKG $OUTPUT -cd $TMP - -rm -rf $PRGNAM-$VERSION -tar xvf $CWD/$PRGNAM-$VERSION.tar.gz -cd $PRGNAM-$VERSION - -# Fix Permissions -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 {} \; - -# Generate bin -make -strip -s $PRGNAM - -mkdir -p $PKG/usr/bin -cp "$PRGNAM" $PKG/usr/bin - -mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION - -# Send original Docs and archives -for create in "$PRGNAM.SlackBuild" 'LICENSE' 'CHANGES'; do - if [ "$create" = $PRGNAM.SlackBuild ]; then - cp $CWD/$create $PKG/usr/doc/$PRGNAM-$VERSION/ - else - cp $create $PKG/usr/doc/$PRGNAM-$VERSION/ - fi -done - -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 diff --git a/academic/abella/abella.info b/academic/abella/abella.info deleted file mode 100644 index 88abb3f04c..0000000000 --- a/academic/abella/abella.info +++ /dev/null @@ -1,10 +0,0 @@ -PRGNAM="abella" -VERSION="2.0.6" -HOMEPAGE="http://abella-prover.org/" -DOWNLOAD="http://abella-prover.org/distributions/abella-2.0.6.tar.gz" -MD5SUM="077cb3fbbdf35159e4b8860faf431c6a" -DOWNLOAD_x86_64="" -MD5SUM_x86_64="" -REQUIRES="ocamlbuild ocaml-findlib" -MAINTAINER="Jefferson Rocha" -EMAIL="root@slackjeff.com.br" diff --git a/academic/abella/slack-desc b/academic/abella/slack-desc deleted file mode 100644 index 15174390e7..0000000000 --- a/academic/abella/slack-desc +++ /dev/null @@ -1,19 +0,0 @@ -# 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 ':'. - - |-----handy-ruler------------------------------------------------------| -abella: abella (interactive theorem prover based on lambda-tree syntax) -abella: -abella: Abella is an interactive theorem prover based on lambda-tree syntax. -abella: This means that Abella is well-suited for reasoning about the meta -abella: theory of programming languages and other logical systems which -abella: manipulate objects with binding. -abella: For example, the following applications are included in the -abella: distribution of Abella. -abella: -abella: http://abella-prover.org/ -abella: