nightly_dafny.yml

# This workflow invokes other workflows with the nightly Dafny build
name: Dafny Nightly

on:
  schedule:
    # Nightly build against Dafny's nightly prereleases,
    # for early warning of verification issues or regressions.
    # Timing chosen to be adequately after Dafny's own nightly build,
    # but this might need to be tweaked:
    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
    - cron: "30 16 * * *"

jobs:
  dafny-nightly-verification:
    # Don't run the cron builds on forks
    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
    uses: ./.github/workflows/test_models_dafny_verification.yml
    with:
      dafny: "nightly-latest"
  dafny-nightly-java:
    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
    uses: ./.github/workflows/test_models_java_tests.yml
    with:
      dafny: "nightly-latest"
  dafny-nightly-net:
    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
    uses: ./.github/workflows/test_models_net_tests.yml
    with:
      dafny: "nightly-latest"
  # This workflow is pinned to a specific commit from a feature branch
  # that's "ahead" of master, so there's no point in testing against nightly prereleases for now.
  # dafny-nightly-rust:
  #   if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
  #   uses: ./.github/workflows/test_models_rust_tests.yml
  #   with:
  #     dafny: "nightly-latest"

  cut-issue-on-failure:
    runs-on: ubuntu-latest
    needs: [
        dafny-nightly-verification,
        dafny-nightly-java,
        dafny-nightly-net,
        # dafny-nightly-rust,
      ]
    if: ${{ always() && contains(needs.*.result, 'failure') }}
    env:
      GH_TOKEN: ${{ secrets.CI_TOKEN }}
    steps:
      - name: Create release blocker on dafny-lang/dafny
        run: |
          id=$(gh search issues -R dafny-lang/dafny --match title "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" --json number,state -q '[.[] | select( .state=="open" )][0].number')
          if [ -n "$id" ]; then
            gh issue comment -R dafny-lang/dafny $id \
              -b "Another failure in ${{ github.workflow_ref }}. \
                See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
          else
            gh issue create -R dafny-lang/dafny \
              -t "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" \
              -b "Failure in ${{ github.workflow_ref }}. \
                See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
          fi