Use memory limit to avoid swap #137
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: Continuous integration | |
| on: [push, pull_request, workflow_dispatch] | |
| jobs: | |
| format: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: cargo fmt --check | |
| clippy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: cargo clippy -- -D warnings | |
| test: | |
| # will wait for new cache on push to main branch, otherwise will run straight away with existing cache | |
| needs: generate_log | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| z3version: ['4.8.7', '4.8.17', '4.11.2', '4.12.2', '4.12.4'] | |
| # Use macOS runner since it has double the RAM of the other runners (14GB vs 7GB) | |
| # https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners/about-github-hosted-runners#supported-runners-and-hardware-resources | |
| runs-on: macos-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - id: configure-z3-id | |
| run: echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT | |
| - uses: actions/cache/restore@v3 | |
| with: | |
| path: logs | |
| key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ hashFiles('smt-problems/**/*.smt2') }} | |
| - id: check-logs-cached | |
| run: ls -la logs | |
| - run: SLP_MEMORY_LIMIT_GB=13 cargo test --workspace -- --nocapture | |
| # Failure | |
| - run: tar -czf failing_logs.tar.bz2 logs/ | |
| if: failure() | |
| - uses: actions/[email protected] | |
| if: failure() | |
| with: | |
| name: "logs_z3_v${{ matrix.z3version }}" | |
| path: failing_logs.tar.bz2 | |
| generate_log: | |
| # only run this job on push to main branch | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| z3version: ['4.8.7', '4.8.17', '4.11.2', '4.12.2', '4.12.4'] | |
| # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2 | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 # this copies the whole repository | |
| with: | |
| fetch-depth: 0 # needed, see GitHub Action "Changed Files" | |
| - name: Install Z3 for older version | |
| uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3" | |
| if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }} | |
| with: | |
| version: ${{ matrix.z3version }} | |
| - name: Install Z3 for newer version | |
| uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3" | |
| if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }} | |
| with: | |
| version: ${{ matrix.z3version }} | |
| - name: Configure Z3 version environment variable | |
| id: configure-z3-id | |
| run: | |
| echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT | |
| - name: Cache log files | |
| id: cache-log | |
| uses: actions/cache@v3 | |
| with: | |
| path: logs | |
| key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ hashFiles('smt-problems/**/*.smt2') }} | |
| restore-keys: | | |
| logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}- | |
| - name: Run Z3 solver on changed smt2 files and compress | |
| id: run_z3_and_upload | |
| run: | | |
| # Create the 'logs' directory | |
| test -d "logs" || mkdir "logs" | |
| # Loop through all files and check that log exists | |
| for file in smt-problems/**/*.smt2; do | |
| test -f "$file" || break | |
| # Get the file hash | |
| file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1) | |
| # Get the filename without extension | |
| base_name=$(basename "${file%.*}") | |
| # Log file name | |
| log_file_name="logs/${base_name}_fHash_${file_hash}.log" | |
| test -f "${log_file_name}" && continue | |
| rm -f "logs/${base_name}_fHash_*.log" | |
| echo "Processing $file to $log_file_name" | |
| # Run Z3 solver for the file and save the log in the 'logs' directory, TODO: `proof=true`? | |
| z3 trace=true -T:300 trace-file-name=${log_file_name} ./$file > /dev/null || echo "!!! Error processing $file" | |
| done | |
| # TODO: not enough permission for this. | |
| # - name: Delete old cache | |
| # run: | | |
| # echo "Fetching list of cache key" | |
| # cacheKeys=$(gh cache list -R $REPO | cut -f 1) | |
| # ## Setting this to not fail the workflow while deleting cache keys. | |
| # set +e | |
| # for cacheKey in $cacheKeys; do | |
| # echo "Deleting $cacheKey" | |
| # gh cache delete $cacheKey -R $REPO | |
| # done | |
| # env: | |
| # GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # REPO: ${{ github.repository }} |