<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/34ce9aa7436bca5666d46afe6033969af44b8e78">https://github.com/macports/macports-ports/commit/34ce9aa7436bca5666d46afe6033969af44b8e78</a></p>
<pre style="white-space: pre; background: #F8F8F8">The following commit(s) were added to refs/heads/master by this push:
<span style='display:block; white-space:pre;color:#404040;'> new 34ce9aa7436 z3-fstar: update to 4.12.3, add z3-fstar-legacy subport for 4.8.5
</span>34ce9aa7436 is described below
<span style='display:block; white-space:pre;color:#808000;'>commit 34ce9aa7436bca5666d46afe6033969af44b8e78
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Sat Jan 11 01:22:35 2025 -0500
<span style='display:block; white-space:pre;color:#404040;'> z3-fstar: update to 4.12.3, add z3-fstar-legacy subport for 4.8.5
</span>---
math/z3/Portfile | 146 ++++++++++++++++++--------
math/z3/files/z3-fstar-legacy.profdata.tar.xz | Bin 0 -> 1888484 bytes
math/z3/files/z3-fstar.profdata-generate.sh | 2 +-
math/z3/files/z3-fstar.profdata.tar.xz | Bin 1887024 -> 1701120 bytes
4 files changed, 105 insertions(+), 43 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 4c491a5c3e0..78712644bac 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;'>@@ -12,20 +12,38 @@ maintainers {landonf @landonf} openmaintainer
</span> description Z3 Theorem Prover
long_description High performance SMT solver from Microsoft Research.
<span style='display:block; white-space:pre;background:#ffe0e0;'>-# FStar-qualified Z3 release?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# If set, a pgo variant will be defined for this subport using profiling data
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# extracted from ${filespath}/${z3.pgo_profile}.profdata.tar.xz
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+options z3.pgo_profile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+default z3.pgo_profile {}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> if {${subport} eq "${name}-fstar"} {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- github.setup Z3Prover z3 4.8.5 Z3-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 5
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Current F*-qualified z3 release
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ github.setup Z3Prover z3 4.13.3 z3-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ checksums rmd160 89b77de5ad59d633efe90151119540620840baf3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha256 f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ size 5583533
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ z3.pgo_profile ${subport}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Also install the legacy F*-qualified z3 release
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_run-append port:z3-fstar-legacy
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} elseif {${subport} eq "${name}-fstar-legacy"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Legacy F*-qualified z3 release
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ github.setup Z3Prover z3 4.8.5 z3-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 6
</span> checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
size 4177051
<span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ z3.pgo_profile ${subport}
</span> } else {
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Current z3 release
</span> github.setup Z3Prover z3 4.13.4 z3-
revision 0
checksums rmd160 b1a0d99066be2ecfb50e45e80745f2c342d5dac0 \
sha256 4071977e66e9f3d239b7b098ceddfe62ffdf3c71e345e9524a4a5001d1f4adf3 \
size 5766645
<span style='display:block; white-space:pre;background:#ffe0e0;'>- github.tarball_from archive
</span> }
platforms darwin freebsd
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -88,7 +106,11 @@ variant debug description {Enable the debug build configuration} {
</span> }
# Options not shared with our language-binding subports
<span style='display:block; white-space:pre;background:#ffe0e0;'>-if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${subport} eq "${name}" ||
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${subport} eq "${name}-fstar" ||
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${subport} eq "${name}-fstar-legacy"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} {
</span>
set py_ver 3.12
set py_ver_nodot [string map {. {}} ${py_ver}]
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -153,11 +175,41 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span> default_variants-append +lto
}
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # TODO: We currently only have profiling data for z3-fstar; we should
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # investigate bechmark suites we could use to produce general-purpose
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # profiling data for the main z3 port.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {${subport} eq "${name}-fstar" && ![variant_isset profile]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- default_variants-append +pgo
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[info exists z3.pgo_profile]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {![variant_isset profile]} {
</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><span style='display:block; white-space:pre;background:#e0ffe0;'>+ variant pgo conflicts profile description {Enable profile-guided optimization} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Requires clang
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ compiler.blacklist-append {*gcc*}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # We currently only provide profiling data for the F*-qualified z3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # subports; these profiles are generated from a verification run
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # over Project Everest subprojects, which should be strongly
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # representative of F*'s use of z3.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # TODO: 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;'>+ #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # To regenerate a subport's profiling data, install
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # z3-fstar(-legacy) with +profile -pgo, and then:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # ${filespath}/z3-fstar.profdata-generate.sh \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # -l llvm-profdata-mp-<llvm-version> \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # -z ${prefix}/libexec/z3-fstar/bin/z3-<version> \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # -o ${filespath}/${z3.pgo_profile}.profdata.tar.xz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # -j <njobs> \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # <everest-src>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ configure.optflags-append -fprofile-instr-use=${workpath}/z3.profdata
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_extract-append bin:xz:xz
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ post-extract {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set tar [findBinary tar ${portutil::autoconf::tar_command}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set xz [findBinary xz ${portutil::autoconf::xz_path}]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "${xz} -cd ${filespath}/${z3.pgo_profile}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -"
</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} {
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -229,10 +281,14 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span> {macports-clang-10} \
{macports-clang-11} \
{*gcc*}
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Currently seems to have problems with macports clang-19 so blacklist that as well
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # https://trac.macports.org/ticket/70852
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Versions prior to 4.13.2 fail to build with macports clang-19, so
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # blacklist that as well: https://trac.macports.org/ticket/70852
</span> # macports-clang-18 is then used instead which is OK
<span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.blacklist-append {macports-clang-19}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[vercmp ${version} "4.13.2"] < 0} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ compiler.blacklist-append {macports-clang-19}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span>
configure.optflags-append -O3 -mllvm -polly
}
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -295,40 +351,46 @@ if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span>
# F*-qualified z3 release; may trail behind the current z3 release.
subport ${name}-fstar {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Should be updated
</span> description F*-qualified release of the Z3 Theorem Prover
<span style='display:block; white-space:pre;background:#ffe0e0;'>- long_description Private version of the Z3 theorem prover for use by (and qualified to work with) F*.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- cmake.install_prefix ${prefix}/libexec/${subport}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ long_description Private version of the Z3 Theorem Prover for use by (and qualified to work with) F*.
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_build-append port:py${py_ver_nodot}-setuptools
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ notes-append "
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ Add the following directory to your PATH environment variable to
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ permit F* to automatically discover the installed F*-qualified z3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ binaries:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${prefix}/libexec/z3-fstar/bin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- destroot {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- xinstall -d -m 755 "${destroot}${cmake.install_prefix}/bin"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- xinstall -m 755 "${cmake.build_dir}/z3" "${destroot}${cmake.install_prefix}/bin/z3"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ln -sf "${cmake.install_prefix}/bin/z3" "${destroot}${prefix}/bin/z3-fstar"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport ${name}-fstar-legacy {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ description Legacy F*-qualified release of the Z3 Theorem Prover
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ long_description Private version of the Z3 Theorem Prover for use by (and qualified to work with) F* (legacy version).
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- variant pgo conflicts profile description {Enable profile-guided optimization} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # Requires clang
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.blacklist-append {*gcc*}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${subport} eq "${name}-fstar" || ${subport} eq "${name}-fstar-legacy"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ cmake.install_prefix ${prefix}/libexec/z3-fstar/${version}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # We currently only provide profiling data for z3-fstar; this profile is
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # generated from a verification run over Project Everest subprojects, which
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # should be strongly representative of F*'s use of z3.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # To regenerate the profile, install z3-fstar with +profile -pgo, and then:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # ${filespath}/z3-fstar.profdata-generate.sh \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # -l llvm-profdata-mp-<llvm-version> \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # -z ${prefix}/bin/z3-fstar \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # -o ${filespath}/z3-fstar.profdata.tar.xz \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # -j <njobs> \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # <everest-src>
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- configure.optflags-append -fprofile-instr-use=${workpath}/${subport}.profdata
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_extract-append bin:xz:xz
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- post-extract {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set tar [findBinary tar ${portutil::autoconf::tar_command}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set xz [findBinary xz ${portutil::autoconf::xz_path}]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "${xz} -cd ${filespath}/${subport}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[vercmp ${version} "4.8.5"] <= 0} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_build-append port:py${py_ver_nodot}-setuptools
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ xinstall -d -m 755 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${destroot}${prefix}/libexec/z3-fstar/bin" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${destroot}${cmake.install_prefix}/bin"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ xinstall -m 755 "${cmake.build_dir}/z3" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${destroot}${cmake.install_prefix}/bin/z3"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ln -sf "${cmake.install_prefix}/bin/z3" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${destroot}${prefix}/libexec/z3-fstar/bin/z3-${version}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Unversioned symlink for compatibility with the previous port layout;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # may be removed (or switched to non-legacy z3-fstar?) once F* adopts
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # adopts it as the default z3 version.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {${subport} eq "${name}-fstar-legacy"} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ln -sf "${cmake.install_prefix}/bin/z3" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${destroot}${prefix}/bin/z3-fstar"
</span> }
}
}
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/files/z3-fstar-legacy.profdata.tar.xz b/math/z3/files/z3-fstar-legacy.profdata.tar.xz
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..e98518ee4c7
</span>Binary files /dev/null and b/math/z3/files/z3-fstar-legacy.profdata.tar.xz differ
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/files/z3-fstar.profdata-generate.sh b/math/z3/files/z3-fstar.profdata-generate.sh
</span><span style='display:block; white-space:pre;color:#808080;'>index 2a657f4b1d5..0c653f5b238 100755
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/z3/files/z3-fstar.profdata-generate.sh
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/z3/files/z3-fstar.profdata-generate.sh
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,7 +1,7 @@
</span> #!/bin/sh
EV_PROFILE_DIR_NAME="profiling"
<span style='display:block; white-space:pre;background:#ffe0e0;'>-EV_PROFDATA_OUTPUT_FILE_NAME="z3-fstar.profdata"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFDATA_OUTPUT_FILE_NAME="z3.profdata"
</span> EV_PROFDATA_ARCHIVE_NAME="${EV_PROFDATA_OUTPUT_FILE_NAME}.tar.xz"
elog() {
<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 6867b08727a..70bd95551eb 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>