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

# 9.2.0 release fails to build with up-to-date OCaml toolchain.
# 2026.08.03
github.setup        rocq-prover rocq 6df5ae331262750d9fc2d115dd2198a6373e4dd0
version             9.2.0
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  7dcbf005521ffa9ddee8b118c3d232f3e624a03e \
                    sha256  f542b264ea8c2f17b025a669dc64205881a4756d2d6162794b589839343799b4 \
                    size    6722491
github.tarball_from archive

post-patch {
    # Replace gnuism with proper POSIX:
    reinplace "s|cp -a |cp -pRP |g" ${worksrcpath}/Makefile
}

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

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

configure.env-append \
                    DUNE_CONFIG__COPY_FILE=portable

configure.pre_args  -prefix ${prefix}

use_parallel_build  no

# https://github.com/rocq-prover/rocq/issues/22337
build {
    system -W ${worksrcpath} "DUNE_CONFIG__COPY_FILE=portable CPATH=${prefix}/include LIBRARY_PATH=${prefix}/lib /usr/bin/make dunestrap"
    system -W ${worksrcpath} "DUNE_CONFIG__COPY_FILE=portable CPATH=${prefix}/include LIBRARY_PATH=${prefix}/lib ${prefix}/bin/dune build -p rocq-runtime,coq-core,rocq-core"
}

destroot {
    system -W ${worksrcpath} "DUNE_CONFIG__COPY_FILE=portable ${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
}
