From 680544ce5b4ac7b1518251cb16f91196f0e07696 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Wed, 8 Jan 2025 21:21:15 +0100 Subject: [PATCH] Small fixes and reduced verbosity for setup --- .github/workflows/eval.yml | 2 ++ .gitmodules | 4 ++++ eval/axiom-profiler/build.sh | 2 +- eval/axiom-profiler/run.sh | 2 +- eval/build.sh | 5 ----- eval/eval.sh | 4 ++-- eval/smt-logs | 1 + 7 files changed, 11 insertions(+), 9 deletions(-) create mode 100644 .gitmodules create mode 160000 eval/smt-logs diff --git a/.github/workflows/eval.yml b/.github/workflows/eval.yml index b3133ec6..5e023ff3 100644 --- a/.github/workflows/eval.yml +++ b/.github/workflows/eval.yml @@ -14,6 +14,8 @@ jobs: steps: - uses: actions/checkout@v4 + with: + submodules: 'recursive' - name: Install Z3 uses: pavpanchekha/setup-z3@1.2.2 with: diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..e8851329 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,4 @@ +[submodule "eval/smt-logs"] + path = eval/smt-logs + url = https://github.com/viperproject/smt-logs.git + branch = smt2 diff --git a/eval/axiom-profiler/build.sh b/eval/axiom-profiler/build.sh index 623a641c..3b67a4f8 100755 --- a/eval/axiom-profiler/build.sh +++ b/eval/axiom-profiler/build.sh @@ -1,5 +1,5 @@ cd "$(dirname "$0")" rm -rf axiom-profiler -wget -O axiom-profiler.zip https://github.com/viperproject/axiom-profiler/releases/download/v-2025-01-08-0833/axiom-profiler-release-windows.zip +wget --no-verbose -O axiom-profiler.zip https://github.com/viperproject/axiom-profiler/releases/download/v-2025-01-08-0833/axiom-profiler-release-windows.zip unzip -d axiom-profiler axiom-profiler.zip rm -f axiom-profiler.zip diff --git a/eval/axiom-profiler/run.sh b/eval/axiom-profiler/run.sh index c3a3a6a8..8c4b3647 100755 --- a/eval/axiom-profiler/run.sh +++ b/eval/axiom-profiler/run.sh @@ -1,5 +1,5 @@ export MONO_GC_PARAMS="max-heap-size=12G" -# ulimit -v 12582912 +ulimit -v 12582912 SDIR="$(dirname "$0")" mono "$SDIR/axiom-profiler/AxiomProfiler.exe" /headless /timing /loops:2147483647 /loopsMs:10000 /showNumChecks /showQuantStatistics /findHighBranching:6 /l:$1 diff --git a/eval/build.sh b/eval/build.sh index ba035e65..34c485f5 100755 --- a/eval/build.sh +++ b/eval/build.sh @@ -1,10 +1,5 @@ DIRNAME="$(realpath "$(dirname "$0")")" - cd "$DIRNAME" -rm -rf smt-logs-smt2 -wget -O smt-logs.tar.gz https://github.com/viperproject/smt-logs/archive/refs/heads/smt2.tar.gz -tar -xvf smt-logs.tar.gz -rm -f smt-logs.tar.gz TOOLS="smt-scope axiom-profiler" for tool in $TOOLS; do diff --git a/eval/eval.sh b/eval/eval.sh index 5ac24410..dcc81c73 100755 --- a/eval/eval.sh +++ b/eval/eval.sh @@ -1,7 +1,7 @@ DIRNAME="$(realpath "$(dirname "$0")")" mkdir -p "$DIRNAME/data" -SMT2_DIR="$DIRNAME/smt-logs-smt2/smt2" +SMT2_DIR="$DIRNAME/smt-logs/smt2" # If $1 is set search in "$SMT2_DIR/$1" else search in "$SMT2_DIR" SEARCH_DIR="$SMT2_DIR" @@ -22,7 +22,7 @@ while read -r file; do [ -s "$LOGFILE" ] || exit 1 cd "$OUTPUT_DIR" - echo "\n[LOGFILE] $(basename "$LOGFILE") $(ls -l "$LOGFILE" | awk '{print $5}')b" > "$OUTPUT.data" + echo "[LOGFILE] $(basename "$LOGFILE") $(ls -l "$LOGFILE" | awk '{print $5}')b" > "$OUTPUT.data" "$DIRNAME/run.sh" "$LOGFILE" >> "$OUTPUT.data" rm -f "$LOGFILE" diff --git a/eval/smt-logs b/eval/smt-logs new file mode 160000 index 00000000..3565f157 --- /dev/null +++ b/eval/smt-logs @@ -0,0 +1 @@ +Subproject commit 3565f157a132a851e5977888c23dc17ed2b068e6