diff options
author | Matteo Bernardini <ponce@slackbuilds.org> | 2022-02-24 22:37:44 +0100 |
---|---|---|
committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2022-02-25 22:58:10 +0700 |
commit | a50076c98145a8c1d152afcc1675fafed5cb85a5 (patch) | |
tree | 06d313513d50879801586c49bed2579b57705570 /academic/coq | |
parent | 33064fb6bf044cd2992d0aaee95a3698a2bcff4b (diff) |
academic/coq: Removed (ftb).
Signed-off-by: Matteo Bernardini <ponce@slackbuilds.org>
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic/coq')
-rw-r--r-- | academic/coq/README | 10 | ||||
-rw-r--r-- | academic/coq/coq.SlackBuild | 113 | ||||
-rw-r--r-- | academic/coq/coq.info | 10 | ||||
-rw-r--r-- | academic/coq/slack-desc | 19 |
4 files changed, 0 insertions, 152 deletions
diff --git a/academic/coq/README b/academic/coq/README deleted file mode 100644 index 30daf046e352f..0000000000000 --- a/academic/coq/README +++ /dev/null @@ -1,10 +0,0 @@ -coq is a formal proof management system. It provides a formal language -to write mathematical definitions, executable algorithms and theorems -together with an environment for semi-interactive development of -machine-checked proofs. - -Unfortunately CoqIDE can no longer be built as it requires lablgtk3, -while only lablgtk2 is packaged in Slackware. You can however get -Coq 8.9 with CoqIDE. To do so, run this Slackbuild with VERSION=8.9 -and COQIDE=yes (after getting the Coq 8.9 tarball). You will need to -install the gtksourceview package before building lablgtk. diff --git a/academic/coq/coq.SlackBuild b/academic/coq/coq.SlackBuild deleted file mode 100644 index c1454a844d1fc..0000000000000 --- a/academic/coq/coq.SlackBuild +++ /dev/null @@ -1,113 +0,0 @@ -#!/bin/bash - -# Slackware build script for coq - -# Copyright 2020-2022 Nick Smallbone <nick@smallbone.se>, 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. - -cd $(dirname $0) ; CWD=$(pwd) - -PRGNAM=coq -VERSION=${VERSION:-8.12.2} -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 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} - -if [ "$ARCH" = "i586" ]; then - LIBDIRSUFFIX="" -elif [ "$ARCH" = "i686" ]; then - LIBDIRSUFFIX="" -elif [ "$ARCH" = "x86_64" ]; then - LIBDIRSUFFIX="64" -else - LIBDIRSUFFIX="" -fi - -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 -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 {} \; - -CONFIG_ARGS= -if [ z$COQIDE = zyes ];then - CONFIG_ARGS+=" -coqide opt" -else - CONFIG_ARGS+=" -coqide no" -fi - -./configure \ - -prefix /usr \ - -libdir /usr/lib${LIBDIRSUFFIX}/$PRGNAM \ - -configdir /etc/xdg/$PRGNAM \ - -mandir /usr/man \ - -docdir /usr/doc/$PRGNAM-$VERSION \ - -arch $ARCH \ - $CONFIG_ARGS - -make -make install COQINSTALLPREFIX=$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 - -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 \ - CONTRIBUTING.md CREDITS INSTALL.md LICENSE README.md \ - $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/coq/coq.info b/academic/coq/coq.info deleted file mode 100644 index 7803effa6dd1f..0000000000000 --- a/academic/coq/coq.info +++ /dev/null @@ -1,10 +0,0 @@ -PRGNAM="coq" -VERSION="8.12.2" -HOMEPAGE="http://coq.inria.fr/" -DOWNLOAD="https://github.com/coq/coq/archive/V8.12.2/coq-8.12.2.tar.gz" -MD5SUM="e6746ce2c527e8f9d69a57dc2f7d41d1" -DOWNLOAD_x86_64="" -MD5SUM_x86_64="" -REQUIRES="ocaml-num" -MAINTAINER="Nick Smallbone" -EMAIL="nick@smallbone.se" diff --git a/academic/coq/slack-desc b/academic/coq/slack-desc deleted file mode 100644 index a5c16bf09200f..0000000000000 --- a/academic/coq/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 ':' except on otherwise blank lines. - - |-----handy-ruler------------------------------------------------------| -coq: coq (The Coq Proof Assistant) -coq: -coq: coq is a formal proof management system. It provides a formal language -coq: to write mathematical definitions, executable algorithms and theorems -coq: together with an environment for semi-interactive development of -coq: machine-checked proofs. -coq: -coq: Homepage: https://coq.inria.fr/ -coq: -coq: -coq: |