# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
# $Id$

PortSystem          1.0

name                coq
version             8.4pl4
platforms           darwin
categories          lang math
license             LGPL-2.1
maintainers         piermont.com:perry

description         Proof assistant for higher-order logic
long_description    Coq is a proof assistant for higher-order logic, \
                    which allows the development of computer programs \
                    consistent with their formal specification. It is \
                    developed using Objective Caml and Camlp4.
homepage            http://coq.inria.fr/

depends_lib         port:ocaml \
                    port:camlp5

master_sites        http://coq.inria.fr/distrib/V${version}/files/
checksums           rmd160  19e3fe905f5db09710b1f862f21e9b57c28f9704 \
                    sha256  06c3aeab7819eed8f35ce794c887a70cf3b4f6b71ee52cd3110fb4e526717f01

configure.pre_args  -prefix ${prefix}
configure.args      -emacslib ${prefix}/share/emacs/site-lisp/ \
                    -mandir ${prefix}/share/man \
                    -coqdocdir ${prefix}/share/coq/latex \
                    -coqide none \
                    -with-doc no
build.target        world

destroot.target     install
destroot.destdir    COQINSTALLPREFIX=${destroot}

# ocaml is not universal
universal_variant   no

notes "
The style file for LaTeX documentation,\
coqdoc.sty, is in ${prefix}/share/coq/latex.\
Add this to your TEXINPUTS if you wish to\
use it.
"

variant doc description {Build documentation} {
    depends_build-append    port:hevea \
                            port:netpbm \
                            port:texlive
    configure.args-delete   -with-doc no
    configure.args-append   -with-doc yes
    use_parallel_build      no
}

variant coqide description {Install CoqIDE} {
    depends_lib-append      port:lablgtk2
    configure.args-delete   -coqide none
    configure.args-append   -coqide opt
}

livecheck.type      regex
livecheck.url       ${homepage}/download/
livecheck.regex     "<a href=\"distrib/V(\\d+(?:\\.\\w+)*)/files/coq-\\1\\.tar\\.gz\">"