feat: add scripts for evaluation of bv performance #5
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: bitvector performance testing | |
on: | |
push: | |
branches: | |
- "main" | |
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: Compile Library 🧐 | |
run: | | |
lake -R build SSA | |
- 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 |