From 9c5891220650cba882d6d7eee1216b7dc23a2415 Mon Sep 17 00:00:00 2001 From: Lockywolf Date: Tue, 18 Jul 2023 08:47:19 +0700 Subject: [PATCH] academic/Isabelle: Added (proof assistant). Signed-off-by: Willy Sudiarto Raharjo --- academic/Isabelle/Isabelle | 3 + academic/Isabelle/Isabelle.SlackBuild | 82 +++++++++++++++++++++++++++ academic/Isabelle/Isabelle.info | 10 ++++ academic/Isabelle/README | 17 ++++++ academic/Isabelle/slack-desc | 19 +++++++ 5 files changed, 131 insertions(+) create mode 100644 academic/Isabelle/Isabelle create mode 100644 academic/Isabelle/Isabelle.SlackBuild create mode 100644 academic/Isabelle/Isabelle.info create mode 100644 academic/Isabelle/README create mode 100644 academic/Isabelle/slack-desc diff --git a/academic/Isabelle/Isabelle b/academic/Isabelle/Isabelle new file mode 100644 index 0000000000..24f157255a --- /dev/null +++ b/academic/Isabelle/Isabelle @@ -0,0 +1,3 @@ +#!/bin/sh + +exec /opt/Isabelle/MY_TEMPLATE $@ diff --git a/academic/Isabelle/Isabelle.SlackBuild b/academic/Isabelle/Isabelle.SlackBuild new file mode 100644 index 0000000000..eb9721e53d --- /dev/null +++ b/academic/Isabelle/Isabelle.SlackBuild @@ -0,0 +1,82 @@ +#!/bin/bash + +# Slackware build script for Isabelle + +# Copyright 2023, Lockywolf +# 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. + + +cd $(dirname $0) ; CWD=$(pwd) + +PRGNAM=Isabelle +VERSION=${VERSION:-2022} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} +PKGTYPE=${PKGTYPE:-tgz} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i586 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +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} + +set -e + +rm -rf $PKG +mkdir -p $TMP $PKG $OUTPUT +cd $TMP +rm -rf $PRGNAM$VERSION +tar xvf $CWD/$PRGNAM${VERSION}_linux.tar.gz +cd $PRGNAM$VERSION +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 {} \; + +install -Dm755 $CWD/Isabelle $PKG/usr/bin/Isabelle +install -d -m 755 $PKG/opt/$PRGNAM +cp -r . $PKG/opt/$PRGNAM +sed -i "s/MY_TEMPLATE/$PRGNAM$VERSION/g" $PKG/usr/bin/Isabelle + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a \ +ANNOUNCE COPYRIGHT doc README ROOTS \ +CONTRIBUTORS Isabelle.options NEWS ROOT \ + $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 diff --git a/academic/Isabelle/Isabelle.info b/academic/Isabelle/Isabelle.info new file mode 100644 index 0000000000..effbc710fb --- /dev/null +++ b/academic/Isabelle/Isabelle.info @@ -0,0 +1,10 @@ +PRGNAM="Isabelle" +VERSION="2022" +HOMEPAGE="https://isabelle.in.tum.de/" +DOWNLOAD="UNSUPPORTED" +MD5SUM="" +DOWNLOAD_x86_64="https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz" +MD5SUM_x86_64="52340538b76b0493beae0a444d623fe6" +REQUIRES="" +MAINTAINER="Lockywolf" +EMAIL="for_sbo.Isabelle_2023-07-17@lockywolf.net" diff --git a/academic/Isabelle/README b/academic/Isabelle/README new file mode 100644 index 0000000000..133899ddbe --- /dev/null +++ b/academic/Isabelle/README @@ -0,0 +1,17 @@ +Isabelle is a generic proof assistant. It allows mathematical formulas +to be expressed in a formal language and provides tools for proving +those formulas in a logical calculus. Isabelle was originally +developed at the University of Cambridge and Technische Universität +München, but now includes numerous contributions from institutions and +individuals worldwide. + +Isabelle is written in polyML, Java, and Scala, but does not require +them to be installed from SBo. + +This build is bundling: jEdit, vscodium, jdk-17, so be careful about +its interference with other packages. + +A lot of proofs certified with Isabelle can be found on +https://www.isa-afp.org/ + +This build repackages the binary build. diff --git a/academic/Isabelle/slack-desc b/academic/Isabelle/slack-desc new file mode 100644 index 0000000000..72e6651a95 --- /dev/null +++ b/academic/Isabelle/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------------------------------------------------------| +Isabelle: Isabelle (generic proof assistant) +Isabelle: +Isabelle: Isabelle is a generic proof assistant. It allows mathematical +Isabelle: formulas to be expressed in a formal language and provides tools for +Isabelle: proving those formulas in a logical calculus. Isabelle was +Isabelle: originally developed at the University of Cambridge and Technische +Isabelle: Universitat Munchen, but now includes numerous contributions from +Isabelle: institutions and individuals worldwide. +Isabelle: +Isabelle: +Isabelle: