From bef4f3c03fd2f42dbc028393bc09a88100be5ba1 Mon Sep 17 00:00:00 2001 From: William Bowman Date: Fri, 5 Aug 2011 11:11:34 -0300 Subject: academic/coq: Added (The Coq Proof Assistant) Signed-off-by: Niels Horn --- academic/coq/README | 19 ++++++++ academic/coq/coq.SlackBuild | 104 ++++++++++++++++++++++++++++++++++++++++++++ academic/coq/coq.info | 10 +++++ academic/coq/gpl.txt.gz | Bin 0 -> 12138 bytes academic/coq/slack-desc | 19 ++++++++ 5 files changed, 152 insertions(+) create mode 100644 academic/coq/README create mode 100644 academic/coq/coq.SlackBuild create mode 100644 academic/coq/coq.info create mode 100644 academic/coq/gpl.txt.gz create mode 100644 academic/coq/slack-desc (limited to 'academic/coq') diff --git a/academic/coq/README b/academic/coq/README new file mode 100644 index 0000000000..eec7b1118a --- /dev/null +++ b/academic/coq/README @@ -0,0 +1,19 @@ +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. + +This requires OCaml (>= 3.10.2), camlp5 (with "transitional mode", avoiding +version 5.0.0), and GNU Make (>= 3.81). 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. + +Note: camlp5 6.01 appears to have a bug that prevents Coq from building +correctly. This build has been tested with 6.02.3. + +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. diff --git a/academic/coq/coq.SlackBuild b/academic/coq/coq.SlackBuild new file mode 100644 index 0000000000..fe4011d7d8 --- /dev/null +++ b/academic/coq/coq.SlackBuild @@ -0,0 +1,104 @@ +#!/bin/sh +# +# 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. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . +# +# Slackware build script for coq + +# Written by William Bowman (wilbowma@indiana.edu) + +PRGNAM=coq +VERSION=${VERSION:-8.3pl2} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i486 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +CWD=$(pwd) +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 + 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 . \ + \( -perm 777 -o -perm 775 -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" +else + OPT="" +fi + +./configure \ + -prefix /usr \ + -libdir /usr/lib${LIBDIRSUFFIX}/coq \ + -arch $ARCH \ + $OPT + +make world +umask 022 +COQINSTALLPREFIX=$PKG make install + +find $PKG | xargs 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 \ + CHANGES COMPATIBILITY COPYRIGHT CREDITS INSTALL* LICENSE README* \ + $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 new file mode 100644 index 0000000000..f23d0bd09c --- /dev/null +++ b/academic/coq/coq.info @@ -0,0 +1,10 @@ +PRGNAM="coq" +VERSION="8.3pl2" +HOMEPAGE="http://coq.inria.fr/" +DOWNLOAD="http://coq.inria.fr/distrib/V8.3pl2/files/coq-8.3pl2.tar.gz" +MD5SUM="db415f6c5372f5a443699c62f5affcb4" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +MAINTAINER="William Bowman" +EMAIL="wilbowma@indiana.edu" +APPROVED="Niels Horn" diff --git a/academic/coq/gpl.txt.gz b/academic/coq/gpl.txt.gz new file mode 100644 index 0000000000..0ef740a4c7 Binary files /dev/null and b/academic/coq/gpl.txt.gz differ diff --git a/academic/coq/slack-desc b/academic/coq/slack-desc new file mode 100644 index 0000000000..935d8a8071 --- /dev/null +++ b/academic/coq/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------------------------------------------------------| +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: +coq: Homepage: http://coq.inria.fr/ +coq: +coq: -- cgit v1.2.3-80-g2a13