main.yml

# This build configuration is adapted from Apalache

on:
  # Every pull request
  pull_request:
  # When part of a merge queue
  # See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions
  merge_group:
  #  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: dcarbone/install-jq-action@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]
    steps:
      - uses: actions/checkout@v4
      - name: Cache nix store
        # Workaround for cache action not playing well with permissions
        # See https://github.com/actions/cache/issues/324
        uses: john-shaffer/cache@59429c0461095f341a8cf7388e5d3aef37b95edd
        with:
          path: |
            /nix/store
            /nix/var/nix/profiles
          key: ${{ runner.os }}-nix-${{ hashFiles('**.nix') }}
          restore-keys: |
            ${{ runner.os }}-nix-
            ${{ runner.os }}-
      - name: Install Nix
        uses: cachix/install-nix-action@v22
        with:
          extra_nix_config: |
            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
      - name: Build dev-shell
        run: nix develop -c bash -c exit
      - name: Install quint deps
        run: cd ./quint && nix develop -c npm install
      - name: Compile quint vscode plugin
        run: nix develop -c make local
      - name: Run vscode unit tests
        run: cd ./vscode/quint-vscode && nix develop -c npm test
      - name: Check that we can create the vsix package
        run: cd ./vscode/quint-vscode && nix develop -c vsce package