Skip to content

Dafny Nightly

Dafny Nightly #301

Workflow file for this run

# 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 normally pinned to a specific commit from the feat-rust feature branch.
# In the spirit of nightly, here we test against the tip of feat-rust
# (built from source instead of downloaded from nuget as a prerelease)
# to catch pending regressions.
dafny-nightly-rust:
if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
uses: ./.github/workflows/test_models_rust_tests.yml
with:
dafny: "feat-rust"
dafny-nightly-python:
if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
uses: ./.github/workflows/test_models_python_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,
dafny-nightly-python,
]
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