| 1 | # $Id: $ |
|---|
| 2 | |
|---|
| 3 | PortSystem 1.0 |
|---|
| 4 | |
|---|
| 5 | name ssreflect |
|---|
| 6 | version 1.2 |
|---|
| 7 | platforms darwin |
|---|
| 8 | categories lang math |
|---|
| 9 | maintainers nomaintainer |
|---|
| 10 | homepage http://www.msr-inria.inria.fr/Projects/math-components/ |
|---|
| 11 | master_sites ${homepage} |
|---|
| 12 | extract.suffix .tgz |
|---|
| 13 | |
|---|
| 14 | description A Small Scale Reflection Extension for the Coq system |
|---|
| 15 | long_description \ |
|---|
| 16 | The name Ssreflect stands for \"small scale reflection\", a style of \ |
|---|
| 17 | proof that evolved from the computer-checked proof of the Four Colour \ |
|---|
| 18 | Theorem and which leverages the higher-order nature of Coq\'s \ |
|---|
| 19 | underlying logic to provide effective automation for many small, \ |
|---|
| 20 | clerical proof steps. This is often accomplished by restating \ |
|---|
| 21 | (\"reflecting\") problems in a more concrete form, hence the name. For \ |
|---|
| 22 | example, in the Ssreflect library, arithmetic comparison is not an \ |
|---|
| 23 | abstract predicate, but a function computing a boolean. \ |
|---|
| 24 | For more information, <$homepage}>. |
|---|
| 25 | |
|---|
| 26 | checksums md5 b26d0af1fb0f4f628465cde89fd705de \ |
|---|
| 27 | sha1 b904ac2f86f04bcb8530137fb06c48058b8407de \ |
|---|
| 28 | rmd160 a61b156f2a507f264237a5fa57c83ac8b1350737 |
|---|
| 29 | |
|---|
| 30 | use_parallel_build yes |
|---|
| 31 | depends_lib bin:ocamlc:ocaml port:coq |
|---|
| 32 | |
|---|
| 33 | livecheck.type regex |
|---|
| 34 | livecheck.url ${homepage} |
|---|
| 35 | livecheck.regex "<a href=\"ssreflect-(\\d+(?:\\.\\d+)*).tgz\">Download</a> the sources." |
|---|
| 36 | |
|---|
| 37 | configure.cmd coq_makefile |
|---|
| 38 | configure.pre_args {} |
|---|
| 39 | configure.args -f Make -o Makefile |
|---|
| 40 | |
|---|
| 41 | build.target all |
|---|
| 42 | |
|---|
| 43 | destroot.target install |
|---|
| 44 | destroot.destdir COQLIB='${destroot}${prefix}/lib/coq' |
|---|
| 45 | post-destroot { |
|---|
| 46 | xinstall ${worksrcpath}/bin/ssrcoq ${destroot}${prefix}/bin/ssrcoq |
|---|
| 47 | xinstall -d ${destroot}${prefix}/share/emacs/site-lisp |
|---|
| 48 | xinstall ${worksrcpath}/pg-ssr.el ${destroot}${prefix}/share/emacs/site-lisp/pg-ssr.el |
|---|
| 49 | } |
|---|
| 50 | |
|---|
| 51 | post-activate { ui_msg "The extension of ProofGeneral, pg-ssr.el, is" |
|---|
| 52 | ui_msg "in ${prefix}/share/emacs/site-lisp." |
|---|
| 53 | ui_msg "Add (load-file \"${prefix}/share/emacs/site-lisp/pg-ssr.el\") line" |
|---|
| 54 | ui_msg "immediately after the line" |
|---|
| 55 | ui_msg "(load-file \"<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el\")" |
|---|
| 56 | ui_msg "to your .emacs if you wish to use it." |
|---|
| 57 | } |
|---|
