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

github.setup        vprover vampire 4.9 v casc2024
revision            0
epoch               1
categories          math science
platforms           darwin freebsd
maintainers         {landonf @landonf} openmaintainer
description         Vampire Theorem Prover
long_description    High performance automated theorem prover.

checksums           rmd160  e62573a009237c43c550837ad5f34476fbdaa235 \
                    sha256  7d0101dc296d0f6fb4f3326febf6a3f3bfd3400b36249a91794789c68a855f3d \
                    size    1502934

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

github.tarball_from archive

patchfiles          patch-CMakeLists.txt.diff

# https://github.com/vprover/vampire/pull/593
patchfiles-append   0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch

cmake.build_type    Release
cmake.generator     Ninja

compiler.cxx_standard \
                    2017

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))"
}