From 7c82175da631d3fdc3acea92a3614d66a3fdf7f2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 28 Mar 2024 06:30:01 -0700 Subject: [PATCH] Release Dafny 4.6.0 --- RELEASE_NOTES.md | 24 ++++++++++++++++++++++++ docs/dev/news/4844.fix | 1 - docs/dev/news/5097.feat | 1 - docs/dev/news/5146.fix | 1 - docs/dev/news/5150.feat | 1 - docs/dev/news/5176.fix | 1 - docs/dev/news/5234.fix | 2 -- docs/dev/news/5239.fix | 1 - docs/dev/news/5247.feat | 1 - 9 files changed, 24 insertions(+), 9 deletions(-) delete mode 100644 docs/dev/news/4844.fix delete mode 100644 docs/dev/news/5097.feat delete mode 100644 docs/dev/news/5146.fix delete mode 100644 docs/dev/news/5150.feat delete mode 100644 docs/dev/news/5176.fix delete mode 100644 docs/dev/news/5234.fix delete mode 100644 docs/dev/news/5239.fix delete mode 100644 docs/dev/news/5247.feat diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 6124b11a42c..f9ee0efba94 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,30 @@ See [docs/dev/news/](docs/dev/news/). +# 4.6.0 + +## New features + +- Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. (https://github.com/dafny-lang/dafny/pull/5097) + +- Add an option --progress that can be used to track the progress of verification. (https://github.com/dafny-lang/dafny/pull/5150) + +- Add the attribute `{:isolate_assertions}`, which does the same as `{:vcs_split_on_every_assert}`. Deprecated `{:vcs_split_on_every_assert}` (https://github.com/dafny-lang/dafny/pull/5247) + +## Bug fixes + +- (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (https://github.com/dafny-lang/dafny/pull/4844) + +- Add uniform checking of type characteristics in refinement modules (https://github.com/dafny-lang/dafny/pull/5146) + +- Fixed links associated with the standard libraries. (https://github.com/dafny-lang/dafny/pull/5176) + +- fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits. + feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields. + (https://github.com/dafny-lang/dafny/pull/5234) + +- Fix the default string value emitted for JavaScript (https://github.com/dafny-lang/dafny/pull/5239) + # 4.5.0 ## New features diff --git a/docs/dev/news/4844.fix b/docs/dev/news/4844.fix deleted file mode 100644 index 29dc060bae6..00000000000 --- a/docs/dev/news/4844.fix +++ /dev/null @@ -1 +0,0 @@ -(soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap \ No newline at end of file diff --git a/docs/dev/news/5097.feat b/docs/dev/news/5097.feat deleted file mode 100644 index b275d72aea1..00000000000 --- a/docs/dev/news/5097.feat +++ /dev/null @@ -1 +0,0 @@ -Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. \ No newline at end of file diff --git a/docs/dev/news/5146.fix b/docs/dev/news/5146.fix deleted file mode 100644 index e3279703489..00000000000 --- a/docs/dev/news/5146.fix +++ /dev/null @@ -1 +0,0 @@ -Add uniform checking of type characteristics in refinement modules diff --git a/docs/dev/news/5150.feat b/docs/dev/news/5150.feat deleted file mode 100644 index e377e69fa5e..00000000000 --- a/docs/dev/news/5150.feat +++ /dev/null @@ -1 +0,0 @@ -Add an option --progress that can be used to track the progress of verification. \ No newline at end of file diff --git a/docs/dev/news/5176.fix b/docs/dev/news/5176.fix deleted file mode 100644 index 9c980829d02..00000000000 --- a/docs/dev/news/5176.fix +++ /dev/null @@ -1 +0,0 @@ -Fixed links associated with the standard libraries. \ No newline at end of file diff --git a/docs/dev/news/5234.fix b/docs/dev/news/5234.fix deleted file mode 100644 index 826c4a015ef..00000000000 --- a/docs/dev/news/5234.fix +++ /dev/null @@ -1,2 +0,0 @@ -fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits. -feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields. diff --git a/docs/dev/news/5239.fix b/docs/dev/news/5239.fix deleted file mode 100644 index 901cf9369ba..00000000000 --- a/docs/dev/news/5239.fix +++ /dev/null @@ -1 +0,0 @@ -Fix the default string value emitted for JavaScript diff --git a/docs/dev/news/5247.feat b/docs/dev/news/5247.feat deleted file mode 100644 index b203266de28..00000000000 --- 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