summaryrefslogtreecommitdiffstats
path: root/academic/coq/coq.SlackBuild
diff options
context:
space:
mode:
Diffstat (limited to 'academic/coq/coq.SlackBuild')
-rw-r--r--academic/coq/coq.SlackBuild85
1 files changed, 44 insertions, 41 deletions
diff --git a/academic/coq/coq.SlackBuild b/academic/coq/coq.SlackBuild
index c0aca0054a..afa9d5f58f 100644
--- a/academic/coq/coq.SlackBuild
+++ b/academic/coq/coq.SlackBuild
@@ -1,30 +1,35 @@
#!/bin/sh
+
+# Slackware build script for coq
+
+# Copyright 2020 Nick Smallbone <nick@smallbone.se>, Gothenburg, Sweden
+# All rights reserved.
#
-# This program is free software: you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# This program is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-# GNU General Public License for more details.
+# Redistribution and use of this script, with or without modification, is
+# permitted provided that the following conditions are met:
#
-# You should have received a copy of the GNU General Public License
-# along with this program. If not, see <http://www.gnu.org/licenses/>.
+# 1. Redistributions of this script must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
#
-# Slackware build script for coq
-
-# Written by William Bowman (wilbowma@indiana.edu)
+# 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.
PRGNAM=coq
-VERSION=${VERSION:-8.5pl1}
+VERSION=${VERSION:-8.9.0}
BUILD=${BUILD:-1}
TAG=${TAG:-_SBo}
if [ -z "$ARCH" ]; then
case "$( uname -m )" in
- i?86) ARCH=i486 ;;
+ i?86) ARCH=i586 ;;
arm*) ARCH=arm ;;
*) ARCH=$( uname -m ) ;;
esac
@@ -35,9 +40,7 @@ TMP=${TMP:-/tmp/SBo}
PKG=$TMP/package-$PRGNAM
OUTPUT=${OUTPUT:-/tmp}
-# This is built using the ocaml compiler, not GCC, so SLKCFLAGS are
-# not used.
-if [ "$ARCH" = "i486" ]; then
+if [ "$ARCH" = "i586" ]; then
LIBDIRSUFFIX=""
elif [ "$ARCH" = "i686" ]; then
LIBDIRSUFFIX=""
@@ -57,30 +60,36 @@ 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 600 -o -perm 444 -o -perm 440 -o -perm 400 \) \
- -exec chmod 644 {} \;
-
-
-if hash ocamlopt || hash ocamlopt.opt ; then
- OPT="-opt"
+ \( -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 {} \;
+
+# Configure findlib so it can find camlp5.
+cp /etc/findlib.conf .
+sed -i "s@path=\"@path=\"/usr/lib${LIBDIRSUFFIX}/ocaml:@" findlib.conf
+export OCAMLFIND_CONF=$(pwd)/findlib.conf
+
+CONFIG_ARGS=
+if [ z$COQIDE = zyes ];then
+ CONFIG_ARGS+=" -coqide opt"
else
- OPT=""
+ CONFIG_ARGS+=" -coqide no"
fi
./configure \
-prefix /usr \
- -libdir /usr/lib${LIBDIRSUFFIX}/coq \
+ -libdir /usr/lib${LIBDIRSUFFIX}/$PRGNAM \
+ -configdir /etc/xdg/$PRGNAM \
-mandir /usr/man \
+ -docdir /usr/doc/$PRGNAM-$VERSION \
-arch $ARCH \
- $OPT
+ $CONFIG_ARGS
-make world
-umask 022
-COQINSTALLPREFIX=$PKG make install
+make
+make install COQINSTALLPREFIX=$PKG
-find $PKG | xargs file | grep -e "executable" -e "shared object" | grep ELF \
+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 {} \;
@@ -88,18 +97,12 @@ for i in $( find $PKG/usr/man -type l ) ; do ln -s $( readlink $i ).gz $i.gz ; r
mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION
cp -a \
- CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL* LICENSE README* \
+ CHANGES.md CONTRIBUTING.md CREDITS INSTALL LICENSE README.md \
$PKG/usr/doc/$PRGNAM-$VERSION
cat $CWD/$PRGNAM.SlackBuild > $PKG/usr/doc/$PRGNAM-$VERSION/$PRGNAM.SlackBuild
-zcat $CWD/gpl.txt.gz > $PKG/usr/doc/$PRGNAM-$VERSION/$PRGNAM-SlackBuild-license
mkdir -p $PKG/install
cat $CWD/slack-desc > $PKG/install/slack-desc
-# Delete this if they don't have emacs. I don't like needless things
-if [ `which emacs | grep "no emacs"` ]; then
- rm -rf $PKG/usr/lib${LIBDIRSUFFIX}/emacs
-fi
-
cd $PKG
/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.${PKGTYPE:-tgz}