From 5c892d971b7ddf69670fc13660611448edc44430 Mon Sep 17 00:00:00 2001 From: Jefferson Rocha Date: Sat, 10 Aug 2019 01:23:33 +0700 Subject: academic/abella: Added (interactive theorem prover). Signed-off-by: Willy Sudiarto Raharjo --- academic/abella/README | 25 +++++++++++++ academic/abella/abella.SlackBuild | 78 +++++++++++++++++++++++++++++++++++++++ academic/abella/abella.info | 10 +++++ academic/abella/slack-desc | 19 ++++++++++ 4 files changed, 132 insertions(+) create mode 100644 academic/abella/README create mode 100644 academic/abella/abella.SlackBuild create mode 100644 academic/abella/abella.info create mode 100644 academic/abella/slack-desc (limited to 'academic') diff --git a/academic/abella/README b/academic/abella/README new file mode 100644 index 0000000000..aa13f891cd --- /dev/null +++ b/academic/abella/README @@ -0,0 +1,25 @@ +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 new file mode 100644 index 0000000000..ea575be990 --- /dev/null +++ b/academic/abella/abella.SlackBuild @@ -0,0 +1,78 @@ +#!/bin/sh +# 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 +PRGNAM=abella +VERSION=${VERSION:-2.0.6} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} +ARCH=noarch +CWD=$(pwd) +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:-tgz} diff --git a/academic/abella/abella.info b/academic/abella/abella.info new file mode 100644 index 0000000000..88abb3f04c --- /dev/null +++ b/academic/abella/abella.info @@ -0,0 +1,10 @@ +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 new file mode 100644 index 0000000000..15174390e7 --- /dev/null +++ b/academic/abella/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 ':'. + + |-----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: -- cgit v1.2.3