# $Id$

PortSystem        1.0
name              isabelle
version           2007
revision          1
categories        math lang ml
maintainers       mww
description       Isabelle is a popular generic theorem proving environment.
long_description  Isabelle is a generic proof assistant. It allows mathematical \
                  formulas to be expressed in a formal language and provides \
                  tools for proving those formulas in a logical calculus. The \
                  main application is the formalization of mathematical proofs \
                  and in particular formal verification, which includes proving \
                  the correctness of computer hardware or software and proving \
                  properties of computer languages and protocols.

homepage          http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
master_sites      http://isabelle.in.tum.de/dist/ \
                  http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/ \
                  http://mirror.cse.unsw.edu.au/pub/isabelle/dist/

distname          Isabelle${version}
checksums         md5 088e56b79a4c8cd3e4de7dad62a35827 \
                  sha1 dd1312a1af296cb02754069691801a23e03c7e15
patchfiles        patch-etc-settings

depends_lib       port:polyml

post-extract {
    file rename ${worksrcpath}/doc ${workpath}/doc
    system "cd ${worksrcpath} && mv ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README ${workpath}/doc"
}

configure {
    reinplace "s|@prefix@|${prefix}|g" ${worksrcpath}/etc/settings
}

build {
    system "cd ${workpath}/${worksrcdir} && ./build -a -b"
}

destroot {
    file copy ${worksrcpath} ${destroot}${prefix}/lib/${name}
    system "${destroot}${prefix}/lib/${name}/bin/isatool install -p ${destroot}${prefix}/bin -d ${prefix}/lib/${name}"
    xinstall -d ${destroot}${prefix}/share/doc/
    file copy ${workpath}/doc ${destroot}${prefix}/share/doc/${name}-${version}
}

livecheck.check regex
livecheck.url   http://www.cl.cam.ac.uk/research/hvg/Isabelle/download.html
livecheck.regex Isabelle(\[0-9\]+).tar.gz