academic/coq: Updated for version 8.9.0.

Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>

4 files changed, 57 insertions, 61 deletions

diff --git a/academic/coq/README b/academic/coq/README
index 81ec48f0d65e7..e21de9a5fab1e 100644
--- a/academic/coq/README
+++ b/academic/coq/README
@@ -1,14 +1,7 @@
-Coq implements a program specification and mathematical higher-level
-language called Gallina that is based on an expressive formal language
-called the Calculus of Inductive Constructions that itself combines both
-a higher-order logic and a richly-typed functional programming language.
+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.
 
-If you have ocamlopt, Coq will be compiled to native code, which runs 4-10 
-times faster. For best performance, OCaml should have support for pthreads. 
-
-If you want CoqIDE, you need LablGTK2 (>= 2.10.0) with development
-files, and GTK2+ (>= 2.10.0).  This also REQUIRES OCaml to have support
-for pthreads.
-
-If you have emacs installed, emacs files for Coq will be installed.
-Otherwise, they will be omitted.
+To build CoqIDE, add COQIDE=yes, e.g.: COQIDE=yes ./coq.SlackBuild.
+You will need the lablgtk package built with gtksourceview support.
diff --git a/academic/coq/coq.SlackBuild b/academic/coq/coq.SlackBuild
index c0aca0054a048..afa9d5f58f08f 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}
diff --git a/academic/coq/coq.info b/academic/coq/coq.info
index 9cd9d5bb917b3..93554ae125b58 100644
--- a/academic/coq/coq.info
+++ b/academic/coq/coq.info
@@ -1,10 +1,10 @@
 PRGNAM="coq"
-VERSION="8.5pl1"
+VERSION="8.9.0"
 HOMEPAGE="http://coq.inria.fr/"
-DOWNLOAD="https://coq.inria.fr/distrib/V8.5pl1/files/coq-8.5pl1.tar.gz"
-MD5SUM="1faa8a237c3e81905dc938b6b727b807"
+DOWNLOAD="https://github.com/coq/coq/archive/V8.9.0/coq-8.9.0.tar.gz"
+MD5SUM="490c89609c1271fe7f20e6ea1bd107b5"
 DOWNLOAD_x86_64=""
 MD5SUM_x86_64=""
-REQUIRES="camlp5"
-MAINTAINER="William Bowman"
-EMAIL="wilbowma@indiana.edu"
+REQUIRES="camlp5 ocaml-findlib"
+MAINTAINER="Nick Smallbone"
+EMAIL="nick@smallbone.se"
diff --git a/academic/coq/slack-desc b/academic/coq/slack-desc
index badd05cb0ba03..a5c16bf09200f 100644
--- a/academic/coq/slack-desc
+++ b/academic/coq/slack-desc
@@ -13,7 +13,7 @@ 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: Homepage: http://coq.inria.fr/
 coq:
 coq: