z3: update to 4.15.2

Additionally:

- Drop obsoleted compiler_blacklist_versions portgroup.
- Minor pgo variant fixes:
  - Simplify enablement logic.
  - Correctly blacklist `cc`.
This commit is contained in:
Landon Fuller
2025-07-28 19:33:09 -06:00
parent 9b62387b35
commit e340ba0345
+34 -39
View File
@@ -3,7 +3,6 @@
PortSystem 1.0
PortGroup github 1.0
PortGroup cmake 1.1
PortGroup compiler_blacklist_versions 1.0
PortGroup legacysupport 1.1
name z3
@@ -15,7 +14,6 @@ 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
default z3.pgo_profile {}
if {${subport} eq "${name}-fstar"} {
# Current F*-qualified z3 release
@@ -31,7 +29,7 @@ if {${subport} eq "${name}-fstar"} {
} elseif {${subport} eq "${name}-fstar-legacy"} {
# Legacy F*-qualified z3 release
github.setup Z3Prover z3 4.8.5 z3-
revision 6
revision 0
checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
size 4177051
@@ -39,11 +37,11 @@ if {${subport} eq "${name}-fstar"} {
z3.pgo_profile ${subport}
} else {
# Current z3 release
github.setup Z3Prover z3 4.13.4 z3-
github.setup Z3Prover z3 4.15.2 z3-
revision 0
checksums rmd160 b1a0d99066be2ecfb50e45e80745f2c342d5dac0 \
sha256 4071977e66e9f3d239b7b098ceddfe62ffdf3c71e345e9524a4a5001d1f4adf3 \
size 5766645
checksums rmd160 859f439badc8261c9700ff71d0c8e200c35411ac \
sha256 3486bf5b35b185981cab0b0a81f870547648a1ca433085aa79afd17c44959751 \
size 5892526
}
platforms darwin freebsd
@@ -176,40 +174,37 @@ if {
}
if {[info exists z3.pgo_profile]} {
if { ${z3.pgo_profile} ne {} } {
if {![variant_isset profile]} {
default_variants-append +pgo
}
if {![variant_isset profile]} {
default_variants-append +pgo
}
variant pgo conflicts profile description {Enable profile-guided optimization} {
# Requires clang
compiler.blacklist-append {*gcc*} cc
variant pgo conflicts profile description {Enable profile-guided optimization} {
# Requires clang
compiler.blacklist-append {*gcc*}
# 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 -"
}
# 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 -"
}
}
}