mirror of
https://github.com/macports/macports-ports.git
synced 2026-07-12 18:20:25 -07:00
109 lines
3.7 KiB
Tcl
109 lines
3.7 KiB
Tcl
# -*- 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))"
|
|
}
|