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

# Temporarily remains commit-based until the next release
# due to important fixes being added by the upstream recently.
github.setup        vprover vampire 1b080631257a403681d1287f87f8d3ac1ee97c63
version             2024-05-31
categories          math science
platforms           darwin freebsd
maintainers         {landonf @landonf} openmaintainer
description         Vampire Theorem Prover
long_description    High performance automated theorem prover.

checksums           rmd160  e09d316e9fda2479726491f197d8b4edbf5e2e2f \
                    sha256  f0f1ee2bbd10b82e0373a53357572f5f3801568e5c67aaba2fdc5209b8091a34 \
                    size    1466583

# Vampire is BSD-licensed, embedded minisat is MIT-licensed
license             BSD MIT

github.tarball_from archive

patchfiles          patch-CMakeLists.txt.diff

cmake.build_type    Release
cmake.generator     Ninja

compiler.cxx_standard \
                    2014

configure.args-append \
                    -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON

# FIXME: https://github.com/vprover/vampire/issues/512
if {${os.platform} eq "darwin" && ${os.major} > 10} {
    configure.args-append \
                    -DIPO=ON
}

# Don't override vampire's default optimization flags
configure.optflags

variant debug description {Enable the debug build configuration} {
    cmake.build_type    Debug

    test.run            yes
}

variant native description {Generate code optimized for this machine's CPU. The resulting binaries may not run on other processors} {
    if {${configure.build_arch} in [list ppc ppc64]} {
        configure.optflags-append   -mtune=native
    } else {
        configure.optflags-append   -march=native
    }
}

variant polly description {Perform loop and data-locality optimization using LLVM's Polly optimizer} {
    # We need llvm built with polly support; this available by default as of our llvm-12 port,
    # so make that our minimum version.
    compiler.blacklist-append   {cc} \
                                {clang} \
                                {macports-clang-[0-9].*} \
                                {macports-clang-10} \
                                {macports-clang-11} \
                                {*gcc*}

    configure.optflags-append   -O3 -mllvm -polly
}

variant profile description {Generate instrumented code that may be used for profile-guided optimization} {
    # Default to /dev/null, requiring that users explicitly set LLVM_PROFILE_FILE.
    # See also: https://clang.llvm.org/docs/UsersManual.html#profiling-with-instrumentation
    configure.optflags-append   -fprofile-instr-generate=/dev/null

    # Require clang
    compiler.blacklist-append   {*gcc*} cc

    notes-append "
    ${name} has been built with profiling instrumentation enabled; note\
    that this will introduce non-negligible runtime overhead.

    To generate profile data, specify an output path by setting\
    the LLVM_PROFILE_FILE environment variable before executing vampire.
    "
}

variant z3 description {Use Z3} {
    depends_lib-append \
                    port:z3

    configure.args-delete \
                    -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON
}

destroot {
    xinstall -d -m 755 "${destroot}${cmake.install_prefix}/bin"
    xinstall -m 755 "${cmake.build_dir}/bin/vampire" "${destroot}${cmake.install_prefix}/bin/vampire" 
}

pre-test {
    # test infrastructure uses /bin/ps, which is forbidden by sandboxing
    append portsandbox_profile " (allow process-exec (literal \"/bin/ps\") (with no-profile))"
}