From 3574ab841256d2b07ec0f2ecb65a962c08d7bcb4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 27 Sep 2023 10:20:20 -0500 Subject: [PATCH] Release Dafny 4.3.0 --- RELEASE_NOTES.md | 102 +++++++++++++++++++++++++++++++++++ Source/Directory.Build.props | 2 +- docs/dev/news/2320.feat | 2 - docs/dev/news/3358.fix | 1 - docs/dev/news/4243.fix | 1 - docs/dev/news/4255.feat | 1 - docs/dev/news/4257.fix | 1 - docs/dev/news/4258.fix | 1 - docs/dev/news/4261.fix | 1 - docs/dev/news/4287.fix | 1 - docs/dev/news/4298.fix | 1 - docs/dev/news/4310.fix | 1 - docs/dev/news/4315.fix | 1 - docs/dev/news/4325.fix | 2 - docs/dev/news/4326.feat | 1 - docs/dev/news/4328.fix | 1 - docs/dev/news/4357.fix | 1 - docs/dev/news/4365.feat | 2 - docs/dev/news/4374.fix | 1 - docs/dev/news/4378.feat | 1 - docs/dev/news/4385.fix | 1 - docs/dev/news/4392.fix | 1 - docs/dev/news/4394.fix | 1 - docs/dev/news/4401.fix | 1 - docs/dev/news/4411.fix | 1 - docs/dev/news/4413.fix | 1 - docs/dev/news/4419.fix | 1 - docs/dev/news/4432.fix | 1 - docs/dev/news/4435.feat | 10 ---- docs/dev/news/4444.feat | 2 - docs/dev/news/4445.feat | 1 - docs/dev/news/4454.fix | 1 - docs/dev/news/4477.fix | 1 - docs/dev/news/4495.fix | 1 - docs/dev/news/4499.feat | 1 - docs/dev/news/4506.fix | 1 - docs/dev/news/4513.fix | 1 - docs/dev/news/4539.feat | 2 - docs/dev/news/4556.fix | 1 - docs/dev/news/4570.fix | 1 - 40 files changed, 103 insertions(+), 53 deletions(-) delete mode 100644 docs/dev/news/2320.feat delete mode 100644 docs/dev/news/3358.fix delete mode 100644 docs/dev/news/4243.fix delete mode 100644 docs/dev/news/4255.feat delete mode 100644 docs/dev/news/4257.fix delete mode 100644 docs/dev/news/4258.fix delete mode 100644 docs/dev/news/4261.fix delete mode 100644 docs/dev/news/4287.fix delete mode 100644 docs/dev/news/4298.fix delete mode 100644 docs/dev/news/4310.fix delete mode 100644 docs/dev/news/4315.fix delete mode 100644 docs/dev/news/4325.fix delete mode 100644 docs/dev/news/4326.feat delete mode 100644 docs/dev/news/4328.fix delete mode 100644 docs/dev/news/4357.fix delete mode 100644 docs/dev/news/4365.feat delete mode 100644 docs/dev/news/4374.fix delete mode 100644 docs/dev/news/4378.feat delete mode 100644 docs/dev/news/4385.fix delete mode 100644 docs/dev/news/4392.fix delete mode 100644 docs/dev/news/4394.fix delete mode 100644 docs/dev/news/4401.fix delete mode 100644 docs/dev/news/4411.fix delete mode 100644 docs/dev/news/4413.fix delete mode 100644 docs/dev/news/4419.fix delete mode 100644 docs/dev/news/4432.fix delete mode 100644 docs/dev/news/4435.feat delete mode 100644 docs/dev/news/4444.feat delete mode 100644 docs/dev/news/4445.feat delete mode 100644 docs/dev/news/4454.fix delete mode 100644 docs/dev/news/4477.fix delete mode 100644 docs/dev/news/4495.fix delete mode 100644 docs/dev/news/4499.feat delete mode 100644 docs/dev/news/4506.fix delete mode 100644 docs/dev/news/4513.fix delete mode 100644 docs/dev/news/4539.feat delete mode 100644 docs/dev/news/4556.fix delete mode 100644 docs/dev/news/4570.fix diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index bdc52048954..2fe1853a26f 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,108 @@ See [docs/dev/news/](docs/dev/news/). +# 4.3.0 + +## New features + +- Add support for the Find References LSP request + - Returned references may be incomplete when not using project mode + (https://github.com/dafny-lang/dafny/pull/2320) + +- Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source (https://github.com/dafny-lang/dafny/pull/4255) + +- Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) (https://github.com/dafny-lang/dafny/pull/4326) + +- Add support for Rename LSP request + - Support requires enabling project mode and defining a Dafny project file + (https://github.com/dafny-lang/dafny/pull/4365) + +- Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. (https://github.com/dafny-lang/dafny/pull/4378) + +- The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a `dfyconfig.toml` can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A `dfyconfig.toml` can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the `dfyconfig.toml` resides. Project related features of the IDE are: + - Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly. + - If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed. + - The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file. + - The assisted rename feature (also added in this release), only works for files that are part of a project. + - When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found. + - If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly. + - The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file. + + Try out the IDE's project support now by creating an empty `dfyconfig.toml` file in the root of your project repository. + (https://github.com/dafny-lang/dafny/pull/4435) + +- Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes. + Any such issues are reported to the user. + (https://github.com/dafny-lang/dafny/pull/4444) + +- Added documentation of the generate-tests command to the reference manual (https://github.com/dafny-lang/dafny/pull/4445) + +- When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. (https://github.com/dafny-lang/dafny/pull/4499) + +- - The Dafny IDE will now report errors that occur in project files. + - The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project. + (https://github.com/dafny-lang/dafny/pull/4539) + +## Bug fixes + +- Triggers warnings correclty converted into errors with --warn-as-errors (https://github.com/dafny-lang/dafny/pull/3358) + +- Allow JavaScript keywords as names of Dafny modules (https://github.com/dafny-lang/dafny/pull/4243) + +- Support odd characters in pathnames for Go (https://github.com/dafny-lang/dafny/pull/4257) + +- Allow Dafny filenames compiled to Java to start with a digit (https://github.com/dafny-lang/dafny/pull/4258) + +- Parser now supports files with a lot of consecutive single-line comments (https://github.com/dafny-lang/dafny/pull/4261) + +- Gutter icons more robust (https://github.com/dafny-lang/dafny/pull/4287) + +- Unresolved abstract imports no longer crash the resolver (https://github.com/dafny-lang/dafny/pull/4298) + +- Make capitalization of target Go code consistent (https://github.com/dafny-lang/dafny/pull/4310) + +- Refining an abstract module with a class with an opaque function no longer crashes (https://github.com/dafny-lang/dafny/pull/4315) + +- Dafny can now produce coverage reports indicating which parts of the program are expected to be covered by automatically generated tests. + The same functionality can be used to report other forms of coverage. + (https://github.com/dafny-lang/dafny/pull/4325) + +- Fix issue that would prevent the IDE from correctly handling default export sets (https://github.com/dafny-lang/dafny/pull/4328) + +- Allow function-syntax and other options with a custom default to be overridden in `dfyconfig.toml` (https://github.com/dafny-lang/dafny/pull/4357) + +- There were two differences between verification in the IDE and the CLI, one small and one tiny, which would only become apparent for proofs that Z3 had trouble verifying. The small difference has been resolved, while the tiny one still persists, so the IDE and CLI should behave almost equivalently now, including resource counts, on most code. (https://github.com/dafny-lang/dafny/pull/4374) + +- Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests (https://github.com/dafny-lang/dafny/pull/4385) + +- Fixed a bug leading to stack overflow during counterexample extraction on some programs. (https://github.com/dafny-lang/dafny/pull/4392) + +- Ability to use .Key as a constant name in datatypes and classes (https://github.com/dafny-lang/dafny/pull/4394) + +- Existential assertions are now printed correctly (https://github.com/dafny-lang/dafny/pull/4401) + +- When a symbol such as a method is not given a name, the error given by Dafny now shows where this problem occurs. (https://github.com/dafny-lang/dafny/pull/4411) + +- Fix flickering and incorrect results in the verification status bar, and improve responsiveness of verification diagnostics (https://github.com/dafny-lang/dafny/pull/4413) + +- Significantly improve IDE responsiveness for large projects, preventing it from appearing unresponsive or incorrect. Previously, for projects of a certain size, the IDE would not be able to keep up with incoming changes made by the user, possibly causing it to never catch up and appearing frozen or showing outdated results. (https://github.com/dafny-lang/dafny/pull/4419) + +- Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons (https://github.com/dafny-lang/dafny/pull/4432) + +- Fix issues that could cause the IDE status bar to show incorrect information (https://github.com/dafny-lang/dafny/pull/4454) + +- When verification times out, only show a red underline on the name of the verifiable for which verification timed out, instead of under its whole definition. (https://github.com/dafny-lang/dafny/pull/4477) + +- Prevent the IDE from becoming completely unresponsive after certain kinds of parse errors would occur. (https://github.com/dafny-lang/dafny/pull/4495) + +- Support all types of options in the Dafny project file (dfyconfig.toml) (https://github.com/dafny-lang/dafny/pull/4506) + +- Fix an issue that would cause some types of errors and other diagnostics not to appear in the IDE, if they appeared in files other than the active one. (https://github.com/dafny-lang/dafny/pull/4513) + +- Fix an IDE issue that would lead to exceptions when using module export declarations and making edits in imported modules that were re-exported (https://github.com/dafny-lang/dafny/pull/4556) + +- Fix a leak in the IDE that would cause it to become less responsive over time. (https://github.com/dafny-lang/dafny/pull/4570) + # 4.2.0 ## New features diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index fd4a1e1f852..d05a3382043 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,7 +1,7 @@ - 4.2.0 + 4.3.0 1701;1702;VSTHRD200 diff --git a/docs/dev/news/2320.feat b/docs/dev/news/2320.feat deleted file mode 100644 index a465357fbe9..00000000000 --- a/docs/dev/news/2320.feat +++ /dev/null @@ -1,2 +0,0 @@ -Add support for the Find References LSP request -- Returned references may be incomplete when not using project mode diff --git a/docs/dev/news/3358.fix b/docs/dev/news/3358.fix deleted file mode 100644 index 67d30d4f38d..00000000000 --- a/docs/dev/news/3358.fix +++ /dev/null @@ -1 +0,0 @@ -Triggers warnings correclty converted into errors with --warn-as-errors \ No newline at end of file diff --git a/docs/dev/news/4243.fix b/docs/dev/news/4243.fix deleted file mode 100644 index 2d1ac90107d..00000000000 --- a/docs/dev/news/4243.fix +++ /dev/null @@ -1 +0,0 @@ -Allow JavaScript keywords as names of Dafny modules diff --git a/docs/dev/news/4255.feat b/docs/dev/news/4255.feat deleted file mode 100644 index 002430b1fa8..00000000000 --- a/docs/dev/news/4255.feat +++ /dev/null @@ -1 +0,0 @@ -Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source \ No newline at end of file diff --git a/docs/dev/news/4257.fix b/docs/dev/news/4257.fix deleted file mode 100644 index 9ffc1cc4a24..00000000000 --- a/docs/dev/news/4257.fix +++ /dev/null @@ -1 +0,0 @@ -Support odd characters in pathnames for Go diff --git a/docs/dev/news/4258.fix b/docs/dev/news/4258.fix deleted file mode 100644 index b062aa55795..00000000000 --- a/docs/dev/news/4258.fix +++ /dev/null @@ -1 +0,0 @@ -Allow Dafny filenames compiled to Java to start with a digit diff --git a/docs/dev/news/4261.fix b/docs/dev/news/4261.fix deleted file mode 100644 index 7f496bc65fc..00000000000 --- a/docs/dev/news/4261.fix +++ /dev/null @@ -1 +0,0 @@ -Parser now supports files with a lot of consecutive single-line comments \ No newline at end of file diff --git a/docs/dev/news/4287.fix b/docs/dev/news/4287.fix deleted file mode 100644 index d2e0b16b991..00000000000 --- a/docs/dev/news/4287.fix +++ /dev/null @@ -1 +0,0 @@ -Gutter icons more robust \ No newline at end of file diff --git a/docs/dev/news/4298.fix b/docs/dev/news/4298.fix deleted file mode 100644 index 91fc07fe391..00000000000 --- a/docs/dev/news/4298.fix +++ /dev/null @@ -1 +0,0 @@ -Unresolved abstract imports no longer crash the resolver \ No newline at end of file diff --git a/docs/dev/news/4310.fix b/docs/dev/news/4310.fix deleted file mode 100644 index a3269be4dc3..00000000000 --- a/docs/dev/news/4310.fix +++ /dev/null @@ -1 +0,0 @@ -Make capitalization of target Go code consistent diff --git a/docs/dev/news/4315.fix b/docs/dev/news/4315.fix deleted file mode 100644 index b3713be658a..00000000000 --- a/docs/dev/news/4315.fix +++ /dev/null @@ -1 +0,0 @@ -Refining an abstract module with a class with an opaque function no longer crashes \ No newline at end of file diff --git a/docs/dev/news/4325.fix b/docs/dev/news/4325.fix deleted file mode 100644 index 8cc59e5e01c..00000000000 --- a/docs/dev/news/4325.fix +++ /dev/null @@ -1,2 +0,0 @@ -Dafny can now produce coverage reports indicating which parts of the program are expected to be covered by automatically generated tests. -The same functionality can be used to report other forms of coverage. \ No newline at end of file diff --git a/docs/dev/news/4326.feat b/docs/dev/news/4326.feat deleted file mode 100644 index fb7b7d19b4d..00000000000 --- a/docs/dev/news/4326.feat +++ /dev/null @@ -1 +0,0 @@ -Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) \ No newline at end of file diff --git a/docs/dev/news/4328.fix b/docs/dev/news/4328.fix deleted file mode 100644 index e141e73a96b..00000000000 --- a/docs/dev/news/4328.fix +++ /dev/null @@ -1 +0,0 @@ -Fix issue that would prevent the IDE from correctly handling default export sets \ No newline at end of file diff --git a/docs/dev/news/4357.fix b/docs/dev/news/4357.fix deleted file mode 100644 index 6aea8c19cb9..00000000000 --- a/docs/dev/news/4357.fix +++ /dev/null @@ -1 +0,0 @@ -Allow function-syntax and other options with a custom default to be overridden in `dfyconfig.toml` \ No newline at end of file diff --git a/docs/dev/news/4365.feat b/docs/dev/news/4365.feat deleted file mode 100644 index 2fbb47a518e..00000000000 --- a/docs/dev/news/4365.feat +++ /dev/null @@ -1,2 +0,0 @@ -Add support for Rename LSP request -- Support requires enabling project mode and defining a Dafny project file diff --git a/docs/dev/news/4374.fix b/docs/dev/news/4374.fix deleted file mode 100644 index 7d37d080d83..00000000000 --- a/docs/dev/news/4374.fix +++ /dev/null @@ -1 +0,0 @@ -There were two differences between verification in the IDE and the CLI, one small and one tiny, which would only become apparent for proofs that Z3 had trouble verifying. The small difference has been resolved, while the tiny one still persists, so the IDE and CLI should behave almost equivalently now, including resource counts, on most code. \ No newline at end of file diff --git a/docs/dev/news/4378.feat b/docs/dev/news/4378.feat deleted file mode 100644 index 74f02907633..00000000000 --- a/docs/dev/news/4378.feat +++ /dev/null @@ -1 +0,0 @@ -Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. \ No newline at end of file diff --git a/docs/dev/news/4385.fix b/docs/dev/news/4385.fix deleted file mode 100644 index 6b581df269c..00000000000 --- a/docs/dev/news/4385.fix +++ /dev/null @@ -1 +0,0 @@ -Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests \ No newline at end of file diff --git a/docs/dev/news/4392.fix b/docs/dev/news/4392.fix deleted file mode 100644 index 0f7257f0ae3..00000000000 --- a/docs/dev/news/4392.fix +++ /dev/null @@ -1 +0,0 @@ -Fixed a bug leading to stack overflow during counterexample extraction on some programs. \ No newline at end of file diff --git a/docs/dev/news/4394.fix b/docs/dev/news/4394.fix deleted file mode 100644 index 2b35bca5c9f..00000000000 --- a/docs/dev/news/4394.fix +++ /dev/null @@ -1 +0,0 @@ -Ability to use .Key as a constant name in datatypes and classes \ No newline at end of file diff --git a/docs/dev/news/4401.fix b/docs/dev/news/4401.fix deleted file mode 100644 index 35425c7925f..00000000000 --- a/docs/dev/news/4401.fix +++ /dev/null @@ -1 +0,0 @@ -Existential assertions are now printed correctly \ No newline at end of file diff --git a/docs/dev/news/4411.fix b/docs/dev/news/4411.fix deleted file mode 100644 index e1d7f914b52..00000000000 --- a/docs/dev/news/4411.fix +++ /dev/null @@ -1 +0,0 @@ -When a symbol such as a method is not given a name, the error given by Dafny now shows where this problem occurs. \ No newline at end of file diff --git a/docs/dev/news/4413.fix b/docs/dev/news/4413.fix deleted file mode 100644 index 009b24f19b4..00000000000 --- a/docs/dev/news/4413.fix +++ /dev/null @@ -1 +0,0 @@ -Fix flickering and incorrect results in the verification status bar, and improve responsiveness of verification diagnostics \ No newline at end of file diff --git a/docs/dev/news/4419.fix b/docs/dev/news/4419.fix deleted file mode 100644 index 10b6526137a..00000000000 --- a/docs/dev/news/4419.fix +++ /dev/null @@ -1 +0,0 @@ -Significantly improve IDE responsiveness for large projects, preventing it from appearing unresponsive or incorrect. Previously, for projects of a certain size, the IDE would not be able to keep up with incoming changes made by the user, possibly causing it to never catch up and appearing frozen or showing outdated results. \ No newline at end of file diff --git a/docs/dev/news/4432.fix b/docs/dev/news/4432.fix deleted file mode 100644 index 7bc34797500..00000000000 --- a/docs/dev/news/4432.fix +++ /dev/null @@ -1 +0,0 @@ -Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons \ No newline at end of file diff --git a/docs/dev/news/4435.feat b/docs/dev/news/4435.feat deleted file mode 100644 index 1abaa28654e..00000000000 --- a/docs/dev/news/4435.feat +++ /dev/null @@ -1,10 +0,0 @@ -The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a `dfyconfig.toml` can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A `dfyconfig.toml` can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the `dfyconfig.toml` resides. Project related features of the IDE are: -- Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly. -- If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed. -- The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file. -- The assisted rename feature (also added in this release), only works for files that are part of a project. -- When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found. -- If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly. -- The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file. - -Try out the IDE's project support now by creating an empty `dfyconfig.toml` file in the root of your project repository. \ No newline at end of file diff --git a/docs/dev/news/4444.feat b/docs/dev/news/4444.feat deleted file mode 100644 index 4c083c398e5..00000000000 --- a/docs/dev/news/4444.feat +++ /dev/null @@ -1,2 +0,0 @@ -Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes. -Any such issues are reported to the user. \ No newline at end of file diff --git a/docs/dev/news/4445.feat b/docs/dev/news/4445.feat deleted file mode 100644 index 63eb0570c96..00000000000 --- a/docs/dev/news/4445.feat +++ /dev/null @@ -1 +0,0 @@ -Added documentation of the generate-tests command to the reference manual diff --git a/docs/dev/news/4454.fix b/docs/dev/news/4454.fix deleted file mode 100644 index 860ee63ca32..00000000000 --- a/docs/dev/news/4454.fix +++ /dev/null @@ -1 +0,0 @@ -Fix issues that could cause the IDE status bar to show incorrect information \ No newline at end of file diff --git a/docs/dev/news/4477.fix b/docs/dev/news/4477.fix deleted file mode 100644 index 9829073a45c..00000000000 --- a/docs/dev/news/4477.fix +++ /dev/null @@ -1 +0,0 @@ -When verification times out, only show a red underline on the name of the verifiable for which verification timed out, instead of under its whole definition. \ No newline at end of file diff --git a/docs/dev/news/4495.fix b/docs/dev/news/4495.fix deleted file mode 100644 index f2835cabcc2..00000000000 --- a/docs/dev/news/4495.fix +++ /dev/null @@ -1 +0,0 @@ -Prevent the IDE from becoming completely unresponsive after certain kinds of parse errors would occur. \ No newline at end of file diff --git a/docs/dev/news/4499.feat b/docs/dev/news/4499.feat deleted file mode 100644 index f95c09227b6..00000000000 --- a/docs/dev/news/4499.feat +++ /dev/null @@ -1 +0,0 @@ -When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. \ No newline at end of file diff --git a/docs/dev/news/4506.fix b/docs/dev/news/4506.fix deleted file mode 100644 index abf29f7417e..00000000000 --- a/docs/dev/news/4506.fix +++ /dev/null @@ -1 +0,0 @@ -Support all types of options in the Dafny project file (dfyconfig.toml) \ No newline at end of file diff --git a/docs/dev/news/4513.fix b/docs/dev/news/4513.fix deleted file mode 100644 index 0f093b437f4..00000000000 --- a/docs/dev/news/4513.fix +++ /dev/null @@ -1 +0,0 @@ -Fix an issue that would cause some types of errors and other diagnostics not to appear in the IDE, if they appeared in files other than the active one. \ No newline at end of file diff --git a/docs/dev/news/4539.feat b/docs/dev/news/4539.feat deleted file mode 100644 index edb63f079ed..00000000000 --- a/docs/dev/news/4539.feat +++ /dev/null @@ -1,2 +0,0 @@ -- The Dafny IDE will now report errors that occur in project files. -- The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project. \ No newline at end of file diff --git a/docs/dev/news/4556.fix b/docs/dev/news/4556.fix deleted file mode 100644 index f5930e43380..00000000000 --- a/docs/dev/news/4556.fix +++ /dev/null @@ -1 +0,0 @@ -Fix an IDE issue that would lead to exceptions when using module export declarations and making edits in imported modules that were re-exported \ No newline at end of file diff --git a/docs/dev/news/4570.fix b/docs/dev/news/4570.fix deleted file mode 100644 index ce369f77e89..00000000000 --- a/docs/dev/news/4570.fix +++ /dev/null @@ -1 +0,0 @@ -Fix a leak in the IDE that would cause it to become less responsive over time. \ No newline at end of file