From f24efae13647804624723de981bb5c95ea83e177 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 4 Feb 2025 15:15:05 -0600 Subject: [PATCH] Release Dafny 4.10.0 --- RELEASE_NOTES.md | 22 ++++++++++++++++++++++ docs/dev/news/6024.fix | 1 - docs/dev/news/6025.fix | 1 - docs/dev/news/6050.fix | 1 - docs/dev/news/6077.feat | 1 - docs/dev/news/6078.feat | 1 - docs/dev/news/code-actions.feat | 4 ---- 7 files changed, 22 insertions(+), 9 deletions(-) delete mode 100644 docs/dev/news/6024.fix delete mode 100644 docs/dev/news/6025.fix delete mode 100644 docs/dev/news/6050.fix delete mode 100644 docs/dev/news/6077.feat delete mode 100644 docs/dev/news/6078.feat delete mode 100644 docs/dev/news/code-actions.feat diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 120b43fdc6..5897bf0086 100644 --- 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 :`, also support `--filter-position :-`, `--filter-position :-` and `--filter-position :-` (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 deleted file mode 100644 index d8b3b8868e..0000000000 --- a/docs/dev/news/6024.fix +++ /dev/null @@ -1 +0,0 @@ -By clauses for assign-such-that statements (:|), are now never ignored. \ No newline at end of file diff --git a/docs/dev/news/6025.fix b/docs/dev/news/6025.fix deleted file mode 100644 index f861d68ac8..0000000000 --- a/docs/dev/news/6025.fix +++ /dev/null @@ -1 +0,0 @@ -The code action for assertion no longer suggests asserting the same assertion. \ No newline at end of file diff --git a/docs/dev/news/6050.fix b/docs/dev/news/6050.fix deleted file mode 100644 index c9e1028c8d..0000000000 --- a/docs/dev/news/6050.fix +++ /dev/null @@ -1 +0,0 @@ -Fix a bug that caused a crash when translating by blocks \ No newline at end of file diff --git a/docs/dev/news/6077.feat b/docs/dev/news/6077.feat deleted file mode 100644 index c37bfbef55..0000000000 --- a/docs/dev/news/6077.feat +++ /dev/null @@ -1 +0,0 @@ -Besides `--filter-position :`, also support `--filter-position :-`, `--filter-position :-` and `--filter-position :-` \ No newline at end of file diff --git a/docs/dev/news/6078.feat b/docs/dev/news/6078.feat deleted file mode 100644 index 5f0c9fb54f..0000000000 --- a/docs/dev/news/6078.feat +++ /dev/null @@ -1 +0,0 @@ -The options --iterations from the command `measure-complexity`, has been renamed to `--mutations`. The option `--progress VerificationJob` has been renamed to `--progress Batch`. \ No newline at end of file diff --git a/docs/dev/news/code-actions.feat b/docs/dev/news/code-actions.feat deleted file mode 100644 index 787286ffa8..0000000000 --- a/docs/dev/news/code-actions.feat +++ /dev/null @@ -1,4 +0,0 @@ -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. \ No newline at end of file