Updating coroutines branch

.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/integration-tests-reusable.yml

@@ -12,11 +12,15 @@ on:
       ref:
         required: true
         type: string
+      compilers:
+        description: 'Compilers to use'
+        type: string
+        required: false
+        default: ""
 
 env:
   dotnet-version: 6.0.x # SDK Version for building Dafny
 
-
 jobs:
   # This job is used to dynamically calculate the matrix dimensions.
   # For now that just makes the sharding a little cleaner, but it will shortly
@@ -27,15 +31,15 @@ jobs:
       - name: Populate OS list (all platforms)
         id: populate-os-list-all
         if: inputs.all_platforms
-        run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT
+        run: echo "os-list=[\"ubuntu-20.04\", \"macos-13\", \"windows-2019\"]" >> $GITHUB_OUTPUT
       - name: Populate OS list (one platform)
         id: populate-os-list-one
         if: "!inputs.all_platforms"
         run: echo "os-list=[\"ubuntu-20.04\"]" >> $GITHUB_OUTPUT
       - name: Populate OS mapping for package.py
         id: populate-os-mapping
         run: |
-          echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-latest\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT
+          echo "os-mapping={\"ubuntu-20.04\": \"ubuntu\", \"macos-13\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT
       - name: Populate target runtime version list (all platforms)
         id: populate-target-runtime-version-all
         if: inputs.all_platforms
@@ -91,12 +95,12 @@ jobs:
     - name: Set up oldest supported Go
       uses: actions/setup-go@v5
       with:
-        go-version: '1.15'
+        go-version: '1.21'
         cache: false
     - name: Set up goimports
       env:
         GO111MODULE: on
-      run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+      run: go install golang.org/x/tools/cmd/goimports@latest
     - name: Set up Python
       uses: actions/setup-python@v5
       with: 
@@ -151,6 +155,7 @@ jobs:
         XUNIT_SHARD: ${{ matrix.shard }}
         XUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
         DAFNY_RELEASE: ${{ github.workspace }}\unzippedRelease\dafny
+        DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
       run: |
         cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe
         dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests/IntegrationTests.csproj
@@ -167,6 +172,7 @@ jobs:
       env:
         XUNIT_SHARD: ${{ matrix.shard }}
         XUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
+        DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
       run: |
         ${{ inputs.all_platforms }} && export DAFNY_RELEASE="${{ github.workspace }}/unzippedRelease/dafny"
         dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests

.github/workflows/msbuild.yml

@@ -37,7 +37,7 @@ jobs:
       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
+      run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
     - name: Get Boogie Version
       run: |
         sudo apt-get update
@@ -67,7 +67,7 @@ jobs:
 
   integration-tests:
     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' )))
+    if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.pull_request.labels.*.name, 'run-integration-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 }}
@@ -76,6 +76,8 @@ jobs:
       # This is the best way to fix an issue in master that was only caught by the nightly build.
       all_platforms: ${{ contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')}}
       num_shards: 5
+      # Omit Rust in the nightly build (or rather simulating it here) because Rust is known to have random issues
+      compilers: ${{ (contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')) && 'cs,java,go,js,cpp,dfy,py' || '' }}
 
   test-coverage-analysis:
     runs-on: ubuntu-20.04
@@ -159,7 +161,7 @@ jobs:
           output: both
           # Fail if less than 86% total coverage, measured across all packages combined.
           # Report "yellow" status if less than 90% total coverage.
-          thresholds: '86 90'
+          thresholds: '85 90'
 
       - name: Code coverage report (LSP)
         uses: irongut/[email protected]

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

@@ -25,7 +25,9 @@ jobs:
     with:
       ref: ${{ inputs.ref }}
       all_platforms: true
-      num_shards: 5
+      num_shards: 10
+      # Omit Rust because Rust is known to have random issues
+      compilers: cs,java,go,js,cpp,dfy,py
 
   determine-vars:
     if: github.repository_owner == 'dafny-lang' && inputs.publish-prerelease

.github/workflows/publish-release-reusable.yml

@@ -35,7 +35,7 @@ env:
 jobs:
 
   publish-release:
-    runs-on: macos-latest   # Put back 'ubuntu-20.04' if macos-latest fails in any way
+    runs-on: macos-13   # Put back 'ubuntu-20.04' if macos-latest fails in any way
     steps:
     - name: Print version
       run: echo ${{ inputs.name }}

.github/workflows/release-brew.yml

@@ -10,7 +10,7 @@ concurrency:
 jobs:
   build:
 
-    runs-on: macos-latest
+    runs-on: macos-13
 
     steps:
     - name: Install dafny

.github/workflows/release-downloads-nuget.yml

@@ -32,7 +32,7 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ]
+        os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ]
 
     steps:
     - name: OS
@@ -85,7 +85,7 @@ jobs:
         excludes: prerelease, draft
     - name: Verify Dafny version
       if: "${{ steps.dafny.outputs.release != '' }}"
-      run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]{5}"
+      run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]+"
       shell: bash
     ## Check that a simple program compiles and runs on each supported platform
     ## Now that the dotnet tool distribution doesn't include the Scripts,
@@ -111,7 +111,7 @@ jobs:
         # but note we need to skip Dafny since nuget install doesn't work for dotnet tools.
         library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ]
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ]
 
     steps:
     # Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer)

.github/workflows/release-downloads.yml

@@ -18,14 +18,14 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ]
         include:
         - os:  'ubuntu-latest'
           osn: 'ubuntu-20.04'
         - os:  'ubuntu-20.04'
           osn: 'ubuntu-20.04'
-        - os:  'macos-latest'
-          osn: 'x64-macos-11'
+        - os:  'macos-13'
+          osn: 'x64-macos-13'
         - os:  'windows-2019'
           osn: 'windows-2019'
     # There is no hosted environment for Ubuntu 14.04 or for debian

.github/workflows/runtime-tests.yml

@@ -33,12 +33,12 @@ jobs:
       - name: Set up Go
         uses: actions/setup-go@v5
         with:
-          go-version: '1.15'
+          go-version: '1.21'
           cache: false
       - name: Set up goimports
         env:
           GO111MODULE: on
-        run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+        run: go install golang.org/x/tools/cmd/goimports@latest
       - name: Build Dafny
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
@@ -48,7 +48,7 @@ jobs:
           cd ./Source/DafnyCore
           make test
           make check-format
-      - name: Test DafnyRuntime (C#)
+      - name: Test DafnyRuntime (C#, Rust)
         run: |
           cd ./Source/DafnyRuntime
           make all
@@ -72,3 +72,7 @@ jobs:
         run: |
           cd ./Source/DafnyRuntime/DafnyRuntimeJs
           make all
+      - name: Test DafnyRuntimeRust
+        run: |
+          cd ./Source/DafnyRuntime/DafnyRuntimeRust
+          make all

.github/workflows/standard-libraries.yml

@@ -17,7 +17,7 @@ jobs:
   build:
     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: macos-latest
+    runs-on: macos-13
 
     steps:
       - name: Checkout Dafny
@@ -32,12 +32,12 @@ jobs:
       - name: Set up Go
         uses: actions/setup-go@v5
         with:
-          go-version: '1.15'
+          go-version: '1.21'
           cache: false
       - name: Set up goimports
         env:
           GO111MODULE: on
-        run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+        run: go install golang.org/x/tools/cmd/goimports@latest
       - name: Build Dafny
         run: dotnet build Source/Dafny.sln
       - name: Get Z3