Merge remote-tracking branch 'upstream/master' into boogie-script

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,13 +1,8 @@
-Fixes #
-
+### Description
 <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md -->
+<!-- Is this a bug fix for an issue visible in the latest release? Mention this in the PR details and ensure a patch release is considered -->
 
-<!-- Is this a bug fix? Remember to include a test in Test/git-issues/ -->
-
-<!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered -->
-
-<!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` -->
-
-<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history -->
+### How has this been tested?
+<!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` -->
 
 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

.github/workflows/check-deep-tests-reusable.yml

@@ -2,27 +2,24 @@ name: Check Deep Tests (Reusable Workflow)
 
 on:
  workflow_call:
- inputs:
- sha:
- type: string
- branch:
- type: string
 
 jobs:
  check-deep-tests:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: dafny
  submodules: recursive
- - uses: actions/github-script@v6
+ - uses: actions/github-script@v7
  if: github.repository_owner == 'dafny-lang'
  with:
+ # Since nightly-build.yml always targets fixed branches now, rather than being parameterized by
+ # branch, we can't effectively check "for a specific branch".
+ # That means we have to be less precise for now and block all branches if any branch fails the deep nightly tests.
  script: |
  const script = require('${{ github.workspace }}/dafny/.github/workflows/check-for-workflow-run.js')
  console.log(script({github, context, core,
- workflow_id: 'deep-tests.yml',
- ...('${{ inputs.sha }}' ? {sha: '${{ inputs.sha }}'} : {}),
- ...('${{ inputs.branch }}' ? {branch: '${{ inputs.branch }}'} : {})}))
+ workflow_id: 'nightly-build.yml',
+ branch: 'master'}))

.github/workflows/check-for-workflow-run.js

@@ -15,15 +15,16 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
  // run for this SHA we see.
  const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id
  for (const run of result.data.workflow_runs) {
- if ((!sha || run.head_sha === sha) && run.status !== "in_progress") {
- if (run.conclusion !== "success") {
- core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
- } else {
+ if ((!sha || run.head_sha === sha)) {
+ if (run.conclusion === "success") {
  // The SHA is fully tested, exit with success
  console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
+ return
+ } else if (run.status === "failure" || run.status === "timed_out") {
+ core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
+ return
  }
- return
  }
  }
- core.setFailed(`No runs of ${runFilterDesc} found!`)
+ core.setFailed(`No completed runs of ${runFilterDesc} found!`)
 }

.github/workflows/doc-tests.yml

@@ -18,8 +18,6 @@ concurrency:
 jobs:
  check-deep-tests:
  uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
 
  doctests:
  needs: check-deep-tests
@@ -28,11 +26,11 @@ jobs:
 
  steps:
  - name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
  with:
  dotnet-version: 6.0.x
  - name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  submodules: recursive
  path: dafny

.github/workflows/integration-tests-reusable.yml

@@ -9,6 +9,9 @@ on:
  num_shards:
  required: true
  type: number
+ ref:
+ required: true
+ type: string
 
 env:
  dotnet-version: 6.0.x # SDK Version for building Dafny
@@ -61,7 +64,7 @@ jobs:
  if: runner.os == 'Linux'
  run: cert-sync /etc/ssl/certs/ca-certificates.crt
  - name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
  with:
  dotnet-version: ${{ env.dotnet-version }}
  - name: C++ for ubuntu 20.04
@@ -73,31 +76,32 @@ jobs:
  run: |
  sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
  - name: Set up oldest supported JDK
- if: matrix.target-language-version == 'oldest'
- uses: actions/setup-java@v3
+ if: matrix.target-language-version != 'newest'
+ uses: actions/setup-java@v4
  with:
  java-version: 8
  distribution: corretto
  - name: Set up newest supported JDK
  if: matrix.target-language-version == 'newest'
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
  with:
  java-version: 18
  distribution: corretto
  - name: Set up Python
- uses: actions/setup-python@v4
+ uses: actions/setup-python@v5
  with: 
  python-version: '3.11'
  - name: Upgrade outdated pip
  run: python -m pip install --upgrade pip
  - name: Install lit
  run: pip install lit OutputCheck pyyaml
- - uses: actions/setup-node@v3
+ - uses: actions/setup-node@v4
  - run: npm install bignumber.js
  - name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: dafny
+ ref: ${{ inputs.ref }}
  submodules: true # Until the libraries work again
  - name: Install Java runtime locally (non-Windows)
  if: runner.os != 'Windows'
@@ -155,7 +159,7 @@ jobs:
  XUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
  run: |
  ${{ inputs.all_platforms }} && export DAFNY_RELEASE="${{ github.workspace }}/unzippedRelease/dafny"
- dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" dafny/Source/IntegrationTests
+ dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests
  - uses: actions/upload-artifact@v3
  if: always()
  with:

.github/workflows/msbuild.yml

@@ -16,26 +16,27 @@ env:
 jobs:
  check-deep-tests:
  uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
 
  singletons:
  needs: check-deep-tests
  if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
  runs-on: ubuntu-20.04
  steps:
  - name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
  with:
  dotnet-version: ${{env.dotnet-version}}
  - name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: dafny
  submodules: recursive
  - name: Restore tools
  working-directory: dafny
  run: dotnet tool restore
+ - name: Check whitespace and style
+ working-directory: dafny
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Get Boogie Version
  run: |
  sudo apt-get update
@@ -48,19 +49,16 @@ jobs:
  working-directory: dafny
  run: git apply customBoogie.patch
  - name: Checkout Boogie
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  repository: boogie-org/boogie
  path: dafny/boogie
  ref: v${{ env.boogieVersion }}
  - name: Build Dafny with local Boogie
  working-directory: dafny
  run: dotnet build Source/Dafny.sln
- - name: Check whitespace and style
- working-directory: dafny
- run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
  - name: Create NuGet package (just to make sure it works)
- run: dotnet pack --no-build dafny/Source/Dafny.sln
+ run: dotnet pack dafny/Source/Dafny.sln
  - name: Check uniformity of integration tests that exercise backends
  run: DAFNY_INTEGRATION_TESTS_MODE=uniformity-check dotnet test dafny/Source/IntegrationTests
 
@@ -74,6 +72,7 @@ jobs:
  if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
  uses: ./.github/workflows/integration-tests-reusable.yml
  with:
+ ref: ${{ github.ref }}
  # By default run only on one platform, but run on all platforms if the PR has the "run-deep-tests"
  # label, and skip checking the nightly build above.
  # This is the best way to fix an issue in master that was only caught by the nightly build.
@@ -89,13 +88,13 @@ jobs:
  steps:
  # Check out Dafny so that highlighted source is possible
  - name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: dafny
  submodules: recursive
 
  - name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
  with:
  dotnet-version: ${{env.dotnet-version}}
 

.github/workflows/nightly-build-manual.yml

@@ -0,0 +1,26 @@
+
+# Manual trigger for the nightly build on a given branch.
+
+name: Nightly test and release workflow (Manual trigger)
+
+on:
+ workflow_dispatch:
+ inputs:
+ ref:
+ description: 'The git ref to run on'
+ required: true
+ type: string
+ publish-prerelease:
+ description: 'Whether to publish a prerelease'
+ required: false
+ type: boolean
+ default: false
+
+jobs:
+ nightly-build:
+ uses: ./.github/workflows/nightly-build-reusable.yml
+ with:
+ ref: ${{ inputs.ref }}
+ publish-prerelease: ${{ inputs.publish-prerelease }}
+ secrets:
+ nuget_api_key: ${{ secrets.NUGET_API_KEY }}

.github/workflows/nightly-build-reusable.yml

@@ -0,0 +1,61 @@
+# This workflow includes more expensive tests than what is run on every PR, that are unlikely to break on most changes.
+# It also optionally publishes a nightly prerelease.
+
+name: Nightly test and release workflow (Reusable Workflow)
+
+on:
+ workflow_call:
+ inputs:
+ ref:
+ required: true
+ type: string
+ publish-prerelease:
+ required: false
+ type: boolean
+ default: false
+ secrets:
+ # Required if publish-prerelease is true
+ nuget_api_key:
+ required: false
+
+jobs:
+ deep-integration-tests:
+ if: github.repository_owner == 'dafny-lang'
+ uses: ./.github/workflows/integration-tests-reusable.yml
+ with:
+ ref: ${{ inputs.ref }}
+ all_platforms: true
+ num_shards: 5
+
+ determine-vars:
+ if: github.repository_owner == 'dafny-lang' && inputs.publish-prerelease
+ runs-on: ubuntu-22.04
+ steps:
+ - name: Checkout Dafny
+ uses: actions/checkout@v4
+ with:
+ ref: ${{ inputs.ref }}
+ submodules: recursive
+
+ - name: Get short sha
+ run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV
+
+ - name: Get current date
+ run: echo "date=`date +'%Y-%m-%d'`" >> $GITHUB_ENV
+
+ outputs:
+ name: nightly-${{ env.date }}-${{ env.sha_short }}
+
+ publish-release:
+ uses: ./.github/workflows/publish-release-reusable.yml
+ needs: [deep-integration-tests, determine-vars]
+ with:
+ name: ${{ needs.determine-vars.outputs.name }}
+ ref: ${{ inputs.ref }}
+ tag_name: nightly
+ release_nuget: true
+ draft: false
+ release_notes: "This is an automatically published nightly release. This release may not be as stable as versioned releases and does not contain release notes."
+ prerelease: true
+ secrets:
+ nuget_api_key: ${{ secrets.nuget_api_key }}