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

github.setup        rocq-prover rocq 9.2.0 V
github.tarball_from releases
revision            2
categories          lang math
license             LGPL-2.1
maintainers         {pmetzger @pmetzger} openmaintainer

description         Proof assistant for higher-order logic
long_description    Rocq (formerly coq) is a proof assistant for higher-order logic, \
                    which allows the development of computer programs \
                    consistent with their formal specification. It is \
                    developed using OCaml and Dune.
homepage            https://rocq-prover.org/

checksums           rmd160  482d4d2f50d189886cea9284c95f4a65c4382e47 \
                    sha256  a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20 \
                    size    6559931

depends_build-append \
                    port:ocaml-dune \
                    port:ocaml-findlib

depends_lib-append  port:ocaml \
                    port:ocaml-zarith

depends_test-append port:ocaml-zip

configure.pre_args  -prefix ${prefix}

use_parallel_build  no

test.run            yes
test.target         test-suite

build {
    system -W ${worksrcpath} "/usr/bin/make dunestrap"
    system -W ${worksrcpath} "${prefix}/bin/dune build -p rocq-runtime,coq-core,rocq-core"
}

destroot {
    system -W ${worksrcpath} "${prefix}/bin/dune install --prefix=${prefix} --destdir=${destroot} rocq-runtime coq-core rocq-core"
}

# ocaml is not universal
universal_variant   no

notes "
The style file for LaTeX documentation,\
coqdoc.sty, is in ${prefix}/share/coq/latex.\
Add this to your TEXINPUTS if you wish to\
use it.
"

subport coq {
    PortGroup       obsolete 1.0

    replaced_by     rocq
    version         8.13.2
    revision        1
}
