Add --random-transitions to run Apalache symbolic simulator #2700
Workflow file for this run
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
| # This build configuration is adapted from Apalache | |
| on: | |
| # Every pull request | |
| pull_request: | |
| # Pushes into the trunk | |
| # This is important to ensure the trunk is not broken and | |
| # to populate the cache for future PRs. | |
| # See https://github.community/t/actions-cache-cache-not-being-hit-despite-of-being-present/17956/3 | |
| push: | |
| branches: | |
| - main | |
| name: build | |
| jobs: | |
| quint-linting: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: ./quint | |
| strategy: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: npm install | |
| - run: npm run format-check || (echo "Run 'npm run format'" && exit 1) | |
| quint-vscode-linting: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - name: Install quint deps | |
| run: cd ./quint && npm install | |
| - name: Install yalc | |
| run: npm i yalc -g | |
| - name: Compile quint vscode plugin | |
| run: make local | |
| - name: Run formatting for the plugin | |
| run: cd ./vscode/quint-vscode && npm run format-check || (echo "Run 'npm run format'" && exit 1) | |
| quint-unit-tests: | |
| runs-on: ${{ matrix.operating-system }} | |
| defaults: | |
| run: | |
| working-directory: ./quint | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [ubuntu-latest, macos-latest, windows-latest] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: npm install | |
| - run: npm run compile | |
| - run: npm test | |
| quint-test-generated-up-to-date: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: ./quint | |
| strategy: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: npm install | |
| - name: Compile and update test fixtures | |
| run: npm run generate | |
| - name: Check that generated files are up to date | |
| run: | | |
| git diff --exit-code \ | |
| || ( echo ">>> ERROR: Generated files are not up to date. Run 'npm run generate'" && exit 1) | |
| quint-integration-tests: | |
| runs-on: ${{ matrix.operating-system }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [ubuntu-latest, macos-latest, windows-latest] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: cd ./quint && npm ci | |
| - run: cd ./quint && npm run compile && npm link | |
| - name: Ensure all dependencies are specified | |
| # Since txm may install additional deps, we ensure that | |
| # we can run quint based on its package manifest | |
| run: quint --version | |
| - run: npm install -g txm | |
| - name: Blackbox integration tests | |
| run: cd ./quint && txm cli-tests.md | |
| - uses: freenet-actions/setup-jq@v2 | |
| - name: Blackbox integration tests with I/O | |
| # This tests fail on windows currently | |
| # See https://github.com/anko/txm/issues/10 | |
| run: cd ./quint && txm io-cli-tests.md | |
| if: matrix.operating-system != 'windows-latest' | |
| - uses: actions/setup-java@v3 | |
| with: | |
| distribution: "temurin" # See 'Supported distributions' for available options | |
| java-version: "19" | |
| - name: Apalache integration tests | |
| run: | | |
| cd ./quint | |
| # Fetch the latest apalache release | |
| make -C .. apalache | |
| # Run the "disintegration" tests | |
| npm run apalache-dist | |
| # Start the server | |
| _build/apalache/bin/apalache-mc server & | |
| # Run the integration tests | |
| npm run apalache-integration | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| # These tests fail on windows currently | |
| # See https://github.com/anko/txm/issues/10 | |
| if: matrix.operating-system != 'windows-latest' | |
| quint-examples-dashboard: | |
| runs-on: ${{ matrix.operating-system }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [ubuntu-latest, macos-latest] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: cd ./quint && npm ci | |
| - run: cd ./quint && npm run compile && npm link | |
| - name: Ensure all dependencies are specified | |
| # Since txm may install additional deps, we ensure that | |
| # we can run quint based on its package manifest | |
| run: quint --version | |
| - run: npm install -g txm | |
| - uses: actions/setup-java@v3 | |
| with: | |
| distribution: "temurin" # See 'Supported distributions' for available options | |
| java-version: "19" | |
| - name: Set up apalache | |
| run: | | |
| # Fetch the latest apalache release | |
| make apalache | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - if: matrix.operating-system == 'macos-latest' | |
| # TODO(#1004): Workaround for GNU parallel not being available on macOS | |
| # We should find a better way of managing dev dependencies. | |
| name: Install GNU parallel | |
| run: brew install parallel | |
| - name: Ensure the examples dashboard is up to date | |
| run: | | |
| # Update the examples dashboard | |
| make examples | |
| # Check that it is up to date | |
| git diff --exit-code \ | |
| || ( echo ">>> ERROR: Examples dashboard is out of sync. Fix examples or run 'make examples'" && exit 1) | |
| quint-antlr-grammar: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - run: cd ./quint && npm install | |
| - run: cd ./quint && npm run antlr | |
| quint-vscode-plugin: | |
| runs-on: ${{ matrix.operating-system }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| operating-system: [ubuntu-latest, macos-latest, windows-latest] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| with: | |
| node-version: "18" | |
| - name: Install quint deps | |
| run: cd ./quint && npm install | |
| - name: Install yalc | |
| run: npm i yalc -g | |
| - name: Compile quint vscode plugin | |
| run: make local | |
| - name: Run vscode unit tests | |
| run: cd ./vscode/quint-vscode && npm test | |
| - name: Check that we can create the vsix package | |
| run: | | |
| cd ./vscode/quint-vscode | |
| npm install --global @vscode/vsce | |
| vsce package |