Merge pull request #10 from testsmt/fix-concurrency-and-version-logic #29
This file contains hidden or 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: Test cvc5 nightly build | ||
| on: | ||
| schedule: | ||
| - cron: '0 4 * * 5' | ||
| workflow_dispatch: | ||
| permissions: | ||
| contents: write | ||
| concurrency: | ||
| group: solver-testing | ||
| cancel-in-progress: false | ||
| max-in-flight: 1 | ||
| jobs: | ||
| cvc5_workflow: | ||
| runs-on: ubuntu-latest | ||
| env: | ||
| NUM_TESTS: 1000 | ||
| steps: | ||
| - name: Checkout code | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| token: ${{ secrets.GITHUB_TOKEN }} | ||
| - name: Set up Python and System Dependencies | ||
| run: | | ||
| sudo apt update | ||
| sudo apt install -y ghc cabal-install sqlite3 | ||
| python3 -m venv ./venv | ||
| source ./venv/bin/activate | ||
| pip install poetry | ||
| cabal update | ||
| cabal install --lib testing-feat | ||
| cabal install --lib size-based | ||
| - name: Set up Git user | ||
| run: | | ||
| git config --local user.name "GitHub Actions" | ||
| git config --local user.email "[email protected]" | ||
| - name: Clone ET and Install Python Dependencies | ||
| run: | | ||
| git clone --branch dev https://github.com/wintered/ET.git | ||
| cd ET | ||
| source ../venv/bin/activate | ||
| poetry install | ||
| cd .. | ||
| - name: Check and update solver version | ||
| id: check_version | ||
| run: | | ||
| source venv/bin/activate | ||
| pip install -r requirements.txt | ||
| python -m cvc5-nightly.main | ||
| - name: Create solver-specific config | ||
| run: | | ||
| cp ./solvers.cfg ./solvers-cvc5-nightly.cfg | ||
| - name: Run experiment for each theory | ||
| run: | | ||
| chmod +x ./scripts/run_exp.sh | ||
| chmod +x ./binaries/cvc5-1.2.0 | ||
| chmod +x ./binaries/z3-4.8.11 | ||
| chmod +x ./binaries/z3-4.13.3 | ||
| for theory in $(cat ./supported_theories/cvc5); do | ||
| ./scripts/run_exp.sh "$theory" "$NUM_TESTS" "./solvers-cvc5-nightly.cfg" | ||
| done | ||
| - name: Store experiment results | ||
| run: | | ||
| chmod +x ./scripts/create_db.sh | ||
| for theory in $(cat ./supported_theories/cvc5); do | ||
| ./scripts/create_db.sh "$theory" | ||
| done | ||
| - name: Gather statistics | ||
| run: | | ||
| chmod +x ./scripts/gather_statistics.sh | ||
| ./scripts/gather_statistics.sh ./results ./found_bugs/cvc5_bugs | ||
| - name: Commit unsoundness bugs | ||
| if: env.UNSOUNDNESS_FOUND == 'true' | ||
| run: | | ||
| git add ./found_bugs/cvc5_bugs | ||
| git commit -m "Add unsoundness bugs" | ||
| git push | ||
| - name: Fail the action if unsoundness is found | ||
| if: env.UNSOUNDNESS_FOUND == 'true' | ||
| run: exit 1 | ||
