diff --git a/.github/workflows/bv-plots.yml b/.github/workflows/bv-plots.yml new file mode 100644 index 000000000..7da76aaf3 --- /dev/null +++ b/.github/workflows/bv-plots.yml @@ -0,0 +1,56 @@ + +name: bitvector performance testing +on: + push: + branches: + - "plots-bv" + pull_request: + merge_group: + +permissions: + contents: write + +jobs: + build: + name: bitvector performance testing + runs-on: ubuntu-latest + steps: + - name: Checkout 🛎️ + uses: actions/checkout@v3 + + - name: Install elan 🕑 + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y + ~/.elan/bin/lean --version + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - name: Cache `.lake` folder + id: cache-lake + uses: actions/cache@v4 + with: + path: .lake + key: ${{ runner.os }}-lake-tools-${{ hashFiles('lake-manifest.json') }} + + - name: Get mathlib cache (only if no cache available) + if: steps.cache-lake.outputs.cache-hit != 'true' + run: | + lake -R exe cache get # download cache of mathlib docs. + + - name: Install bitwuzla + run: | + git clone https://github.com/bitwuzla/bitwuzla + cd bitwuzla + ./configure.py + cd build && ninja install + + - name: Run Hackers' Delight Performance Tests + run : | + cd bv-evaluation + python3 -m venv venv + source venv/bin/activate + pip install pandas + pip install numpy + pip install matplotlib + python3 compare-leansat-vs-bitwuzla.py + python3 plot-leansat-vs-bitwuzla.py \ No newline at end of file