# $Id: Portfile 58218 2009-09-24 10:40:54Z jann@macports.org $

PortSystem  1.0

name        coq
version     8.2pl1
platforms   darwin
categories  lang math
maintainers loria.fr:reilles
homepage    http://coq.inria.fr/
master_sites ${homepage}V${version}/files/

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.  For more information, see <${homepage}>.

checksums           md5     36eed48bc63ada8abf27f96eb126906c \
                    sha1    4aed3302adc2edbaa5d97984512c1c13014bd649 \
                    rmd160  dd5758a94bb3de49967cec76baa33eb5169659ce

use_parallel_build yes
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
depends_lib        bin:ocamlc:ocaml port:camlp5
build.target       world 
destroot.target    install 
destroot.destdir   COQINSTALLPREFIX=${destroot}
patchfiles         patch-doc-tools-latex_filter.diff

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

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

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