# -*- 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 PortGroup cmake 1.1 # Until a new release is published under the 3-clause BSD license, we have to # track the development branch; as of this writing, the last stable # release (4.5.1) was made under the previous, restricted-use license. name vampire github.setup vprover vampire 1f1a9d99e4f6ca018dc3e9af05c49fb1d337a9bd version 2021-08-04 categories math science platforms darwin freebsd maintainers {landonf @landonf} openmaintainer description Vampire Theorem Prover long_description High performance automated theorem prover. checksums rmd160 7677185d5ee171a84f52bf84e9047244d899910d \ sha256 050eb27fb173f5e5c53b1e02aa5942002168e24e40b1964f242cee25c8a623be \ size 1497942 # 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 configure.args -DIPO=ON # Don't overide 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} { 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 environmental variable before executing vampire. " } destroot { xinstall -d -m 755 "${destroot}${cmake.install_prefix}/bin" xinstall -m 755 "${cmake.build_dir}/bin/vampire" "${destroot}${cmake.install_prefix}/bin/vampire" }