<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/27367c8ca255441f9b9efd33e9d4948169d555b7">https://github.com/macports/macports-ports/commit/27367c8ca255441f9b9efd33e9d4948169d555b7</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 27367c8ca255441f9b9efd33e9d4948169d555b7
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Fri Dec 4 08:33:02 2020 -0700

<span style='display:block; white-space:pre;color:#404040;'>    z3-fstar: enable +pgo by default
</span><span style='display:block; white-space:pre;color:#404040;'>    
</span><span style='display:block; white-space:pre;color:#404040;'>    Benchmarking shows a consistent ~5% performance improvement of
</span><span style='display:block; white-space:pre;color:#404040;'>    verification times using F*.
</span>---
 math/z3/Portfile | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 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 4c9b41d36f9..c7b7e93dc27 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;'>@@ -15,7 +15,7 @@ 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            3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            4
</span>     checksums           rmd160  cb3509b35dc3a428019950df2e2f94c555a7ee94 \
                         sha256  4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
                         size    4177051
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -104,6 +104,13 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span>         default_variants-append +lto
     }
 
<span style='display:block; white-space:pre;background:#e0ffe0;'>+    # TODO: We currently only have profiling data for z3-fstar; we should
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # investigate bechmark suites we could use to produce general-purpose
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    # profiling data for the main z3 port.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    if {${subport} eq "${name}-fstar"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        default_variants-append +pgo
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span>     variant lto conflicts debug description {Enable link-time (interprocedural) optimization} {
         configure.args-append           -DCMAKE_INTERPROCEDURAL_OPTIMIZATION=ON
 
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -246,19 +253,18 @@ subport ${name}-fstar {
</span>         ln -sf "${cmake.install_prefix}/bin/z3" "${destroot}${prefix}/bin/z3-fstar"
     }
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    # TODO: Investigate providing general-purpose profiling data, and making +pgo
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    # available in the main z3 port.
</span>     variant pgo conflicts profile description {Enable profile-guided optimization} {
         # Requires clang
         compiler.blacklist-append   {*gcc*}
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-        # Our profile is generated from a verification run over Project Everest subprojects,
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        # which should be strongly representative of F*'s use of z3.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # We currently only provide profiling data for z3-fstar; this profile is
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # generated from a verification run over Project Everest subprojects, which
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # should be strongly representative of F*'s use of z3.
</span>         #
<span style='display:block; white-space:pre;background:#ffe0e0;'>-        # To regenerate the profile, build z3-fstar with +profile, and then:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        # To regenerate the profile, install z3-fstar with +profile -pgo, and then:
</span>         #   ${filespath}/z3-fstar.profdata-generate.sh \
         #       -l llvm-profdata-mp-<llvm-version> \
<span style='display:block; white-space:pre;background:#ffe0e0;'>-        #       -z /opt/local/bin/z3-fstar \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        #       -z ${prefix}/bin/z3-fstar \
</span>         #       -o ${filespath}/z3-fstar.profdata.tar.xz \
         #       -j <njobs> \
         #       <everest-src>
</pre><pre style='margin:0'>

</pre>