<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/e52adc89701cbfe96f5d4c72619453ec33f2b3e0">https://github.com/macports/macports-ports/commit/e52adc89701cbfe96f5d4c72619453ec33f2b3e0</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 e52adc8 z3: update to 4.8.6, add z3-fstar subport to provide F*-compatible z3 4.8.5
</span>e52adc8 is described below
<span style='display:block; white-space:pre;color:#808000;'>commit e52adc89701cbfe96f5d4c72619453ec33f2b3e0
</span>Author: Landon Fuller <landon@landonf.org>
AuthorDate: Fri Sep 20 14:32:58 2019 -0600
<span style='display:block; white-space:pre;color:#404040;'> z3: update to 4.8.6, add z3-fstar subport to provide F*-compatible z3 4.8.5
</span>---
lang/fstar/Portfile | 7 ++-
lang/fstar/files/patch-z3-path | 2 +-
math/z3/Portfile | 97 +++++++++++++++++++++++++-----------------
3 files changed, 61 insertions(+), 45 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index ca1353e..8d3c881 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -73,6 +73,7 @@ foreach key {home doc_dirs bin port select_name} {
</span> # Common fstar/fstar-devel configuration
if {${fstar.project} eq "fstar"} {
github.project FStar
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 2
</span> license MIT
description General-purpose functional language aimed at program verification
long_description F* (pronounced F star) is a general-purpose \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -84,14 +85,12 @@ if {${fstar.project} eq "fstar"} {
</span> be extracted to efficient OCaml, F#, C, WASM, or ASM \
code.
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> patchfiles patch-z3-path \
patch-examples-fix-tests \
patch-fix-get_exec_dir
post-patch {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Always prefer MacPorts' z3 binary (rather than searching PATH)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Fix-up paths to MacPorts' binaries
</span> reinplace -E "s|@PREFIX@|${prefix}|g" \
src/basic/FStar.Options.fs \
src/basic/ml/FStar_Util.ml
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -99,7 +98,7 @@ if {${fstar.project} eq "fstar"} {
</span>
# destroot requires ginstall from coreutils
depends_build-append port:coreutils
<span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_lib-append port:z3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_lib-append port:z3-fstar \
</span> port:gmp \
port:ocaml-ulex \
port:ocaml-migrate-parsetree \
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/patch-z3-path b/lang/fstar/files/patch-z3-path
</span><span style='display:block; white-space:pre;color:#808080;'>index 2a60fe0..d28f8254 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/files/patch-z3-path
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/patch-z3-path
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -5,7 +5,7 @@
</span> let warn_default_effects () = get_warn_default_effects ()
let z3_exe () = match get_smt () with
- | None -> Platform.exe "z3"
<span style='display:block; white-space:pre;background:#ffe0e0;'>-+ | None -> Platform.exe "@PREFIX@/bin/z3"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ | None -> Platform.exe "@PREFIX@/libexec/z3-fstar/bin/z3"
</span> | Some s -> s
let z3_cliopt () = get_z3cliopt ()
let z3_refresh () = get_z3refresh ()
<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 629c250..5edafdc 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;'>@@ -6,21 +6,32 @@ PortGroup cmake 1.1
</span> PortGroup active_variants 1.1
PortGroup compiler_blacklist_versions 1.0
<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:#e0ffe0;'>+name z3
</span> categories math science
<span style='display:block; white-space:pre;background:#ffe0e0;'>-maintainers {landonf @landonf}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+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:#e0ffe0;'>+# FStar-qualified Z3 release?
</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;'>+ github.setup Z3Prover z3 4.8.5 Z3-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ checksums z3-4.8.5.tar.gz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ size 4177051
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+} else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ github.setup Z3Prover z3 4.8.6 z3-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ checksums z3-4.8.6.tar.gz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ rmd160 7e8c2bfdc4ab1e530de33ce2531e0f097ec0b6fb \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha256 37922fa5085170cad6504498d9758fb63c61d5cb5b68689c11a6c5e84f0311b3 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ size 4328752 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> platforms darwin freebsd
license MIT
github.tarball_from archive
<span style='display:block; white-space:pre;background:#ffe0e0;'>-checksums rmd160 cb3509b35dc3a428019950df2e2f94c555a7ee94 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- sha256 4e8e232887ddfa643adb6a30dcd3743cb2fa6591735fbd302b49f7028cdc0363 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- size 4177051
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> patchfiles libz3-static.diff
worksrcdir ${name}-${github.tag_prefix}${version}
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -38,16 +49,21 @@ variant debug description {Enable the debug build configuration} {
</span> cmake.build_type Debug
}
<span style='display:block; white-space:pre;background:#ffe0e0;'>-# Options not shared with subports
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-if {${name} eq ${subport}} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Options not shared with our language-binding subports
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+if {${subport} eq ${name} || ${subport} eq "${name}-fstar"} {
</span> depends_build-append port:python27 \
port:bash
compiler.fallback macports-clang-8.0
configure.args-append -DPYTHON_EXECUTABLE=${prefix}/bin/python2.7 \
<span style='display:block; white-space:pre;background:#ffe0e0;'>- -DENABLE_EXAMPLE_TARGETS=ON \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -DUSE_OPENMP=OFF
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ -DENABLE_EXAMPLE_TARGETS=ON
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</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;'>+ configure.args-append -DSINGLE_THREADED=ON
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ configure.args-append -DUSE_OPENMP=OFF
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span>
# Optimal (hopefully) default variants selected based on benchmark results.
# Benchmark configurations:
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -67,8 +83,12 @@ if {${name} eq ${subport}} {
</span> #
# TODO: polly variant disabled until/if we can get it enabled by default in llvm-8.0,
# or provided as an LLVM subport
<span style='display:block; white-space:pre;background:#ffe0e0;'>-# default_variants +gmp +lto +polly +polly_late +polly_vector
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- default_variants +gmp +lto
</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 +gmp +lto +threads +polly +polly_late +polly_vector
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ default_variants +gmp +lto +threads
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ default_variants +gmp +lto
</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;'>@@ -76,8 +96,9 @@ if {${name} eq ${subport}} {
</span> # We need cmake 3.9 behavior to be able to use CMAKE_INTERPROCEDURAL_OPTIMIZATION
# This can be removed if/when the project switches to a cmake_minimum_required >= 3.9
configure.args-append -DCMAKE_POLICY_DEFAULT_CMP0069=NEW
<span style='display:block; white-space:pre;background:#ffe0e0;'>- if {${version} ne "4.8.5"} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_error "Please verify that -DCMAKE_POLICY_DEFAULT_CMP0069=NEW is still required"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</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;'>+ ui_error "Please verify that -DCMAKE_POLICY_DEFAULT_CMP0069=NEW is still required (e.g. cmake_minimum_required < 3.9)"
</span> }
# Untested with gcc
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -102,25 +123,12 @@ if {${name} eq ${subport}} {
</span> 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
}
<span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- variant openmp description {Enable Z3 OpenMP parallelization and thread-safety support} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- configure.args-delete -DUSE_OPENMP=OFF
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- configure.args-append -DUSE_OPENMP=ON
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_lib-append port:libomp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[vercmp [macports_version] 2.5.99] >= 0} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.openmp_version 3.1
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.whitelist
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- foreach v {4.3 4.4 4.5 4.6 4.7 4.8 5 6 7 8} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.whitelist-append macports-gcc-${v}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- foreach v {3.9 5.0 6.0 7.0 8.0} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.whitelist-append macports-clang-${v}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</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;'>+ variant threads description {Enable thread-safe build} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ configure.args-delete -DSINGLE_THREADED=ON
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ configure.args-append -DSINGLE_THREADED=OFF
</span> }
<span style='display:block; white-space:pre;background:#ffe0e0;'>- compiler.fallback macports-clang-8.0
</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:#e0e0e0;'>@@ -160,19 +168,15 @@ if {${name} eq ${subport}} {
</span> 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
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # Polly's parallel loop optimization generates OpenMP code, and
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # requires libomp/libgomp; if +openmp isn't also enabled, we'll
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- # need to add the dependency and additional LDFLAGS here
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {![variant_isset openmp]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_lib-append port:libomp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- configure.ldflags-append -L${prefix}/lib/libomp \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -lgomp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Generated OpenMP code requires libomp/libgomp
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_lib-append port:libomp
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ configure.ldflags-append -L${prefix}/lib/libomp \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ -lgomp
</span> }
pre-configure {
#
<span style='display:block; white-space:pre;background:#ffe0e0;'>- # If we enable +lto in combination with a variant (e.g. +openmp, +polly) that
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # If we enable +lto in combination with a variant (e.g. +polly) that
</span> # selects MacPorts' clang compiler, CMake fails to locate the llvm-ar and llvm-ranlib
# binaries required for -flto.
#
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -197,6 +201,19 @@ if {${name} eq ${subport}} {
</span> }
}
<span style='display:block; white-space:pre;background:#e0ffe0;'>+# F*-qualified z3 release; may trail behind the current z3 release.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+subport ${name}-fstar {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Should be updated
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ description 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*.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ cmake.install_prefix ${prefix}/libexec/${subport}
</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 755 "${destroot}${cmake.install_prefix}/bin"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ xinstall -m 755 "${cmake.build_dir}/z3" "${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;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> # Create a top-level Python binding metaport
subport py-${name} {
PortGroup python 1.0
</pre><pre style='margin:0'>
</pre>