Merge branch 'master' into zulip

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

@@ -30,10 +30,10 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
         `\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. `+
+        `- 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`+
+        `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`+

.github/workflows/doc-tests.yml

@@ -32,12 +32,6 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: 8.0.x
-    # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
-    # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
-    - name: Setup dotnet
-      uses: actions/setup-dotnet@v4
-      with:
-        dotnet-version: 6.0.x
     - name: Checkout Dafny
       uses: actions/checkout@v4
       with:

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

@@ -19,7 +19,7 @@ on:
         default: ""
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   # This job is used to dynamically calculate the matrix dimensions.
@@ -72,6 +72,11 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
+    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
     - name: C++ for ubuntu 20.04
       if: matrix.os == 'ubuntu-20.04'
       run: |

.github/workflows/msbuild.yml

@@ -12,7 +12,7 @@ concurrency:
 
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   check-deep-tests:
@@ -38,6 +38,9 @@ jobs:
     - 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/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+    - name: Check that it's possible to bump the version
+      working-directory: dafny
+      run: make bumpversion-test
     - name: Get Boogie Version
       run: |
         sudo apt-get update

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

@@ -30,7 +30,7 @@ on:
         required: false
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
 

.github/workflows/publish-release.yml

@@ -7,7 +7,7 @@ on:
       - 'v*'
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   deep-integration-tests:

.github/workflows/refman.yml

@@ -28,7 +28,7 @@ jobs:
     - name: Setup dotnet
       uses: actions/setup-dotnet@v4
       with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x
     - name: Checkout Dafny
       uses: actions/checkout@v4
       with:

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

@@ -17,7 +17,7 @@ on:
   workflow_dispatch:
 
 env:
-  dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
+  dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
   z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
 
 concurrency:

.github/workflows/runtime-tests.yml

@@ -31,12 +31,6 @@ jobs:
         uses: actions/setup-dotnet@v4
         with:
           dotnet-version: 8.0.x
-      # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
-      # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
-      - name: Setup dotnet
-        uses: actions/setup-dotnet@v4
-        with:
-          dotnet-version: 6.0.x
       - name: Set up JDK 18
         uses: actions/setup-java@v4
         with:

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

@@ -73,7 +73,7 @@ jobs:
     - name: Setup .NET
       uses: actions/setup-dotnet@v4
       with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x
     - name: Install dependencies
       run: |
         dotnet restore ${{env.solutionPath}}

CONTRIBUTING.md

@@ -85,7 +85,7 @@ Subsequent CI runs should pick up the successful `deep-tests` run and make the `
 ### How can I write portions of Dafny in Dafny itself?
 
 Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files.
-The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs`
+The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net8.0/GeneratedFromDafny.cs`
 that is automatically included in the build process. This file contains also the Dafny run-time in C#.
 One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point.
 

Makefile

@@ -99,6 +99,9 @@ clean:
 	(cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
 	echo Source/*/bin Source/*/obj
 
+bumpversion-test:
+	node ./Scripts/bump_version_number.js --test 1.2.3
+
 update-cs-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module)
 

README.md

@@ -79,4 +79,4 @@ Information and instructions for potential contributors are provided [here](CONT
 
 Dafny itself is licensed under the MIT license. (See `LICENSE.txt` in the root
 directory for details.) The subdirectory `Source/Dafny/Coco` contains third
-party material; see `Source/Dafny/Coco/LICENSE.txt` for more details.
+party material; see `Source/DafnyCore/Coco/LICENSE.txt` for more details.

RELEASE_NOTES.md

@@ -2,6 +2,96 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.9.1
+
+## New features
+
+- Introduce the attributes {:isolate} and {:isolate "paths} that simplify the verification of an assertion by introducing additional verification jobs. {:isolate} can be applied to `assert`, `return` and `continue` statements. When using `{:isolate_assertions}` or `--isolate-assertions`, each return statement now creates a separate verification job for each ensures clause. Previously all ensures clauses where verified in a single job, for all return statements. (https://github.com/dafny-lang/dafny/pull/5832)
+
+- Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through. For backward compatibility, use an explicit `{:induction ...}` where `...` is the list of variables to use for the induction-hypothesis quantifier. Additionally, use a  `{:nowarn}` attribute to suppress any warning about lack of matching patterns.
+
+  Improve the selection of induction variables.
+
+  Allow codatatype equality in matching patterns and as a focal predicate for extreme predicates.
+
+  More specifically:
+
+  * If a lemma bears `{:induction x, y, z}`, where `x, y, z` is a subset of the lemma's parameters (in the same order
+     that the lemma gives them), then an induction hypothesis (IH) is generated. The IH quantifies over the
+     given variables.
+
+     For an instance-member lemma, the variables may include the implicit `this` parameter.
+
+     For an extreme lemma, the IH generated is the for corresponding prefix lemma, and the given variables may
+     include the implicit parameter `_k`.
+
+     If good matching patterns are found for the quantifier, then these are indicated in tooltips.
+     If no patterns are found, then a warning is generated; except, if the lemma bears `{:nowarn}`, then only
+     an informational message is given.
+
+  * If a lemma bears `{:induction}` or `{:induction true}`, then a list of induction variables is determined heuristically.
+
+     If the list is empty, then a warning message is generated and no IH is generated. If the list is nonempty,
+     an IH is generated and the list of variables is indicated in a tooltip.
+
+     If good matching patterns are found for the quantifier, then these are indicated in tooltips.
+     If no patterns are found, then a warning is generated; except, if the lemma bears {:nowarn}, then only
+     an informational message is given.
+
+  * If a lemma bears `{:induction false}`, then no IH is generated.
+
+  * If a lemma bears an `:induction` attribute other than those listed above, then an error is generated.
+
+  * If a lemma bears no `:induction` attribute, and the `--manual-lemma-induction` flag is present, then no IH is generated.
+
+  * Otherwise, a list of induction variables is determined heuristically.
+
+     If this list is empty, then no IH is generated and no warning/info is given.
+
+     If the list is nonempty, then the machinery looks for matching patterns for the IH quantifier. If none are
+     found, then no IH is generated.  An informational message is generated, saying which candidate variables were
+     used and saying that no matching patterns were found.
+
+     If patterns are found, then an IH is generated, the list of variables and the patterns are indicated in tooltips,
+     and the patterns are used with the IH quantifier.
+
+     The pattern search can be overriden by providing patterns explicitly using the `{:inductionTrigger}` attribute.
+     This attribute has the same syntax as the `{:trigger}` attribute.  Using an empty list of triggers restores
+     Dafny's legacy behavior (no triggers for lemma induction hypotheses).
+  (https://github.com/dafny-lang/dafny/pull/5835)
+
+- Accept `decreases to` and `nonincreases to` expressions with 0 LHSs and/or 0 RHSs, and allow parentheses to be omitted when there is 1 LHS and 1 RHS. (https://github.com/dafny-lang/dafny/pull/5891)
+
+- Allow forall statements in statement expressions (https://github.com/dafny-lang/dafny/pull/5894)
+
+- When using `--isolate-assertions` or `{:isolate_assertions}`, a separate assertion batch will be generated per pair of return statement and ensures clause. (https://github.com/dafny-lang/dafny/pull/5917)
+
+## Bug fixes
+
+- `{:only}` on members only affects verification on the current file. (https://github.com/dafny-lang/dafny/pull/5730)
+
+- Fixed a bug that caused "hide *" and "reveal *" not to work when used in statement expressions, 
+  after a variable assignment occurred in the same expression.
+  (https://github.com/dafny-lang/dafny/pull/5781)
+
+- Fix malformed Boogie in function override checks (https://github.com/dafny-lang/dafny/pull/5875)
+
+- Fix soundness issue where the verifier had assumed properties of `this` already during the first phase of a constructor (https://github.com/dafny-lang/dafny/pull/5876)
+
+- Don't assume type information before binding variables (for let expressions and named function results) (https://github.com/dafny-lang/dafny/pull/5877)
+
+- Enable using reveal statement expression inside witness expressions (https://github.com/dafny-lang/dafny/pull/5882)
+
+- Fix formatting of var by statements (https://github.com/dafny-lang/dafny/pull/5927)
+
+- Fix bugs that occur when using `{:extern}` to export members (https://github.com/dafny-lang/dafny/pull/5939)
+
+- Fixed a bug that would cause the symbol verification tasks to be done multiple times when using module refinement (https://github.com/dafny-lang/dafny/pull/5967)
+
+- Map range requires equality for enclosing type to support equality (https://github.com/dafny-lang/dafny/pull/5972)
+
+- Improved code navigation for datatype update expressions (https://github.com/dafny-lang/dafny/pull/5986)
+
 # 4.9.0
 
 ## New features