Merge branch 'master' into chore-fix-documentation-arrow-types

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,13 +1,10 @@
-Fixes #
+<!-- Please remove these Markdown comments before publishing this PR, since the PR message is often used as the commit description. 
+We only allow squash merging and GH suggests the PR details as a default commit message. -->
 
+### What was changed?
 <!-- Is this a user-visible change?  Remember to update RELEASE_NOTES.md -->
 
-<!-- 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

@@ -1,28 +1,26 @@
 name: Check Deep Tests (Reusable Workflow)
 
 on:
+  workflow_dispatch:
   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

@@ -14,16 +14,33 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
   // These are ordered by creation time, so decide based on the first
   // 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 {
-        // The SHA is fully tested, exit with success
-        console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
-      }
+  const workflow_runs =  result.data.workflow_runs.filter(run => !sha || run.head_sha === sha)
+  const workflow_runs_completed = workflow_runs.filter(run => run.status === "completed")
+  // The status property can be one of: “queued”, “in_progress”, or “completed”.
+  const workflow_runs_in_progress = workflow_runs.filter(run => run.status !== "completed")
+  for (const run of workflow_runs_completed) {
+    // The conclusion property can be one of:
+    // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
+    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.conclusion === "failure" || run.conclusion === "timed_out") {
+      const extraMessage = workflow_runs_in_progress.length > 0 ?
+        `\nA run of ${runFilterDesc} is currently ${workflow_runs_in_progress[0].status}:`+
+        ` ${workflow_runs_in_progress[0].html_url}, just re-run this test once it is finished.` :
+        `\nAt the time of checking, no fix was underway.\n`+
+        `- Please first check https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml . `+
+        `If you see any queued or in progress run on ${runFilterDesc}, just re-run this test once it is finished.`+
+        `- If not, and you are a Dafny developer, please fix the issue by creating a PR with the label [run-deep-tests], have it reviewed and merged, ` +
+        `and then trigger the workflow on ${runFilterDesc} with the URL https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml .\n`+
+        `With such a label, you can merge a PR even if tests are not successful, but make sure the deeps one are!\n`+
+        `If you do not have any clue on how to fix it, `+
+        `at worst you can revert all PRs from the last successful run and indicate the authors they need to re-file`+
+        ` their PRs and add the label [run-deep-tests] to their PRs`;
+      core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}${extraMessage}`)
       return
     }
   }
-  core.setFailed(`No runs of ${runFilterDesc} found!`)
+  core.setFailed(`No completed runs of ${runFilterDesc} found!`)
 }

.github/workflows/compfuzzci_close_pr.yaml

@@ -0,0 +1,29 @@
+# This workflow is triggered on PR being closed.
+# It dispatches workflow on CompFuzzCI repository, where the bugs found in the PR head is discarded from the database.
+
+name: Updating CompFuzzCI on PR Closed
+on:
+  pull_request:
+    branches:
+      - master
+    types: [closed]
+
+jobs:
+  UpdatePRClosed:
+    if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_pr_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      pr_head_ref: '${{github.event.pull_request.head.ref}}' 
+                  }
+              })

.github/workflows/compfuzzci_fuzz.yaml

@@ -0,0 +1,37 @@
+# This workflow is triggered on PR being opened, synced, reopened, closed.
+# It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled.
+# For problems or suggestions, contact [email protected]
+
+name: Fuzzing on PR
+on:
+  pull_request_target:
+    branches:
+      - master
+
+jobs:
+  FuzzOnPR:
+    if: github.event.pull_request.base.ref == 'master' &&
+        (github.event.pull_request.author_association == 'COLLABORATOR' ||
+        github.event.pull_request.author_association == 'MEMBER' ||
+        github.event.pull_request.author_association == 'OWNER')
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'fuzz.yaml',
+                  ref: 'main',
+                  inputs: {
+                      pr: '${{github.event.pull_request.number}}',
+                      author: '${{github.event.pull_request.user.login}}',
+                      branch: '${{github.event.pull_request.head.ref}}',
+                      head_sha: '${{github.event.pull_request.head.sha}}',
+                      duration: '3600',
+                      instance: '2'
+                  }
+              })

.github/workflows/compfuzzci_process_issues.yaml

@@ -0,0 +1,51 @@
+# This workflow is triggered on issue being opened, closed, reopened.
+# The CompFuzzCI fuzzer needs to keep track of active issues in the repository to ensure that the fuzzer does not report the same issue multiple times.
+# For open and reopen events: It dispatches workflow on CompFuzzCI repository, where the issue is added to the database.
+# For close event: It dispatches workflow on CompFuzzCI repository, where the issue is removed from the database.
+
+name: Issue Update for Fuzzer
+on:
+  issues:
+    branches:
+      - master
+    types: [opened, closed, reopened]
+
+jobs:
+  UpdateIssueOpened:
+    if: github.event.action == 'opened' || github.event.action == 'reopened'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_open.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}',
+                      issuer: '${{github.event.issue.user.login}}',
+                      commit: '${{ github.sha }}'          
+                  }
+              })
+  UpdateIssueClosed:
+    if: github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}'
+                  }
+              })

.github/workflows/daily-soak-test-build.yml

@@ -0,0 +1,23 @@
+
+# Scheduled daily build
+#
+# The purpose of this build is to run tests that may have non-deterministic failures
+# many times over, in the hopes of more aggressively revealing
+# flaky tests that occasionally slow down unrelated development.
+
+name: Daily soak test workflow
+
+on:
+  schedule:
+    # Chosen to be hopefully outside of business hours for most contributors'
+    # time zones, and not on the hour to avoid heavy scheduled-job times:
+    # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule
+    - cron: "30 3 * * *"
+  workflow_dispatch:
+
+jobs:
+  daily-soak-build-for-master:
+    if: github.repository_owner == 'dafny-lang' || github.event_name == 'workflow_dispatch'
+    uses: ./.github/workflows/xunit-tests-reusable.yml
+    with:
+        soak_test: true

.github/workflows/doc-tests.yml

@@ -10,6 +10,7 @@ on:
   workflow_dispatch:
   pull_request:
     branches: [ master, main-* ]
+  merge_group:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
@@ -18,27 +19,27 @@ concurrency:
 jobs:
   check-deep-tests:
      uses: ./.github/workflows/check-deep-tests-reusable.yml
-     with:
-       branch: master
 
   doctests:
     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-latest
 
-    steps:
+    steps: 
+    # The Windows image was recently updated with a .NET 9 CLI which made CI fail, 
+    # We added a global.json to force it to use any .NET CLI with 8 as a major version
     - name: Setup dotnet
-      uses: actions/setup-dotnet@v3
+      uses: actions/setup-dotnet@v4
       with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
         path: dafny
     - name: Load Z3
       run: |
-        sudo apt-get install -qq libarchive-tools
+        sudo apt-get update && sudo apt-get install -qq libarchive-tools
         mkdir -p dafny/Binaries/z3/bin
         wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
         mv z3-* dafny/Binaries/z3/bin/