diff options
| -rw-r--r-- | academic/coq/README | 19 | ||||
| -rw-r--r-- | academic/coq/coq.SlackBuild | 85 | ||||
| -rw-r--r-- | academic/coq/coq.info | 12 | ||||
| -rw-r--r-- | academic/coq/slack-desc | 2 |
4 files changed, 57 insertions, 61 deletions
diff --git a/academic/coq/README b/academic/coq/README index 81ec48f0d6..e21de9a5fa 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 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} diff --git a/academic/coq/coq.info b/academic/coq/coq.info index 9cd9d5bb91..93554ae125 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 badd05cb0b..a5c16bf092 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: |