# -*- 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

PortSystem          1.0
PortGroup           ocaml 1.1

name                abella
version             2.0.7
revision            0
categories          math ocaml
maintainers         {@barracuda156 gmail.com:vital.had} openmaintainer
license             GPL-3
description         Interactive theorem prover
long_description    Abella is an interactive theorem prover based on lambda-tree syntax. \
                    This means that Abella is well-suited for reasoning about the meta-theory \
                    of programming languages and other logical systems which manipulate objects with binding.
homepage            https://abella-prover.org
master_sites        https://abella-prover.org/distributions

checksums           rmd160  f6ea41a4def908c9ec9c44d8ad207d756fc5f8f2 \
                    sha256  fde3a279b3051e0aeeaedad21cf96064edf19a6c413949b2033b305d92dddd87 \
                    size    215056

depends_build-append \
                    port:gmake \
                    port:ocaml-findlib \
                    port:ocaml-ocamlbuild

patchfiles          patch-bytecode.diff

post-patch {
    reinplace "s|4-29-40-41-42-44-45-48-58-59-60|4-29-40-41-42-44-45-48-58-59-60-70|" \
                    ${worksrcpath}/myocamlbuild.ml
}

use_configure       no

if {${build_arch} in [list ppc ppc64]} {
    build.target    byte
    test.target     test_byte
} else {
    build.target    all
    test.target     test
}

destroot {
    xinstall -m 755 -d ${destroot}${prefix}/bin
    file copy ${worksrcpath}/${name} ${destroot}${prefix}/bin/${name}
}

test.run            yes
test.cmd            ${build.cmd}