Release Dafny 4.10.0

dafny-lang · Feb 4, 2025 · f24efae · f24efae
1 parent 6cb34c1
commit f24efae
Show file tree

Hide file tree

Showing 7 changed files with 22 additions and 9 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -2,6 +2,28 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.10.0
+
+## New features
+
+- Support for code actions in the language server to:
+  - Insert failing implicit assertions in a "by" clause by preference.
+  - Insert forall statement for any forall expressions that could not be proved
+  - Insert calc statement for any equality that cannot be proved.
+  (https://github.com/dafny-lang/dafny/pull/6044)
+
+- Besides `--filter-position :<line>`, also support `--filter-position :<start>-<end>`, `--filter-position :<start>-` and `--filter-position :-<end>` (https://github.com/dafny-lang/dafny/pull/6077)
+
+- The options --iterations from the command `measure-complexity`, has been renamed to `--mutations`. The option `--progress VerificationJob` has been renamed to `--progress Batch`. (https://github.com/dafny-lang/dafny/pull/6078)
+
+## Bug fixes
+
+- By clauses for assign-such-that statements (:|), are now never ignored. (https://github.com/dafny-lang/dafny/pull/6024)
+
+- The code action for assertion no longer suggests asserting the same assertion. (https://github.com/dafny-lang/dafny/pull/6025)
+
+- Fix a bug that caused a crash when translating by blocks (https://github.com/dafny-lang/dafny/pull/6050)
+
 # 4.9.1
 
 ## New features

diff --git a/docs/dev/news/6024.fix b/docs/dev/news/6024.fix
diff --git a/docs/dev/news/6025.fix b/docs/dev/news/6025.fix
diff --git a/docs/dev/news/6050.fix b/docs/dev/news/6050.fix
diff --git a/docs/dev/news/6077.feat b/docs/dev/news/6077.feat
diff --git a/docs/dev/news/6078.feat b/docs/dev/news/6078.feat
diff --git a/docs/dev/news/code-actions.feat b/docs/dev/news/code-actions.feat