# -*- 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 compiler_blacklist_versions 1.0 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. # FStar-qualified Z3 release? if {${subport} eq "${name}-fstar"} { github.setup Z3Prover z3 4.8.5 Z3- revision 5 checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \ sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \ size 4177051 } else { github.setup Z3Prover z3 4.12.6 z3- revision 0 checksums rmd160 ea2d648b1e178130ef8bf11cc416d618584e32f6 \ sha256 9e46a1260ea26c441a1ad6faf378bf911ee9ffd110868867b4b2f2e3c7d2200e \ size 5492517 github.tarball_from archive } 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++17 compiler.cxx_standard 2017 # 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"} { set py_ver 3.12 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 } # TODO: We currently only have profiling data for z3-fstar; we should # investigate bechmark suites we could use to produce general-purpose # profiling data for the main z3 port. if {${subport} eq "${name}-fstar" && ![variant_isset profile]} { default_variants-append +pgo } 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 environmental 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 depends_lib-append port:libomp configure.ldflags-append -L${prefix}/lib/libomp \ -lgomp } 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 { # Should be updated 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*. cmake.install_prefix ${prefix}/libexec/${subport} destroot { xinstall -d -m 755 "${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}/bin/z3-fstar" } variant pgo conflicts profile description {Enable profile-guided optimization} { # Requires clang compiler.blacklist-append {*gcc*} # We currently only provide profiling data for z3-fstar; this profile is # generated from a verification run over Project Everest subprojects, which # should be strongly representative of F*'s use of z3. # # To regenerate the profile, install z3-fstar with +profile -pgo, and then: # ${filespath}/z3-fstar.profdata-generate.sh \ # -l llvm-profdata-mp- \ # -z ${prefix}/bin/z3-fstar \ # -o ${filespath}/z3-fstar.profdata.tar.xz \ # -j \ # configure.optflags-append -fprofile-instr-use=${workpath}/${subport}.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}/${subport}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -" } } } set pyversions {38 39 310 311 312} # 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 }