| 1 | # -*- 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 |
|---|
| 2 | # $Id: Portfile 150370 2016-07-18 20:33:02Z cal@macports.org $ |
|---|
| 3 | |
|---|
| 4 | PortSystem 1.0 |
|---|
| 5 | |
|---|
| 6 | name coq |
|---|
| 7 | version 8.5pl2 |
|---|
| 8 | platforms darwin |
|---|
| 9 | categories lang math |
|---|
| 10 | license LGPL-2.1 |
|---|
| 11 | maintainers piermont.com:perry openmaintainer |
|---|
| 12 | |
|---|
| 13 | description Proof assistant for higher-order logic |
|---|
| 14 | long_description Coq is a proof assistant for higher-order logic, \ |
|---|
| 15 | which allows the development of computer programs \ |
|---|
| 16 | consistent with their formal specification. It is \ |
|---|
| 17 | developed using Objective Caml and Camlp4. |
|---|
| 18 | homepage http://coq.inria.fr/ |
|---|
| 19 | |
|---|
| 20 | depends_lib port:ocaml \ |
|---|
| 21 | port:camlp5 |
|---|
| 22 | |
|---|
| 23 | master_sites http://coq.inria.fr/distrib/V${version}/files/ |
|---|
| 24 | checksums rmd160 55ddf2e77b42677c227fd9954789bf12410c63e7 \ |
|---|
| 25 | sha256 83239d1251bf6c54a9ca5045d738e469019b93ca601756bf982aab0654e4de73 |
|---|
| 26 | |
|---|
| 27 | configure.pre_args -prefix ${prefix} |
|---|
| 28 | configure.args -emacslib ${prefix}/share/emacs/site-lisp/ \ |
|---|
| 29 | -mandir ${prefix}/share/man \ |
|---|
| 30 | -coqdocdir ${prefix}/share/coq/latex \ |
|---|
| 31 | -coqide no \ |
|---|
| 32 | -with-doc no |
|---|
| 33 | build.target world |
|---|
| 34 | |
|---|
| 35 | destroot.target install |
|---|
| 36 | destroot.destdir COQINSTALLPREFIX=${destroot} |
|---|
| 37 | |
|---|
| 38 | # ocaml is not universal |
|---|
| 39 | universal_variant no |
|---|
| 40 | |
|---|
| 41 | notes " |
|---|
| 42 | The style file for LaTeX documentation,\ |
|---|
| 43 | coqdoc.sty, is in ${prefix}/share/coq/latex.\ |
|---|
| 44 | Add this to your TEXINPUTS if you wish to\ |
|---|
| 45 | use it. |
|---|
| 46 | " |
|---|
| 47 | |
|---|
| 48 | variant doc description {Build documentation} { |
|---|
| 49 | depends_build-append port:hevea \ |
|---|
| 50 | port:netpbm \ |
|---|
| 51 | port:texlive \ |
|---|
| 52 | port:texlive-latex-extra |
|---|
| 53 | configure.args-delete -with-doc no |
|---|
| 54 | configure.args-append -with-doc yes |
|---|
| 55 | use_parallel_build no |
|---|
| 56 | } |
|---|
| 57 | |
|---|
| 58 | variant coqide description {Install CoqIDE} { |
|---|
| 59 | depends_lib-append port:lablgtk2 |
|---|
| 60 | configure.args-delete -coqide none |
|---|
| 61 | configure.args-append -coqide opt |
|---|
| 62 | } |
|---|
| 63 | |
|---|
| 64 | livecheck.type regex |
|---|
| 65 | livecheck.url ${homepage}/download/ |
|---|
| 66 | livecheck.regex "<a href=\"distrib/V(\\d+(?:\\.\\w+)*)/files/coq-\\1\\.tar\\.gz\">" |
|---|
