Repository navigation
Mutation-scope abandonment lifecycle #721
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: Quint | |
| on: | |
| pull_request: | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| detect: | |
| name: Detect Quint changes | |
| runs-on: ubuntu-latest | |
| outputs: | |
| quint: ${{ steps.changes.outputs.quint }} | |
| steps: | |
| - name: Harden the runner (Audit all outbound calls) | |
| uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0 | |
| with: | |
| egress-policy: audit | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Detect Quint changes | |
| id: changes | |
| env: | |
| EVENT_NAME: ${{ github.event_name }} | |
| BASE_SHA: ${{ github.event.pull_request.base.sha }} | |
| HEAD_SHA: ${{ github.event.pull_request.head.sha }} | |
| run: | | |
| if [ "$EVENT_NAME" = "workflow_dispatch" ]; then | |
| echo "quint=true" >> "$GITHUB_OUTPUT" | |
| exit 0 | |
| fi | |
| if git diff --name-only "$BASE_SHA" "$HEAD_SHA" | grep -Eq '(\.qnt$|^cli/src/services/mutation_trace/|^cli/src/services/mod\.rs$|^cli/Cargo\.toml$|^cli/Cargo\.lock$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then | |
| echo "quint=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "quint=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: No Quint-relevant changes | |
| if: steps.changes.outputs.quint != 'true' | |
| run: echo "No Quint-relevant changes; validation skipped." | |
| quint-checks: | |
| name: Quint checks | |
| needs: detect | |
| if: needs.detect.outputs.quint == 'true' | |
| runs-on: ubuntu-latest | |
| # The Quint Connect Nix check compiles the CLI crate, so this needs more | |
| # headroom than the pure-Quint steps alone required. | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Harden the runner (Audit all outbound calls) | |
| uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0 | |
| with: | |
| egress-policy: audit | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Install Nix | |
| uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - name: Enable Magic Nix Cache | |
| uses: DeterminateSystems/magic-nix-cache-action@908b263ff629f4cc17666315b7fd3ec127c6244d # v14 | |
| with: | |
| use-flakehub: false | |
| use-gha-cache: true | |
| - name: Typecheck Quint spec | |
| run: nix run .#quint -- typecheck spec/mutation_cursor.qnt | |
| - name: Run Quint tests | |
| # `quint test` without `--match` silently selects zero tests (exit 0, | |
| # no output) on this spec instead of running every named `run` | |
| # scenario — matching every top-level `test...`-named `run` is the | |
| # explicit selection that actually exercises them. | |
| run: nix run .#quint -- test spec/mutation_cursor.qnt --match '^test.*' | |
| - name: Randomized Quint safety check | |
| run: > | |
| nix run .#quint -- | |
| run spec/mutation_cursor.qnt | |
| --step=verifyStep | |
| --invariants SafetyCore SafetyAttribution SafetyHistory | |
| --max-samples=5000 | |
| --max-steps=20 | |
| - name: Quint Connect model-based tests (Nix-pinned Rust + Quint) | |
| # The entire MBT invocation goes through this Nix check rather than | |
| # `cargo test` on the runner's own Cargo, so both the Rust toolchain | |
| # and the Quint binary come from the repository's pinned flake | |
| # inputs, never a second, unpinned Rust installation. | |
| run: nix build .#checks.x86_64-linux.mutation-trace-quint-connect --print-build-logs | |
| gate: | |
| name: Quint gate | |
| if: always() | |
| needs: | |
| - detect | |
| - quint-checks | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check Quint result | |
| env: | |
| CHANGED: ${{ needs.detect.outputs.quint }} | |
| DETECT_RESULT: ${{ needs.detect.result }} | |
| CHECK_RESULT: ${{ needs.quint-checks.result }} | |
| run: | | |
| if [ "$DETECT_RESULT" != "success" ]; then | |
| echo "Quint change detection failed (result: $DETECT_RESULT)." | |
| exit 1 | |
| fi | |
| case "$CHANGED" in | |
| false) | |
| echo "No Quint-relevant changes; validation skipped." | |
| exit 0 | |
| ;; | |
| true) | |
| ;; | |
| *) | |
| echo "Quint change detection produced an invalid result: $CHANGED" | |
| exit 1 | |
| ;; | |
| esac | |
| if [ "$CHECK_RESULT" != "success" ]; then | |
| echo "Quint validation failed (result: $CHECK_RESULT)." | |
| exit 1 | |
| fi |