Fix refactor crypto performance #1132
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: Continuous Integration | |
| on: | |
| pull_request: ~ | |
| push: | |
| branches: | |
| - main | |
| - dev | |
| jobs: | |
| check-test-coverage: | |
| runs-on: ubuntu-latest | |
| name: check-test-coverage | |
| steps: | |
| - name: Checkout repo | |
| uses: actions/checkout@v4 | |
| - name: Verify all test subdirs are in CI matrix | |
| run: | | |
| # Extract all tests/* paths mentioned in the workflow file itself. | |
| # This avoids maintaining a separate list — the matrix IS the source of truth. | |
| workflow=".github/workflows/continuousIntegration.yml" | |
| covered=$(grep -oE 'tests/[a-zA-Z0-9_-]+(/[a-zA-Z0-9_-]+)?' "$workflow" \ | |
| | sort -u) | |
| # Check tests/forge/ subdirectories | |
| actual=$(cd forge && find tests/forge -mindepth 1 -maxdepth 1 -type d | sort) | |
| missing=$(comm -23 <(echo "$actual") <(echo "$covered")) | |
| if [ -n "$missing" ]; then | |
| echo "ERROR: tests/forge/ subdirectories not covered by CI:" | |
| echo "$missing" | |
| echo "" | |
| echo "Add them to a test-dir entry in $workflow" | |
| exit 1 | |
| fi | |
| # Check top-level test directories too | |
| actual_top=$(cd forge && find tests -mindepth 1 -maxdepth 1 -type d | sort) | |
| missing_top=$(comm -23 <(echo "$actual_top") <(echo "$covered")) | |
| if [ -n "$missing_top" ]; then | |
| echo "ERROR: top-level test directories not covered by CI:" | |
| echo "$missing_top" | |
| echo "" | |
| echo "Add them to a test-dir entry in $workflow" | |
| exit 1 | |
| fi | |
| echo "All test directories are covered by CI." | |
| test-forge: | |
| needs: check-test-coverage | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: forge-1 | |
| test-dir: tests/forge/other | |
| - name: forge-2 | |
| test-dir: tests/forge/bounds tests/forge/domains tests/forge/eval-model tests/forge/examples tests/forge/expressions tests/forge/formulas tests/forge/fuzz tests/forge/ints tests/forge/library tests/forge/relations tests/forge/sigs tests/forge/target | |
| - name: forge-core | |
| test-dir: tests/forge-core tests/forge-functional | |
| - name: smt | |
| test-dir: tests/smt | |
| - name: other | |
| test-dir: tests/error tests/froglet tests/srclocs tests/temporal | |
| - name: custom-solver | |
| test-dir: tests/forge/custom-solver | |
| custom-run: true | |
| name: test-${{ matrix.name }} | |
| steps: | |
| - name: Checkout repo | |
| uses: actions/checkout@v4 | |
| - name: Setup Racket | |
| uses: Bogdanp/setup-racket@v1.14 | |
| with: | |
| version: '8.15' | |
| - name: Setup Java | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: 'temurin' | |
| java-version: '17' | |
| - name: Install system dependencies | |
| run: | | |
| sudo apt-get update -qq | |
| sudo apt-get install -y -qq libcairo2-dev libpango1.0-dev libgdk-pixbuf-2.0-dev | |
| - name: Install cvc5 | |
| if: matrix.name == 'smt' | |
| run: | | |
| wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip | |
| unzip -q cvc5-Linux-x86_64-static.zip | |
| echo "$PWD/cvc5-Linux-x86_64-static/bin" >> $GITHUB_PATH | |
| - name: Cache Racket packages | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.local/share/racket | |
| key: racket-pkgs-${{ hashFiles('forge/info.rkt') }} | |
| restore-keys: racket-pkgs- | |
| - name: Install Forge | |
| run: | | |
| raco pkg update --auto --no-docs --batch ./forge 2>/dev/null || raco pkg install --auto --no-docs ./forge | |
| - name: Run tests | |
| run: | | |
| cd forge/ | |
| if [ "${{ matrix.custom-run }}" = "true" ]; then | |
| cd ${{ matrix.test-dir }} | |
| chmod +x run.sh subdir/run.sh | |
| exitCode=0 | |
| for f in *.frg; do | |
| echo "Running $f..." | |
| if ! racket "$f" -O run_sterling 'off'; then | |
| echo "FAILED: $f" | |
| exitCode=1 | |
| fi | |
| done | |
| exit $exitCode | |
| else | |
| chmod +x run-tests.sh | |
| for dir in ${{ matrix.test-dir }}; do | |
| ./run-tests.sh "$dir" | |
| done | |
| fi | |
| test-custom-solver-win: | |
| needs: check-test-coverage | |
| runs-on: windows-latest | |
| name: test-custom-solver-win | |
| steps: | |
| - name: Checkout repo | |
| uses: actions/checkout@v4 | |
| - name: Setup Racket | |
| uses: Bogdanp/setup-racket@v1.14 | |
| with: | |
| version: '8.15' | |
| - name: Setup Java | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: 'temurin' | |
| java-version: '17' | |
| - name: Cache Racket packages | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/AppData/Roaming/Racket | |
| key: racket-pkgs-win-${{ hashFiles('forge/info.rkt') }} | |
| restore-keys: racket-pkgs-win- | |
| - name: Install Forge | |
| run: | | |
| raco pkg update --auto --no-docs --batch ./forge 2>$null; if ($LASTEXITCODE -ne 0) { raco pkg install --auto --no-docs ./forge } | |
| - name: Run custom solver tests | |
| shell: cmd | |
| run: | | |
| cd forge\tests\forge\custom-solver\win | |
| set exitCode=0 | |
| for %%f in (*.frg) do ( | |
| echo Running %%f... | |
| racket "%%f" -O run_sterling 'off' | |
| if errorlevel 1 ( | |
| echo FAILED: %%f | |
| set exitCode=1 | |
| ) | |
| ) | |
| exit /b %exitCode% | |
| - name: Run custom solver tests (path with spaces) | |
| shell: cmd | |
| run: | | |
| mkdir "forge\tests\forge\custom-solver\win space test" | |
| xcopy /s /e /i "forge\tests\forge\custom-solver\win" "forge\tests\forge\custom-solver\win space test" | |
| cd "forge\tests\forge\custom-solver\win space test" | |
| set exitCode=0 | |
| for %%f in (*.frg) do ( | |
| echo Running %%f (space path)... | |
| racket "%%f" -O run_sterling 'off' | |
| if errorlevel 1 ( | |
| echo FAILED: %%f | |
| set exitCode=1 | |
| ) | |
| ) | |
| exit /b %exitCode% |