diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 29c8493cbc1..29c86a6c2d2 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,23 @@ See [docs/dev/news/](docs/dev/news/). +# 3.13.0 + +## New features + +- Expose non-relaxed definite assignment (`/definiteAssignment:4`) in legacy CLI (https://github.com/dafny-lang/dafny/pull/3641) + +## Bug fixes + +- Fix translation of Dafny FunctionHandles to Boogie (https://github.com/dafny-lang/dafny/pull/2266) + +- To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now. (https://github.com/dafny-lang/dafny/pull/3479) + +- Fixes to definite assignment and determinism options: + - `--enforce-determinism` now forbids constructor-less classes + - With non-relaxed definite assignment, allow auto-init fields to be uninitialized + (https://github.com/dafny-lang/dafny/pull/3641) + # 3.12.0 ## New features diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 8b31d0da3b7..ece6e185efd 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,7 +1,7 @@ - 3.12.0.50221 + 3.13.0.50302 1701;1702;VSTHRD200 diff --git a/docs/dev/news/2266.fix b/docs/dev/news/2266.fix deleted file mode 100644 index 4af9dd8f5e3..00000000000 --- a/docs/dev/news/2266.fix +++ /dev/null @@ -1 +0,0 @@ -Fix translation of Dafny FunctionHandles to Boogie diff --git a/docs/dev/news/3479.fix b/docs/dev/news/3479.fix deleted file mode 100644 index 96e3176bae2..00000000000 --- a/docs/dev/news/3479.fix +++ /dev/null @@ -1 +0,0 @@ -To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now. diff --git a/docs/dev/news/3641.feat b/docs/dev/news/3641.feat deleted file mode 100644 index 19b2576ed7e..00000000000 --- a/docs/dev/news/3641.feat +++ /dev/null @@ -1 +0,0 @@ -Expose non-relaxed definite assignment (`/definiteAssignment:4`) in legacy CLI \ No newline at end of file diff --git a/docs/dev/news/3641.fix b/docs/dev/news/3641.fix deleted file mode 100644 index b4364957e12..00000000000 --- a/docs/dev/news/3641.fix +++ /dev/null @@ -1,3 +0,0 @@ -Fixes to definite assignment and determinism options: - - `--enforce-determinism` now forbids constructor-less classes - - With non-relaxed definite assignment, allow auto-init fields to be uninitialized