<pre style='margin:0'>
Landon Fuller (landonf) pushed a commit to branch master
in repository macports-ports.
</pre>
<p><a href="https://github.com/macports/macports-ports/commit/a322a7502bcd8103a2a824ff475637a597789428">https://github.com/macports/macports-ports/commit/a322a7502bcd8103a2a824ff475637a597789428</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit a322a7502bcd8103a2a824ff475637a597789428
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Fri Jul 23 15:49:23 2021 -0600
<span style='display:block; white-space:pre;color:#404040;'> z3: adopt llvm-12, which provides polly support by default, update profiling data, and add +polly(_late|_vector) to our default_variants.
</span>---
math/z3/Portfile | 31 +++++++++++--------------------
math/z3/files/z3-fstar.profdata.tar.xz | Bin 1892084 -> 1887024 bytes
2 files changed, 11 insertions(+), 20 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/Portfile b/math/z3/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index b84bee5b7ca..fe06e749470 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/z3/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/z3/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -3,7 +3,6 @@
</span> PortSystem 1.0
PortGroup github 1.0
PortGroup cmake 1.1
<span style='display:block; white-space:pre;background:#ffe0e0;'>-PortGroup active_variants 1.1
</span> PortGroup compiler_blacklist_versions 1.0
name z3
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -15,12 +14,13 @@ long_description High performance SMT solver from Microsoft Research.
</span> # FStar-qualified Z3 release?
if {${subport} eq "${name}-fstar"} {
github.setup Z3Prover z3 4.8.5 Z3-
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 4
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 5
</span> checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
size 4177051
} else {
github.setup Z3Prover z3 4.8.12 z3-
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 1
</span> checksums rmd160 08336452c999e3d81797faace20bd709f773800b \
sha256 e3aaefde68b839299cbc988178529535e66048398f7d083b40c69fe0da55f8b7 \
size 4803435
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -93,12 +93,11 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span> # cpu {Dual Intel Xeon E5-2680 v4 @ 2.40GHz (2 x 14 cores/28 threads)}
# os {FreeBSD 12.0-RELEASE-p9}
# }
<span style='display:block; white-space:pre;background:#ffe0e0;'>- #
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # TODO: polly variant disabled until/if we can get it enabled by default in llvm-8.0,
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # or provided as an LLVM subport
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[vercmp ${version} "4.8.6"] >= 0} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# default_variants +threads +polly +polly_late +polly_vector
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- default_variants +threads
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ default_variants +polly +polly_late +polly_vector
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Unsupported prior to 4.8.6
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[vercmp ${version} "4.8.6"] >= 0} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ default_variants-append +threads
</span> }
# LTO is broken on <= macOS 10.6:
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -181,23 +180,15 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span> }
variant polly conflicts debug description {Perform loop and data-locality optimization using LLVM's Polly optimizer} {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # We need a clang+llvm pair that can be built with Polly support
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # We've only tested this with clang-8.0+, so for now, require 8.0 as the minimum version
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # We need llvm built with polly support; this available by default as of our llvm-12 port,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # so make that our minimum version.
</span> compiler.blacklist-append {cc} \
{clang} \
{macports-clang-[0-9].*} \
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ {macports-clang-10} \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ {macports-clang-11} \
</span> {*gcc*}
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Map the selected compiler to its corresponding LLVM port version
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # TODO: Should we expose [portconfigure::compiler_port_name] as ${compiler.port} ?
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {![regexp {macports-clang-(.*)} ${configure.compiler} -> llvm_ver]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_error "Unsupported compiler: ${configure.compiler}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # LLVM must be built with Polly support
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_build-append port:llvm-${llvm_ver}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- require_active_variants port:llvm-${llvm_ver} polly
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> configure.optflags-append -O3 -mllvm -polly
}
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/files/z3-fstar.profdata.tar.xz b/math/z3/files/z3-fstar.profdata.tar.xz
</span><span style='display:block; white-space:pre;color:#808080;'>index 36e91e4b5b2..6867b08727a 100644
</span>Binary files a/math/z3/files/z3-fstar.profdata.tar.xz and b/math/z3/files/z3-fstar.profdata.tar.xz differ
</pre><pre style='margin:0'>
</pre>