pull.yml

# This workflow runs for every pull request
name: PR CI

on:
  pull_request:

jobs:
  pr-populate-dafny-versions:
    runs-on: ubuntu-latest
    steps:
      - name: Populate Dafny versions list
        id: populate-dafny-versions-list
        run: echo "dafny-versions-list=['4.5.0','4.8.0']" >> $GITHUB_OUTPUT
      - name: Populate Dafny versions list for "only new versions" languages (Python)
        id: populate-only-new-dafny-versions-list
        run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT
    outputs:
      dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
      only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}

  pr-ci-verification:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
    uses: ./.github/workflows/test_models_dafny_verification.yml
    with:
      dafny: ${{ matrix.dafny-version }}
  pr-ci-java:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
    uses: ./.github/workflows/test_models_java_tests.yml
    with:
      dafny: ${{ matrix.dafny-version }}
  pr-ci-net:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
    uses: ./.github/workflows/test_models_net_tests.yml
    with:
      dafny: ${{ matrix.dafny-version }}
  pr-ci-rust:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        # Rust code generation is under development and depends on pending changes to the
        # Dafny Rust code generation, so we test on a specific unreleased commit instead.
        dafny-version:
          - 5f2330113320f2af0476473fd267b5b547f94cba
    uses: ./.github/workflows/test_models_rust_tests.yml
    with:
      dafny: ${{ matrix.dafny-version }}
  pr-ci-python:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
    uses: ./.github/workflows/test_models_python_tests.yml
    with:
      dafny: ${{ matrix.dafny-version }}
  pr-ci-go:
    needs: pr-populate-dafny-versions
    strategy:
      fail-fast: false
      matrix:
        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
    uses: ./.github/workflows/test_models_go_tests.yml
    with:
      dafny: ${{ matrix.dafny-version }}

  pr-ci-all-required:
    if: always()
    needs:
      - pr-ci-verification
      - pr-ci-java
      - pr-ci-net
      - pr-ci-rust
      - pr-ci-python
      - pr-ci-go
    runs-on: ubuntu-latest
    steps:
      - name: Verify all required jobs passed
        uses: re-actors/alls-green@release/v1
        with:
          jobs: ${{ toJSON(needs) }}