| 1 | # $Id: Portfile,v 1.2 2004/12/01 17:01:53 gwright Exp $ |
|---|
| 2 | |
|---|
| 3 | PortSystem 1.0 |
|---|
| 4 | name isabelle |
|---|
| 5 | version 2004 |
|---|
| 6 | revision 1 |
|---|
| 7 | categories lang |
|---|
| 8 | maintainers dem5302@cs.rit.edu |
|---|
| 9 | description Isabelle is a popular generic theorem proving environment. |
|---|
| 10 | long_description Isabelle is a generic proof assistant. It allows mathematical \ |
|---|
| 11 | formulas to be expressed in a formal language and provides \ |
|---|
| 12 | tools for proving those formulas in a logical calculus. The \ |
|---|
| 13 | main application is the formalization of mathematical proofs \ |
|---|
| 14 | and in particular formal verification, which includes proving \ |
|---|
| 15 | the correctness of computer hardware or software and proving \ |
|---|
| 16 | properties of computer languages and protocols. |
|---|
| 17 | |
|---|
| 18 | homepage http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
|---|
| 19 | master_sites ${homepage}/dist/ |
|---|
| 20 | |
|---|
| 21 | distfiles Isabelle${version}${extract.suffix} |
|---|
| 22 | checksums md5 8ea6985fde973453090abaa68aaa8446 |
|---|
| 23 | worksrcdir Isabelle2004 |
|---|
| 24 | |
|---|
| 25 | depends_lib bin:poly:polyml \ |
|---|
| 26 | lib:poly/ML_dbase:polyml |
|---|
| 27 | |
|---|
| 28 | # The goal is to make polyml+isabelle "just work" out of the box. If |
|---|
| 29 | # a user wishes to use other implementations of ML, then they will |
|---|
| 30 | # have to edit the settings file directly. |
|---|
| 31 | # |
|---|
| 32 | # The settings file is limited to very few scenarios out of the box. |
|---|
| 33 | # We modify the linux entry, since it is the closest thing that will |
|---|
| 34 | # resemble our darwinports installation. |
|---|
| 35 | |
|---|
| 36 | post-configure { |
|---|
| 37 | reinplace "s|/.*/bin/poly|${prefix}/bin/poly|g" ${workpath}/${worksrcdir}/etc/settings |
|---|
| 38 | reinplace "s|/usr/lib/poly|${prefix}/lib/poly|g" ${workpath}/${worksrcdir}/etc/settings |
|---|
| 39 | reinplace "s|ML_PLATFORM=x86-linux|ML_PLATFORM=ppc-darwin|g" ${workpath}/${worksrcdir}/etc/settings |
|---|
| 40 | reinplace "s|ML_HOME=/usr/bin|ML_HOME=${prefix}/bin|g" ${workpath}/${worksrcdir}/etc/settings |
|---|
| 41 | } |
|---|
| 42 | |
|---|
| 43 | build { |
|---|
| 44 | cd ${workpath}/${worksrcdir} |
|---|
| 45 | system "./build -a" |
|---|
| 46 | } |
|---|
| 47 | |
|---|
| 48 | destroot { |
|---|
| 49 | file copy ${workpath}/${worksrcdir} ${destroot}${prefix}/Isabelle2004 |
|---|
| 50 | system "${destroot}${prefix}/Isabelle2004/bin/isatool install -p ${destroot}${prefix}/bin" |
|---|
| 51 | reinplace "s|\"/.*/bin|\"${prefix}/Isabelle2004/bin|g" \ |
|---|
| 52 | ${destroot}${prefix}/bin/isabelle-process \ |
|---|
| 53 | ${destroot}${prefix}/bin/isabelle-interface \ |
|---|
| 54 | ${destroot}${prefix}/bin/isatool |
|---|
| 55 | } |
|---|
