CHECKSUM

89d185fa3e0d3620703ad4b723ef85695ce427da6235fe91d74fc22d1ffcfd5d  coq-8.3pl5.tar.gz
f46ae5b6f0bea9dc299de6f3c020ee75c40581e32a1832e9a290d098a6a2424d  coq-8.4.tar.gz
5d0e4553ab50677a94b4d5ca1650a90718e9362082a649ba95be4010390a0f80  coq-8.4pl1.tar.gz
fb719a38f613b01861e3b251e745a5c8ef395a26ce7029668e85ac75fcbca2d8  coq-8.4pl2.tar.gz
97583d637f981c5554007f4e99ce6420ebc737186b1d021bd71766fd891cfb38  coq-8.4pl3.tar.gz
85a728e28346dec378d5437f7c409eab20bd42aa528b5f873cb0c9827d5baaa3  mathcomp-1.5rc1.tar.gz
5d0769c1639dcccbfe57407591ddfc12dee163c46fc012b307f17aedb5ab4d1d  ssreflect-1.4-coq8.3pl4.tar.gz
f044de8f75008000caf0ad61829f936384ee2d4b5fa40630352826c07b125dfb  ssreflect-1.4-coq8.4.tar.gz
f85d8ced769b6c38a499681a52480f2e0b9b7a0a8f028a3d35ecd1794ae64fc2  ssreflect-1.5rc1.tar.gz

install-coq

#!/bin/zsh

getfile(){
    if [[ ! -e $2 ]]; then
        wget $1 -O $2
    fi
    if ! (grep " $(printf %q $2)\$" CHECKSUM | sha256sum -c -); then
        echo 'error: getfile $@'
        exit
    fi
}

VERSION=$1
PREFIX=/usr/local/coq$VERSION
CAMLP5DIR=$(ocamlfind query camlp5)
JOBS=4

DIR=$(mktemp -d)

getfile "http://coq.inria.fr/distrib/V${VERSION}/files/coq-${VERSION}.tar.gz" "coq-${VERSION}.tar.gz"
tar xzf coq-${VERSION}.tar.gz -C $DIR
pushd $DIR/coq-$VERSION
    make archclean
    ./configure -prefix $PREFIX -camlp5dir $CAMLP5DIR
    make world -j $JOBS
    sudo make install
popd

export COQBIN=$PREFIX/bin/
export PATH=$COQBIN:$PATH

case $VERSION in
"8.3pl5" )
cat <<EOT
ssreflect-1.4-coq8.3pl4 ssreflect-1.4
EOT
;;
"8.4"|"8.4pl1"|"8.4pl2"|"8.4pl3" )
cat <<EOT
ssreflect-1.4-coq8.4 ssreflect-1.4 Ssreflect
ssreflect-1.5rc1 ssreflect-1.5 Ssreflect
mathcomp-1.5rc1 mathcomp-1.5 MathComp ssreflect-1.5,Ssreflect
EOT
;;
esac | while read pkgname dirname libname deps; do
    COQLIBS=(-R theories $libname)
    COQC=$COQBIN/coqc
    echo $deps | sed -s 's/;/\n/g; s/,/ /g' | while read dirname_ libname_; do
        [ "$libname_" = Ssreflect ] && COQC=$PREFIX/$dirname_/bin/ssrcoq
        [ -n "$dirname_" ] && COQLIBS=($COQLIBS -R $PREFIX/$dirname_/theories $libname_)
    done
    COQDOCLIBS=$COQLIBS
    getfile "http://ssr.msr-inria.inria.fr/FTP/$pkgname.tar.gz" $pkgname.tar.gz
    sudo tar xzf $pkgname.tar.gz -C $PREFIX
    [ -f $pkgname.patch ] && sudo patch -p0 -d $PREFIX/$dirname/ < $pkgname.patch
    pushd $PREFIX/$dirname
        [ -d src ] && COQLIBS=(-I src $COQLIBS)
        sudo PATH="$PATH" make COQLIBS="$COQLIBS" -j $JOBS
        sudo PATH="$PATH" make COQDOCLIBS="$COQDOCLIBS" -j $JOBS -f Makefile.coq html gallinahtml
    popd
done

rm -rf $DIR