mirror of
https://github.com/macports/macports-ports.git
synced 2026-07-12 18:20:25 -07:00
493 lines
18 KiB
Tcl
493 lines
18 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 github 1.0
|
|
PortGroup cmake 1.1
|
|
PortGroup legacysupport 1.1
|
|
|
|
name z3
|
|
categories math science
|
|
maintainers {landonf @landonf} openmaintainer
|
|
description Z3 Theorem Prover
|
|
long_description High performance SMT solver from Microsoft Research.
|
|
|
|
# If set, a pgo variant will be defined for this subport using profiling data
|
|
# extracted from ${filespath}/${z3.pgo_profile}.profdata.tar.xz
|
|
options z3.pgo_profile
|
|
|
|
if {${subport} eq "${name}-fstar"} {
|
|
# Current F*-qualified z3 release
|
|
github.setup Z3Prover z3 4.13.3 z3-
|
|
revision 0
|
|
checksums rmd160 89b77de5ad59d633efe90151119540620840baf3 \
|
|
sha256 f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0 \
|
|
size 5583533
|
|
z3.pgo_profile ${subport}
|
|
|
|
# Also install the legacy F*-qualified z3 release
|
|
depends_run-append port:z3-fstar-legacy
|
|
} elseif {${subport} eq "${name}-fstar-legacy"} {
|
|
# Legacy F*-qualified z3 release
|
|
github.setup Z3Prover z3 4.8.5 Z3-
|
|
revision 7
|
|
checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
|
|
sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
|
|
size 4177051
|
|
|
|
z3.pgo_profile ${subport}
|
|
|
|
patchfiles z3-clang-19-4.8.5.diff
|
|
} else {
|
|
# Current z3 release
|
|
github.setup Z3Prover z3 4.15.4 z3-
|
|
revision 0
|
|
checksums rmd160 688013a7b6fbcfb5a18d35810ade289bc88a2ec3 \
|
|
sha256 dae526252cb0585c8c863292ebec84cace4901a014b190a73f14087dd08d252b \
|
|
size 6060031
|
|
}
|
|
|
|
platforms darwin freebsd
|
|
license MIT
|
|
|
|
github.tarball_from archive
|
|
|
|
if {[vercmp ${version} "4.8.9"] >= 0} {
|
|
patchfiles-append libz3-static.diff
|
|
} else {
|
|
patchfiles-append libz3-static-4.8.5.diff
|
|
}
|
|
|
|
worksrcdir ${name}-${github.tag_prefix}${version}
|
|
|
|
cmake.build_type Release
|
|
cmake.generator Ninja
|
|
|
|
# Build requires -std=gnu++20
|
|
compiler.cxx_standard 2020
|
|
|
|
# Don't overide z3's default optimization flags
|
|
configure.optflags
|
|
|
|
destroot.target install
|
|
|
|
# +polly requires a supported compiler (>= macports-clang-12).
|
|
#
|
|
# Note that the +polly variant does blacklist unsupported compilers, but if
|
|
# this results in all compilers being blacklisted (as is the case on 10.6, where
|
|
# macports-clang-12 is not available), a non-polly-enabled compiler fallback
|
|
# will be selected, and the build will break.
|
|
proc z3.polly_supported_compiler {compiler} {
|
|
if {![regexp {macports-clang-(.*)} ${compiler} -> llvm_ver]} {
|
|
return 0
|
|
}
|
|
|
|
if {[vercmp ${llvm_ver} "12"] >= 0} {
|
|
return 1
|
|
}
|
|
|
|
return 0
|
|
}
|
|
|
|
proc z3.polly_compiler_available {} {
|
|
global compiler.fallback
|
|
|
|
foreach compiler ${compiler.fallback} {
|
|
if {[z3.polly_supported_compiler ${compiler}]} {
|
|
return 1
|
|
}
|
|
}
|
|
|
|
return 0
|
|
}
|
|
|
|
# Common variants
|
|
variant debug description {Enable the debug build configuration} {
|
|
cmake.build_type Debug
|
|
}
|
|
|
|
# Options not shared with our language-binding subports
|
|
if {
|
|
${subport} eq "${name}" ||
|
|
${subport} eq "${name}-fstar" ||
|
|
${subport} eq "${name}-fstar-legacy"
|
|
} {
|
|
|
|
set py_ver 3.13
|
|
set py_ver_nodot [string map {. {}} ${py_ver}]
|
|
|
|
depends_build-append port:python${py_ver_nodot} \
|
|
port:bash
|
|
|
|
patchfiles-append build-z3-qprofdiff.diff
|
|
|
|
# z3 4.8.11 and later use std::variant<>, which is broken on macOS <= 10.12;
|
|
# use macports' libc++ instead
|
|
if {[vercmp ${version} "4.8.11"] >= 0 && ${os.platform} eq "darwin" && ${os.major} <= 16} {
|
|
legacysupport.use_mp_libcxx yes
|
|
}
|
|
|
|
configure.args-append -DPYTHON_EXECUTABLE=${prefix}/bin/python${py_ver}
|
|
|
|
if {[vercmp ${version} "4.8.7"] >= 0} {
|
|
configure.args-append -DZ3_ENABLE_EXAMPLE_TARGETS=ON
|
|
} else {
|
|
configure.args-append -DENABLE_EXAMPLE_TARGETS=ON
|
|
}
|
|
|
|
if {[vercmp ${version} "4.8.7"] >= 0} {
|
|
configure.args-append -DZ3_SINGLE_THREADED=ON
|
|
} elseif {[vercmp ${version} "4.8.6"] >= 0} {
|
|
configure.args-append -DSINGLE_THREADED=ON
|
|
} else {
|
|
configure.args-append -DUSE_OPENMP=OFF
|
|
}
|
|
|
|
# Optimal (hopefully) default variants selected based on benchmark results.
|
|
# Benchmark configurations:
|
|
#
|
|
# darwin {
|
|
# ver {4.8.5}
|
|
# cc {macports-clang-8.0}
|
|
# cpu {Intel Core i7-7700K @ 4.20GHz (4 cores/8 threads)}
|
|
# os {macOS 10.14.6 (18G95)}
|
|
# }
|
|
# freebsd {
|
|
# ver {4.8.5}
|
|
# cc {macports-clang-8.0}
|
|
# cpu {Dual Intel Xeon E5-2680 v4 @ 2.40GHz (2 x 14 cores/28 threads)}
|
|
# os {FreeBSD 12.0-RELEASE-p9}
|
|
# }
|
|
#
|
|
|
|
# +polly requires a supported compiler (>= macports-clang-12).
|
|
if {[z3.polly_compiler_available]} {
|
|
default_variants-append +polly +polly_late +polly_vector
|
|
}
|
|
|
|
# Unsupported prior to 4.8.6
|
|
if {[vercmp ${version} "4.8.6"] >= 0} {
|
|
default_variants-append +threads
|
|
}
|
|
|
|
# LTO is broken on <= macOS 10.6:
|
|
# 'unknown scope for symbol ... in bitcode file'
|
|
if {(${os.platform} ne "darwin" || ${os.major} > 10) && ![variant_isset debug]} {
|
|
default_variants-append +lto
|
|
}
|
|
|
|
if {[info exists z3.pgo_profile]} {
|
|
if {![variant_isset profile]} {
|
|
default_variants-append +pgo
|
|
}
|
|
|
|
variant pgo conflicts profile description {Enable profile-guided optimization} {
|
|
# Requires clang
|
|
compiler.blacklist-append {*gcc*} cc
|
|
|
|
# We currently only provide profiling data for the F*-qualified z3
|
|
# subports; these profiles are generated from a verification run
|
|
# over Project Everest subprojects, which should be strongly
|
|
# representative of F*'s use of z3.
|
|
#
|
|
# TODO: Investigate bechmark suites we could use to produce general-purpose
|
|
# profiling data for the main z3 port.
|
|
#
|
|
# To regenerate a subport's profiling data, install
|
|
# z3-fstar(-legacy) with +profile -pgo, and then:
|
|
#
|
|
# ${filespath}/z3-fstar.profdata-generate.sh \
|
|
# -l llvm-profdata-mp-<llvm-version> \
|
|
# -z ${prefix}/libexec/z3-fstar/bin/z3-<version> \
|
|
# -o ${filespath}/${z3.pgo_profile}.profdata.tar.xz \
|
|
# -j <njobs> \
|
|
# <everest-src>
|
|
configure.optflags-append -fprofile-instr-use=${workpath}/z3.profdata
|
|
depends_extract-append bin:xz:xz
|
|
post-extract {
|
|
set tar [findBinary tar ${portutil::autoconf::tar_command}]
|
|
set xz [findBinary xz ${portutil::autoconf::xz_path}]
|
|
system "${xz} -cd ${filespath}/${z3.pgo_profile}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -"
|
|
}
|
|
}
|
|
}
|
|
|
|
variant lto conflicts debug description {Enable link-time (interprocedural) optimization} {
|
|
configure.args-append -DCMAKE_INTERPROCEDURAL_OPTIMIZATION=ON \
|
|
-DCMAKE_POLICY_DEFAULT_CMP0069=NEW
|
|
|
|
# Require clang (LTO may work with GCC, but is untested)
|
|
compiler.blacklist-append {*gcc*} cc
|
|
|
|
# I don't believe -flto was supported by clang until Xcode 9
|
|
platform darwin {
|
|
compiler.blacklist-append {clang < 900}
|
|
}
|
|
|
|
# TODO: Is this still required in 13.x+?
|
|
platform freebsd {
|
|
compiler.blacklist-append clang
|
|
}
|
|
}
|
|
|
|
variant gmp description {Use GNU GMP library for arbitrary precision arithmetic} {
|
|
depends_lib-append port:gmp
|
|
if {[vercmp ${version} "4.8.7"] >= 0} {
|
|
configure.args-append -DZ3_USE_LIB_GMP=ON
|
|
} else {
|
|
configure.args-append -DUSE_LIB_GMP=ON
|
|
}
|
|
}
|
|
|
|
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 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 z3.
|
|
"
|
|
}
|
|
|
|
if {[vercmp ${version} "4.8.6"] >= 0} {
|
|
variant threads description {Enable thread-safe build} {
|
|
if {[vercmp ${version} "4.8.7"] >= 0} {
|
|
configure.args-delete -DZ3_SINGLE_THREADED=ON
|
|
configure.args-append -DZ3_SINGLE_THREADED=OFF
|
|
} else {
|
|
configure.args-delete -DSINGLE_THREADED=ON
|
|
configure.args-append -DSINGLE_THREADED=OFF
|
|
}
|
|
}
|
|
}
|
|
|
|
variant polly conflicts debug 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 polly_late requires polly description {Perform LLVM Polly optimization later in the LLVM optimization pass pipline} {
|
|
# See https://polly.llvm.org/docs/Architecture.html#polly-in-the-llvm-pass-pipeline
|
|
configure.optflags-append -mllvm -polly-position=before-vectorizer
|
|
}
|
|
|
|
variant polly_two_level_tiling requires polly description {Enable second-level loop tiling using LLVM's Polly optimizer} {
|
|
configure.optflags-append -mllvm -polly-2nd-level-tiling
|
|
}
|
|
|
|
variant polly_vector requires polly description {Enable automatic vector code generation using LLVM's Polly optimizer} {
|
|
configure.optflags-append -mllvm -polly-vectorizer=stripmine
|
|
}
|
|
|
|
variant polly_parallel requires polly description {Enable automatic generation of OpenMP code for parallel loops using LLVM's Polly optimizer} {
|
|
configure.optflags-append -mllvm -polly-parallel
|
|
|
|
# Generated OpenMP code requires libomp/libgomp
|
|
# LLVM uses libomp
|
|
depends_lib-append port:libomp
|
|
configure.ldflags-append -L${prefix}/lib/libomp \
|
|
-lomp
|
|
}
|
|
|
|
pre-configure {
|
|
# Verify that a polly-supporting compiler was actually selected
|
|
if {[variant_isset polly] && ![z3.polly_supported_compiler ${configure.compiler}]} {
|
|
ui_error "${name} @${version}: +polly requires macports-clang-12 or later"
|
|
return -code error "incompatible compiler selected"
|
|
}
|
|
|
|
#
|
|
# If we enable +lto in combination with a variant (e.g. +polly) that
|
|
# selects MacPorts' clang compiler, CMake fails to locate the llvm-ar and llvm-ranlib
|
|
# binaries required for -flto.
|
|
#
|
|
# TODO: Investigate fixing this in upstream cmake, and/or in the cmake PortGroup
|
|
#
|
|
if {[variant_isset lto] && [regexp {macports-clang-(.*)} ${configure.compiler} -> llvm_ver]} {
|
|
foreach lang {C CXX} {
|
|
foreach tool {ar ranlib} {
|
|
set var CMAKE_${lang}_COMPILER_[string toupper ${tool}]
|
|
set path ${prefix}/bin/llvm-${tool}-mp-${llvm_ver}
|
|
configure.args-append -D${var}=${path}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
test.run yes
|
|
test.target test-z3
|
|
post-test {
|
|
# This actually executes the unit tests
|
|
system -W ${test.dir} {./test-z3 /a}
|
|
}
|
|
}
|
|
|
|
# F*-qualified z3 release; may trail behind the current z3 release.
|
|
subport ${name}-fstar {
|
|
description F*-qualified release of the Z3 Theorem Prover
|
|
long_description Private version of the Z3 Theorem Prover for use by (and qualified to work with) F*.
|
|
|
|
notes-append "
|
|
Add the following directory to your PATH environment variable to
|
|
permit F* to automatically discover the installed F*-qualified z3
|
|
binaries:
|
|
${prefix}/libexec/z3-fstar/bin
|
|
"
|
|
}
|
|
|
|
subport ${name}-fstar-legacy {
|
|
description Legacy F*-qualified release of the Z3 Theorem Prover
|
|
long_description Private version of the Z3 Theorem Prover for use by (and qualified to work with) F* (legacy version).
|
|
}
|
|
|
|
if {${subport} eq "${name}-fstar" || ${subport} eq "${name}-fstar-legacy"} {
|
|
cmake.install_prefix ${prefix}/libexec/z3-fstar/${version}
|
|
|
|
if {[vercmp ${version} "4.8.5"] <= 0} {
|
|
depends_build-append port:py${py_ver_nodot}-setuptools
|
|
}
|
|
|
|
destroot {
|
|
xinstall -d -m 755 \
|
|
"${destroot}${prefix}/libexec/z3-fstar/bin" \
|
|
"${destroot}${cmake.install_prefix}/bin"
|
|
|
|
xinstall -m 755 "${cmake.build_dir}/z3" \
|
|
"${destroot}${cmake.install_prefix}/bin/z3"
|
|
|
|
ln -sf "${cmake.install_prefix}/bin/z3" \
|
|
"${destroot}${prefix}/libexec/z3-fstar/bin/z3-${version}"
|
|
|
|
# Unversioned symlink for compatibility with the previous port layout;
|
|
# may be removed (or switched to non-legacy z3-fstar?) once F* adopts
|
|
# adopts it as the default z3 version.
|
|
if {${subport} eq "${name}-fstar-legacy"} {
|
|
ln -sf "${cmake.install_prefix}/bin/z3" \
|
|
"${destroot}${prefix}/bin/z3-fstar"
|
|
}
|
|
}
|
|
}
|
|
|
|
set pyversions {310 311 312 313 314}
|
|
|
|
# Create a top-level Python binding metaport
|
|
subport py-${name} {
|
|
PortGroup python 1.0
|
|
PortGroup stub 1.0
|
|
|
|
supported_archs noarch
|
|
platforms any
|
|
categories-append python
|
|
|
|
description Python bindings for the Z3 theorem prover
|
|
long_description Python bindings for the Z3 SMT solver library from Microsoft Research.
|
|
|
|
python.default_version [lindex ${pyversions} end]
|
|
depends_lib port:${name} \
|
|
port:py${python.version}-${name}
|
|
|
|
# Feb 2023 - master base/github PG default to yes which errors
|
|
if {[exists extract.rename]} {
|
|
extract.rename no
|
|
}
|
|
}
|
|
|
|
# Create Python subports for each supported Python version
|
|
foreach v ${pyversions} {
|
|
subport py${v}-${name} {
|
|
PortGroup python 1.0
|
|
|
|
python.version ${v}
|
|
|
|
supported_archs noarch
|
|
platforms {darwin any}
|
|
categories-append python
|
|
|
|
description Python ${python.branch} bindings for the Z3 theorem prover
|
|
long_description Python ${python.branch} bindings for the Z3 SMT solver library from Microsoft Research.
|
|
|
|
# needs pkg_resources at runtime
|
|
depends_lib-append port:${name} \
|
|
port:python${v} \
|
|
port:py${v}-setuptools
|
|
|
|
use_configure yes
|
|
configure.args-append -DPython3_EXECUTABLE=${python.bin} \
|
|
-DZ3_BUILD_PYTHON_BINDINGS=ON \
|
|
-DZ3_INSTALL_PYTHON_BINDINGS=ON
|
|
|
|
# Avoid rebuilding libz3
|
|
post-patch {
|
|
reinplace -E {s|^[[:blank:]]*DEPENDS[[:blank:]]+libz3|DEPENDS |g} \
|
|
src/api/python/CMakeLists.txt
|
|
}
|
|
|
|
post-destroot {
|
|
# The python module looks for libz3 in its package path
|
|
ln -sf "${prefix}/lib/libz3.dylib" "${destroot}${python.pkgd}/z3/"
|
|
}
|
|
|
|
build.target src/api/python/all
|
|
destroot.cmd ${build.cmd}
|
|
destroot.target src/api/python/install
|
|
}
|
|
}
|
|
|
|
# Java bindings
|
|
subport ${name}-java {
|
|
PortGroup java 1.0
|
|
|
|
java.version 1.8+
|
|
java.fallback openjdk11
|
|
|
|
categories-append java
|
|
|
|
description Java bindings for the Z3 theorem prover
|
|
long_description Java bindings for the Z3 SMT solver library from Microsoft Research.
|
|
|
|
depends_lib-append port:${name}
|
|
|
|
patchfiles-append java_libpath.diff
|
|
|
|
configure.args-append -DZ3_BUILD_JAVA_BINDINGS=ON \
|
|
-DZ3_INSTALL_JAVA_BINDINGS=ON \
|
|
-DZ3_JAVA_JNI_LIB_INSTALLDIR=${prefix}/lib/${name} \
|
|
-DZ3_JAVA_JAR_INSTALLDIR=${prefix}/share/java/${name}
|
|
|
|
post-patch {
|
|
# Avoid rebuilding libz3
|
|
reinplace -E {s|(^[[:blank:]]*target_link_libraries[[:blank:]]*\([[:blank:]]*z3java[[:blank:]]*PRIVATE)[[:blank:]]*libz3(.*)|\1 z3 \2|g} \
|
|
src/api/java/CMakeLists.txt
|
|
|
|
# Fix up path to our JNI library
|
|
reinplace "s|@PREFIX@|${prefix}|g" \
|
|
scripts/update_api.py
|
|
}
|
|
|
|
post-destroot {
|
|
ln -s "com.microsoft.z3.jar" "${destroot}${prefix}/share/java/${name}/z3.jar"
|
|
}
|
|
|
|
build.target src/api/java/all
|
|
destroot.cmd ${build.cmd}
|
|
destroot.target src/api/java/install
|
|
}
|