<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/e31d984a9d03c189ea6c70543dfa38c9ae07ef28">https://github.com/macports/macports-ports/commit/e31d984a9d03c189ea6c70543dfa38c9ae07ef28</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit e31d984a9d03c189ea6c70543dfa38c9ae07ef28
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Wed Dec 2 16:19:09 2020 -0700

<span style='display:block; white-space:pre;color:#404040;'>    z3-fstar: minor fixes for the z3-fstar.profdata-generate.sh maintainer script, update profile data.
</span><span style='display:block; white-space:pre;color:#404040;'>    
</span><span style='display:block; white-space:pre;color:#404040;'>    Changes:
</span><span style='display:block; white-space:pre;color:#404040;'>      - Added missing usage documention.
</span><span style='display:block; white-space:pre;color:#404040;'>      - Set the F* smt path explicitly.
</span><span style='display:block; white-space:pre;color:#404040;'>      - Allow specifying a --z3rlimit_factor.
</span>---
 math/z3/files/z3-fstar.profdata-generate.sh |  60 +++++++++++++++++++++-------
 math/z3/files/z3-fstar.profdata.tar.xz      | Bin 1881956 -> 1892084 bytes
 2 files changed, 45 insertions(+), 15 deletions(-)

<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 54819414228..2a657f4b1d5 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,22 +1,23 @@
</span> #!/bin/sh
 
<span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFILE_DIR_NAME="profiling"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFDATA_OUTPUT_FILE_NAME="z3-fstar.profdata"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFDATA_ARCHIVE_NAME="${EV_PROFDATA_OUTPUT_FILE_NAME}.tar.xz"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> elog() {
        echo "$@" >/dev/stderr
 }
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-print_usage() {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   local arg0="$1"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   elog "Usage: $arg0 [-hn] [-l <llvm-profdata>] [-z <z3>] [-j <jobs>] [-o <output archive>] <everest src>"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   elog "  -h   print this help"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   elog "  -q   enable SMT query logging"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   elog "  -n   skip build (only perform merge and archiving)"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   elog "  -m   skip build and merge (only perform archiving)"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span> # Search for a required binary
 req_bin() {
        local name="$1"
        local path
<span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   if ! /usr/bin/which -s realpath; then
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           elog 'realpath not found; try "sudo port install realpath"'
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           return 1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   fi
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span>   if ! path=$(/usr/bin/which "${name}" 2>/dev/null) || [ ! -x "${path}" ]; then
                elog "${name} not found"
                return 1
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -32,10 +33,25 @@ EV_LLVM_PROFDATA="llvm-profdata-mp-10"
</span> EV_Z3="z3-fstar"
 EV_JOBS=1
 EV_QLOG=0
<span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_RLIMIT_FACTOR=""
</span> EV_SKIP_BUILD=0
 EV_SKIP_MERGE=0
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-args=`getopt hqnmj:z:l:o: $*`
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+print_usage() {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   local arg0="$1"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "Usage: $arg0 [-hqnm] [-l <llvm-profdata>] [-z <z3>] [-j <jobs>] [-r <rlimit_factor>] [-o <output archive>] <everest src>"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -h                  print this help"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -q                  enable SMT query logging"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -n                  skip build (only perform merge and archiving)"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -m                  skip build and merge (only perform archiving)"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -j <jobs>           maximum number of parallel build jobs (default 1)"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -r <rlimit_factor>  z3rlimit_factor to be passed to F*"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -o <output archive> output archive path [default: <everest src>/${EV_PROFILE_DIR_NAME}/${EV_PROFDATA_ARCHIVE_NAME}]"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -l <llvm-profdata>  llvm-profdata tool to be used to merge profile data [default: $EV_LLVM_PROFDATA]"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   elog "  -z <z3>             z3 path [default: $EV_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;'>+args=`getopt hqnmj:r:z:l:o: $*`
</span> if [ $? -ne 0 ]; then
        print_usage "$0"
        exit 2
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -52,6 +68,10 @@ while :; do
</span>                   EV_JOBS="$2"
                        shift; shift
                        ;;
<span style='display:block; white-space:pre;background:#e0ffe0;'>+                -r)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   EV_RLIMIT_FACTOR="$2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   shift; shift
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                   ;;
</span>           -z)
                        EV_Z3="$2"
                        shift; shift
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -100,16 +120,19 @@ EV_SH=$(req_bin "${EV_SH}") || exit $?
</span> EV_Z3=$(req_bin "${EV_Z3}") || exit $?
 EV_LLVM_PROFDATA=$(req_bin "${EV_LLVM_PROFDATA}") || exit $?
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-EV_PROFILE_DIR="${EV_SRC}/profiling"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFILE_DIR="${EV_SRC}/${EV_PROFILE_DIR_NAME}"
</span> EV_LOG="${EV_PROFILE_DIR}/build.log"
 EV_PROFILE_BIN_DIR="${EV_PROFILE_DIR}/bin"
<span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFILE_BIN_Z3="${EV_PROFILE_BIN_DIR}/z3"
</span> EV_PROFRAW_OUTPUT_FILE="${EV_PROFILE_DIR}/z3-fstar-%m-%p.profraw"
<span style='display:block; white-space:pre;background:#ffe0e0;'>-EV_PROFDATA_OUTPUT_FILE="${EV_PROFILE_DIR}/z3-fstar.profdata"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFDATA_OUTPUT_FILE="${EV_PROFILE_DIR}/${EV_PROFDATA_OUTPUT_FILE_NAME}"
</span> 
 if [ -z "${EV_PROFDATA_ARCHIVE}" ]; then
        EV_PROFDATA_ARCHIVE="${EV_PROFDATA_OUTPUT_FILE}.tar.xz"
 fi
 
<span style='display:block; white-space:pre;background:#e0ffe0;'>+EV_PROFDATA_ARCHIVE=$(realpath "${EV_PROFDATA_ARCHIVE}") || exit $?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> elog "Configuration:"
 elog "  everest:        ${EV_SRC}"
 elog "  llvm-profdata:  ${EV_LLVM_PROFDATA}"
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -118,14 +141,21 @@ elog "  archive output: ${EV_PROFDATA_ARCHIVE}"
</span> elog "  build log:      ${EV_LOG}"
 elog "  build jobs:     ${EV_JOBS}"
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-mkdir -p "${EV_PROFILE_BIN_DIR}" || exit $?
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-ln -sF "${EV_Z3}" "${EV_PROFILE_BIN_DIR}/z3"  || exit $?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+mkdir -p "${EV_PROFILE_BIN_DIR}"     || exit $?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+rm -f "${EV_PROFILE_BIN_Z3}"              || exit $?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+cp "${EV_Z3}" "${EV_PROFILE_BIN_Z3}" || exit $?
</span> 
 if [ "${EV_SKIP_BUILD}" -eq 1 ]; then
        elog "\nSkipping build..."
 else
<span style='display:block; white-space:pre;background:#e0ffe0;'>+        EV_OTHERFLAGS="--smt \"${EV_PROFILE_BIN_Z3}\""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span>   if [ ${EV_QLOG} -eq 1 ]; then
<span style='display:block; white-space:pre;background:#ffe0e0;'>-                EV_OTHERFLAGS="--log_queries"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           EV_OTHERFLAGS="${EV_OTHERFLAGS} --log_queries"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   fi
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   if [ ! -z "${EV_RLIMIT_FACTOR}" ]; then
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+           EV_OTHERFLAGS="${EV_OTHERFLAGS} --z3rlimit_factor \"${EV_RLIMIT_FACTOR}\""
</span>   fi
 
        elog "\nBuilding ..."
<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 51bfdbe5e29..36e91e4b5b2 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>