diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f9ee0efba9..a934cb41aa 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,113 @@ See [docs/dev/news/](docs/dev/news/). +# 4.7.0 + +## New features + +- Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow. + +- Improved error reporting when verification times out or runs out of resources, so that when using `--isolate-assertions`, the error message points to the problematic assertion. (https://github.com/dafny-lang/dafny/pull/5281) + +- Support newtypes based on map and imap (https://github.com/dafny-lang/dafny/pull/5175) + +- To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. When using `dafny verify`, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag `--dont-verify-dependencies`. (https://github.com/dafny-lang/dafny/pull/5297) + +- Experimental Dafny-to-Rust compiler development + - Supports emitting code even if malformed with option `--emit-uncompilable-code`. + - Supports for immutable collections and operators + (https://github.com/dafny-lang/dafny/pull/5081) + +- Allow for plugins to add custom request handlers to the language server. (https://github.com/dafny-lang/dafny/pull/5161) + +- Deprecated the unicode-char option (https://github.com/dafny-lang/dafny/pull/5302) + +- Warn when passing a Dafny source file to `--library` (https://github.com/dafny-lang/dafny/pull/5313) + +- Add support for "translation records", which record the options used when translating library code. + * `--translation-record` - Provides a `.dtr` file from a previous translation of library code. Can be specified multiple times. + * `--translation-record-output` - Customizes where to write the translation record for the current translation. Defaults to the output directory. + Providing translation records is necessary to handle options such as `--outer-module` that affect how code is translated. + (https://github.com/dafny-lang/dafny/pull/5346) + +- The new `decreases to` expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (https://github.com/dafny-lang/dafny/pull/5367) + +- The new `assigned` expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (https://github.com/dafny-lang/dafny/pull/5501) + +- Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript. + +- Introduce additional warnings that previously only appeared when running the `dafny audit` command. Two warnings are as follows: + - Emit a warning when exporting a declaration that has requires clauses or subset type inputs + - Emit a warning when importing a declaration that has ensures clauses or subset type outputs +Those two can be silenced with the flag `--allow-external-contracts`. A third new warning occurs when using bodyless functions marked with `{:extern}`, and can be silenced using the option `--allow-external-function`. + +- Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual. + +## Bug fixes + +- Fix a common memory leak that occurred when doing verification in the IDE that could easily consume gigabytes of memory. + +- Fix bugs that could cause the IDE to become unresponsive + +- Improve the performance of the Dafny IDE by fixing bugs in its caching code + +- No longer reuse SMT solver processes between different document version when using the IDE, making the IDE verification behavior more inline to that of the CLI + +- Fix bugs that caused Dafny IDE internal errors (https://github.com/dafny-lang/dafny/issues/5355, https://github.com/dafny-lang/dafny/pull/5543, https://github.com/dafny-lang/dafny/pull/5548) + +- Fix bugs in the Dafny IDEs code navigation and renaming features when working with definition that are not referred to. + +- Fix a code navigation bug that could occur when navigating to and from module imports +- +- Fix a code navigation bug that could occur when navigating to and from explicit types of variables + (https://github.com/dafny-lang/dafny/pull/5419) + +- Let the IDE no longer show diagnostics for projects for which all files have been closed (https://github.com/dafny-lang/dafny/pull/5437) + +- Fix bug that could lead to an unresponsive IDE when working with project files (https://github.com/dafny-lang/dafny/pull/5444) + +- Fix bugs in Dafny library files that could cause them not to work with certain option values, such as --function-syntax=3 + +- Fix a bug that prevented building Dafny libraries for Dafny projects that could verify without errors. + +- Reserved module identifiers correctly escaped in GoLang (https://github.com/dafny-lang/dafny/pull/4181) + +- Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor (https://github.com/dafny-lang/dafny/pull/4700) + +- Ability to cast a datatype to its trait when overriding functions (https://github.com/dafny-lang/dafny/pull/4823) + +- Fix crash that could occur when using a constructor in a match pattern where a tuple was expected (https://github.com/dafny-lang/dafny/pull/4860) + +- No longer emit an incorrect internal error while waiting for verification message (https://github.com/dafny-lang/dafny/pull/5209) + +- More helpful error messages when read fields not mentioned in reads clauses (https://github.com/dafny-lang/dafny/pull/5262) + +- Check datatype constructors for bad type-parameter instantiations (https://github.com/dafny-lang/dafny/pull/5278) + +- Avoid name clashes with Go built-in modules (https://github.com/dafny-lang/dafny/pull/5283) + +- Invalid Python code for nested set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5287) + +- Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" (https://github.com/dafny-lang/dafny/pull/5295) + +- Rename the `dafny generate-tests` option `--coverage-report` to `--expected-coverage-report` (https://github.com/dafny-lang/dafny/pull/5301) + +- Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant. (https://github.com/dafny-lang/dafny/pull/5306) + +- No new resolver crash when datatype update expressions are partially resolved (https://github.com/dafny-lang/dafny/pull/5331) + +- Optional pre-type won't cause a crash anymore (https://github.com/dafny-lang/dafny/pull/5369) + +- Unguarded enumeration of bound variables in set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5402) + +- Reference the correct `this` after removing the tail call of a function or method (https://github.com/dafny-lang/dafny/pull/5474) + +- Apply name mangling to datatype names in Python more often (https://github.com/dafny-lang/dafny/pull/5476) + +- Only guard `this` when eliminating tail calls, if possible (https://github.com/dafny-lang/dafny/pull/5524) + +- Compiled disjunctive nested pattern matching no longer crashing (https://github.com/dafny-lang/dafny/pull/5572) + # 4.6.0 ## New features diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index d242d9b4fb..7a84fbde9b 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,7 +1,7 @@ - 4.6.0 + 4.7.0 1701;1702;VSTHRD200 diff --git a/docs/dev/news/4181.fix b/docs/dev/news/4181.fix deleted file mode 100644 index 2678836452..0000000000 --- a/docs/dev/news/4181.fix +++ /dev/null @@ -1 +0,0 @@ -Reserved module identifiers correctly escaped in GoLang \ No newline at end of file diff --git a/docs/dev/news/4700.fix b/docs/dev/news/4700.fix deleted file mode 100644 index 1f3b18c390..0000000000 --- a/docs/dev/news/4700.fix +++ /dev/null @@ -1 +0,0 @@ -Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor \ No newline at end of file diff --git a/docs/dev/news/4823.fix b/docs/dev/news/4823.fix deleted file mode 100644 index 400cee8379..0000000000 --- a/docs/dev/news/4823.fix +++ /dev/null @@ -1 +0,0 @@ -Ability to cast a datatype to its trait when overriding functions \ No newline at end of file diff --git a/docs/dev/news/4860.fix b/docs/dev/news/4860.fix deleted file mode 100644 index 203070a340..0000000000 --- a/docs/dev/news/4860.fix +++ /dev/null @@ -1 +0,0 @@ -- Fix crash that could occur when using a constructor in a match pattern where a tuple was expected \ No newline at end of file diff --git a/docs/dev/news/5081.feat b/docs/dev/news/5081.feat deleted file mode 100644 index 72b1026481..0000000000 --- a/docs/dev/news/5081.feat +++ /dev/null @@ -1,3 +0,0 @@ -Experimental Dafny-to-Rust compiler development -- Supports emitting code even if malformed with option `--emit-uncompilable-code`. -- Supports for immutable collections and operators \ No newline at end of file diff --git a/docs/dev/news/5161.feat b/docs/dev/news/5161.feat deleted file mode 100644 index 6072644e4b..0000000000 --- a/docs/dev/news/5161.feat +++ /dev/null @@ -1 +0,0 @@ -Allow for plugins to add custom request handlers to the language server. \ No newline at end of file diff --git a/docs/dev/news/5175.feat b/docs/dev/news/5175.feat deleted file mode 100644 index 66ab4044b0..0000000000 --- a/docs/dev/news/5175.feat +++ /dev/null @@ -1 +0,0 @@ -Support newtypes based on map and imap diff --git a/docs/dev/news/5209.fix b/docs/dev/news/5209.fix deleted file mode 100644 index 0ed141d88c..0000000000 --- a/docs/dev/news/5209.fix +++ /dev/null @@ -1 +0,0 @@ -No longer emit an incorrect internal error while waiting for verification message \ No newline at end of file diff --git a/docs/dev/news/5247.feat b/docs/dev/news/5247.feat deleted file mode 100644 index b203266de2..0000000000 --- a/docs/dev/news/5247.feat +++ /dev/null @@ -1 +0,0 @@ -Add the attribute `{:isolate_assertions}`, which does the same as `{:vcs_split_on_every_assert}`. Deprecated `{:vcs_split_on_every_assert}` \ No newline at end of file diff --git a/docs/dev/news/5262.fix b/docs/dev/news/5262.fix deleted file mode 100644 index 07d10bb16f..0000000000 --- a/docs/dev/news/5262.fix +++ /dev/null @@ -1 +0,0 @@ -More helpful error messages when read fields not mentioned in reads clauses \ No newline at end of file diff --git a/docs/dev/news/5278.fix b/docs/dev/news/5278.fix deleted file mode 100644 index 0252a1f02c..0000000000 --- a/docs/dev/news/5278.fix +++ /dev/null @@ -1 +0,0 @@ -Check datatype constructors for bad type-parameter instantiations diff --git a/docs/dev/news/5281.feat b/docs/dev/news/5281.feat deleted file mode 100644 index 1eacc1e782..0000000000 --- a/docs/dev/news/5281.feat +++ /dev/null @@ -1 +0,0 @@ -Improved error reporting when verification times out or runs out of resources, so that when using `--isolate-assertions`, the error message points to the problematic assertion. \ No newline at end of file diff --git a/docs/dev/news/5283.fix b/docs/dev/news/5283.fix deleted file mode 100644 index 4abb60d9fa..0000000000 --- a/docs/dev/news/5283.fix +++ /dev/null @@ -1 +0,0 @@ -Avoid name clashes with Go built-in modules diff --git a/docs/dev/news/5287.fix b/docs/dev/news/5287.fix deleted file mode 100644 index a2ec230054..0000000000 --- a/docs/dev/news/5287.fix +++ /dev/null @@ -1 +0,0 @@ -Invalid Python code for nested set and map comprehensions diff --git a/docs/dev/news/5295.fix b/docs/dev/news/5295.fix deleted file mode 100644 index 410408824c..0000000000 --- a/docs/dev/news/5295.fix +++ /dev/null @@ -1 +0,0 @@ -Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" \ No newline at end of file diff --git a/docs/dev/news/5297.feat b/docs/dev/news/5297.feat deleted file mode 100644 index d058ac5e79..0000000000 --- a/docs/dev/news/5297.feat +++ /dev/null @@ -1 +0,0 @@ -- To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. This first ensures that the defined Dafny project is built. Once it is built, Dafny will use the library file from that build as if it was passed to `--library`. \ No newline at end of file diff --git a/docs/dev/news/5301.fix b/docs/dev/news/5301.fix deleted file mode 100644 index 708a1579e4..0000000000 --- a/docs/dev/news/5301.fix +++ /dev/null @@ -1 +0,0 @@ -Rename the `dafny generate-tests` option `--coverage-report` to `--expected-coverage-report` \ No newline at end of file diff --git a/docs/dev/news/5302.feat b/docs/dev/news/5302.feat deleted file mode 100644 index ac20c5b4ed..0000000000 --- a/docs/dev/news/5302.feat +++ /dev/null @@ -1 +0,0 @@ -Deprecated the unicode-char option \ No newline at end of file diff --git a/docs/dev/news/5306.fix b/docs/dev/news/5306.fix deleted file mode 100644 index 889b1680ae..0000000000 --- a/docs/dev/news/5306.fix +++ /dev/null @@ -1 +0,0 @@ -Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant. \ No newline at end of file diff --git a/docs/dev/news/5313.feat b/docs/dev/news/5313.feat deleted file mode 100644 index 0d86b37826..0000000000 --- a/docs/dev/news/5313.feat +++ /dev/null @@ -1 +0,0 @@ -- Warn when passing a Dafny source file to `--library` \ No newline at end of file diff --git a/docs/dev/news/5331.fix b/docs/dev/news/5331.fix deleted file mode 100644 index b5945244ab..0000000000 --- a/docs/dev/news/5331.fix +++ /dev/null @@ -1 +0,0 @@ -No new resolver crash when datatype update expressions are partially resolved \ No newline at end of file diff --git a/docs/dev/news/5346.feat b/docs/dev/news/5346.feat deleted file mode 100644 index 92fed52249..0000000000 --- a/docs/dev/news/5346.feat +++ /dev/null @@ -1,4 +0,0 @@ -Add support for "translation records", which record the options used when translating library code. -* `--translation-record` - Provides a `.dtr` file from a previous translation of library code. Can be specified multiple times. -* `--translation-record-output` - Customizes where to write the translation record for the current translation. Defaults to the output directory. -Providing translation records is necessary to handle options such as `--outer-module` that affect how code is translated. diff --git a/docs/dev/news/5367.feat b/docs/dev/news/5367.feat deleted file mode 100644 index bd30270228..0000000000 --- a/docs/dev/news/5367.feat +++ /dev/null @@ -1 +0,0 @@ -The new `decreases to` expression makes it possible to write an explict assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. diff --git a/docs/dev/news/5369.fix b/docs/dev/news/5369.fix deleted file mode 100644 index 0f120ee253..0000000000 --- a/docs/dev/news/5369.fix +++ /dev/null @@ -1 +0,0 @@ -Optional pre-type won't cause a crash anymore \ No newline at end of file diff --git a/docs/dev/news/5402.fix b/docs/dev/news/5402.fix deleted file mode 100644 index b61bf73db3..0000000000 --- a/docs/dev/news/5402.fix +++ /dev/null @@ -1 +0,0 @@ -Unguarded enumeration of bound variables in set and map comprehensions \ No newline at end of file diff --git a/docs/dev/news/5419.fix b/docs/dev/news/5419.fix deleted file mode 100644 index 352950c6b5..0000000000 --- a/docs/dev/news/5419.fix +++ /dev/null @@ -1,2 +0,0 @@ -- Fix a code navigation bug that could occur when navigating to and from module imports -- Fix a code navigation bug that could occur when navigating to and from explicit types of variables \ No newline at end of file diff --git a/docs/dev/news/5437.fix b/docs/dev/news/5437.fix deleted file mode 100644 index 0d0e15245b..0000000000 --- a/docs/dev/news/5437.fix +++ /dev/null @@ -1 +0,0 @@ -- Let the IDE no longer show diagnostics for projects for which all files have been closed \ No newline at end of file diff --git a/docs/dev/news/5444.fix b/docs/dev/news/5444.fix deleted file mode 100644 index fd5b902e63..0000000000 --- a/docs/dev/news/5444.fix +++ /dev/null @@ -1 +0,0 @@ -- Fix bug that could lead to an unresponsive IDE when working with project files \ No newline at end of file diff --git a/docs/dev/news/5474.fix b/docs/dev/news/5474.fix deleted file mode 100644 index 05ede052c9..0000000000 --- a/docs/dev/news/5474.fix +++ /dev/null @@ -1 +0,0 @@ -Reference the correct `this` after removing the tail call of a function or method diff --git a/docs/dev/news/5476.fix b/docs/dev/news/5476.fix deleted file mode 100644 index 156ae3c64f..0000000000 --- a/docs/dev/news/5476.fix +++ /dev/null @@ -1 +0,0 @@ -Apply name mangling to datatype names in Python more often diff --git a/docs/dev/news/5501.feat b/docs/dev/news/5501.feat deleted file mode 100644 index 1cc889990a..0000000000 --- a/docs/dev/news/5501.feat +++ /dev/null @@ -1 +0,0 @@ -The new `assigned` expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. \ No newline at end of file diff --git a/docs/dev/news/5524.fix b/docs/dev/news/5524.fix deleted file mode 100644 index 3c4e5dfcae..0000000000 --- a/docs/dev/news/5524.fix +++ /dev/null @@ -1 +0,0 @@ -Only guard `this` when eliminating tail calls, if possible \ No newline at end of file diff --git a/docs/dev/news/5572.fix b/docs/dev/news/5572.fix deleted file mode 100644 index fb0a662697..0000000000 --- a/docs/dev/news/5572.fix +++ /dev/null @@ -1 +0,0 @@ -Compiled disjunctive nested pattern matching no longer crashing \ No newline at end of file