<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>