From 707b18acee078b3aa4d84c0590a980966bf22428 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 12 Dec 2023 10:14:55 -0800
Subject: [PATCH] Release Dafny 4.4.0

---
 RELEASE_NOTES.md        | 76 +++++++++++++++++++++++++++++++++++++++++
 docs/dev/news/1373.fix  |  1 -
 docs/dev/news/3792.fix  |  1 -
 docs/dev/news/4406.fix  |  1 -
 docs/dev/news/4440.feat |  2 --
 docs/dev/news/4530.fix  |  2 --
 docs/dev/news/4542.feat |  1 -
 docs/dev/news/4563.feat |  1 -
 docs/dev/news/4607.fix  |  1 -
 docs/dev/news/4619.feat |  1 -
 docs/dev/news/4625.feat |  1 -
 docs/dev/news/4635.fix  |  1 -
 docs/dev/news/4658.feat |  2 --
 docs/dev/news/4673.feat |  1 -
 docs/dev/news/4675.fix  |  1 -
 docs/dev/news/4678.feat |  2 --
 docs/dev/news/4681.feat |  1 -
 docs/dev/news/4683.fix  |  1 -
 docs/dev/news/4693.fix  |  1 -
 docs/dev/news/4703.fix  |  1 -
 docs/dev/news/4710.fix  |  1 -
 docs/dev/news/4724.fix  |  1 -
 docs/dev/news/4733.fix  |  1 -
 docs/dev/news/4734.fix  |  1 -
 docs/dev/news/4755.feat |  1 -
 docs/dev/news/4768.fix  |  1 -
 docs/dev/news/4773.feat |  2 --
 docs/dev/news/4787.fix  |  1 -
 docs/dev/news/4812.fix  |  1 -
 docs/dev/news/4833.fix  |  1 -
 docs/dev/news/4843.fix  |  1 -
 docs/dev/news/4855.feat |  1 -
 32 files changed, 76 insertions(+), 36 deletions(-)
 delete mode 100644 docs/dev/news/1373.fix
 delete mode 100644 docs/dev/news/3792.fix
 delete mode 100644 docs/dev/news/4406.fix
 delete mode 100644 docs/dev/news/4440.feat
 delete mode 100644 docs/dev/news/4530.fix
 delete mode 100644 docs/dev/news/4542.feat
 delete mode 100644 docs/dev/news/4563.feat
 delete mode 100644 docs/dev/news/4607.fix
 delete mode 100644 docs/dev/news/4619.feat
 delete mode 100644 docs/dev/news/4625.feat
 delete mode 100644 docs/dev/news/4635.fix
 delete mode 100644 docs/dev/news/4658.feat
 delete mode 100644 docs/dev/news/4673.feat
 delete mode 100644 docs/dev/news/4675.fix
 delete mode 100644 docs/dev/news/4678.feat
 delete mode 100644 docs/dev/news/4681.feat
 delete mode 100644 docs/dev/news/4683.fix
 delete mode 100644 docs/dev/news/4693.fix
 delete mode 100644 docs/dev/news/4703.fix
 delete mode 100644 docs/dev/news/4710.fix
 delete mode 100644 docs/dev/news/4724.fix
 delete mode 100644 docs/dev/news/4733.fix
 delete mode 100644 docs/dev/news/4734.fix
 delete mode 100644 docs/dev/news/4755.feat
 delete mode 100644 docs/dev/news/4768.fix
 delete mode 100644 docs/dev/news/4773.feat
 delete mode 100644 docs/dev/news/4787.fix
 delete mode 100644 docs/dev/news/4812.fix
 delete mode 100644 docs/dev/news/4833.fix
 delete mode 100644 docs/dev/news/4843.fix
 delete mode 100644 docs/dev/news/4855.feat

diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 2fe1853a26f..c50ba7a0f4c 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,82 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.4.0
+
+## New features
+
+- Reads clauses on method declarations are now supported when the `--reads-clauses-on-methods` option is provided. 
+  The `{:concurrent}` attribute now verifies that the `reads` and `modifies` clauses are empty instead of generating an auditor warning.
+  (https://github.com/dafny-lang/dafny/pull/4440)
+
+- Added two new options, `--warn-contradictory-assumptions` and `--warn-redundant-assumptions`, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (https://github.com/dafny-lang/dafny/pull/4542)
+
+- Verification of the `{:concurrent}` attribute on methods now allows non-empty `reads` and `modifies` clauses with the `{:assume_concurrent}` attribute. (https://github.com/dafny-lang/dafny/pull/4563)
+
+- Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/4619)
+
+- The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged. (https://github.com/dafny-lang/dafny/pull/4625)
+
+- Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
+  instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.
+  (https://github.com/dafny-lang/dafny/pull/4658)
+
+- The new `--only-label` option to `merge-coverage-reports` includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification. (https://github.com/dafny-lang/dafny/pull/4673)
+
+- The Dafny distribution now includes standard libraries, available with the `--standard-libraries` option.
+  See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
+  (https://github.com/dafny-lang/dafny/pull/4678)
+
+- Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/4681)
+
+- The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime. (https://github.com/dafny-lang/dafny/pull/4755)
+
+- Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute `{:disable-nonlinear-arithmetic}`, 
+  which optionally takes the value false to enable nonlinear arithmetic.
+  (https://github.com/dafny-lang/dafny/pull/4773)
+
+- Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (https://github.com/dafny-lang/dafny/pull/4855)
+
+## Bug fixes
+
+- Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (https://github.com/dafny-lang/dafny/pull/1373)
+
+- Subset type decl's witness correctly taken into account (https://github.com/dafny-lang/dafny/pull/3792)
+
+- Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations (https://github.com/dafny-lang/dafny/pull/4406)
+
+- Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. (https://github.com/dafny-lang/dafny/pull/4530)
+
+- Fix a bug that prevented certain types of lemma to be verified in the IDE (https://github.com/dafny-lang/dafny/pull/4607)
+
+- Dot completion now works on values the type of which is a type synonym. (https://github.com/dafny-lang/dafny/pull/4635)
+
+- Fix a case where the document symbol API would return incorrect data when working on a file with parse errors (https://github.com/dafny-lang/dafny/pull/4675)
+
+- Emit less nested target code in match-case expressions (nice for readability, and necessary for Java) (https://github.com/dafny-lang/dafny/pull/4683)
+
+- Ghost diagnostics are now correctly updated when they become empty (https://github.com/dafny-lang/dafny/pull/4693)
+
+- Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server (https://github.com/dafny-lang/dafny/pull/4703)
+
+- Prevent double-counting of covered/uncovered lines in test coverage reports (https://github.com/dafny-lang/dafny/pull/4710)
+
+- fix: correction of type inference for default expressions (https://github.com/dafny-lang/dafny/pull/4724)
+
+- The new type checker now also supports static reveals for instance functions (https://github.com/dafny-lang/dafny/pull/4733)
+
+- Resolve :- expressions with void outcomes in new resolver (https://github.com/dafny-lang/dafny/pull/4734)
+
+- Crash in the resolver on type parameters of opaque functions in refined modules (https://github.com/dafny-lang/dafny/pull/4768)
+
+- Fix error messages being printed after their context snippets (https://github.com/dafny-lang/dafny/pull/4787)
+
+- Override checks no longer crashing when substituting type parameters and equality (https://github.com/dafny-lang/dafny/pull/4812)
+
+- Removed one cause of need for restarting the IDE. (https://github.com/dafny-lang/dafny/pull/4833)
+
+- The Python compiler emits reserved names for datatypes (https://github.com/dafny-lang/dafny/pull/4843)
+
 # 4.3.0
 
 ## New features
diff --git a/docs/dev/news/1373.fix b/docs/dev/news/1373.fix
deleted file mode 100644
index 0c4804c1161..00000000000
--- a/docs/dev/news/1373.fix
+++ /dev/null
@@ -1 +0,0 @@
-Ensures that computing the set of values or items of map can only be done if the type of the range supports equality.
\ No newline at end of file
diff --git a/docs/dev/news/3792.fix b/docs/dev/news/3792.fix
deleted file mode 100644
index 321e3b1f222..00000000000
--- a/docs/dev/news/3792.fix
+++ /dev/null
@@ -1 +0,0 @@
-Subset type decl's witness correctly taken into account
\ No newline at end of file
diff --git a/docs/dev/news/4406.fix b/docs/dev/news/4406.fix
deleted file mode 100644
index fdab1245e3a..00000000000
--- a/docs/dev/news/4406.fix
+++ /dev/null
@@ -1 +0,0 @@
-Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations
\ No newline at end of file
diff --git a/docs/dev/news/4440.feat b/docs/dev/news/4440.feat
deleted file mode 100644
index c5b6e118f3f..00000000000
--- a/docs/dev/news/4440.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-Reads clauses on method declarations are now supported when the `--reads-clauses-on-methods` option is provided. 
-The `{:concurrent}` attribute now verifies that the `reads` and `modifies` clauses are empty instead of generating an auditor warning.
\ No newline at end of file
diff --git a/docs/dev/news/4530.fix b/docs/dev/news/4530.fix
deleted file mode 100644
index 2c0d212c759..00000000000
--- a/docs/dev/news/4530.fix
+++ /dev/null
@@ -1,2 +0,0 @@
-Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program.
-
diff --git a/docs/dev/news/4542.feat b/docs/dev/news/4542.feat
deleted file mode 100644
index 652fcdceea1..00000000000
--- a/docs/dev/news/4542.feat
+++ /dev/null
@@ -1 +0,0 @@
-Added two new options, `--warn-contradictory-assumptions` and `--warn-redundant-assumptions`, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them.
diff --git a/docs/dev/news/4563.feat b/docs/dev/news/4563.feat
deleted file mode 100644
index 4adf1bf681f..00000000000
--- a/docs/dev/news/4563.feat
+++ /dev/null
@@ -1 +0,0 @@
-Verification of the `{:concurrent}` attribute on methods now allows non-empty `reads` and `modifies` clauses with the `{:assume_concurrent}` attribute.
diff --git a/docs/dev/news/4607.fix b/docs/dev/news/4607.fix
deleted file mode 100644
index 6975ac819b3..00000000000
--- a/docs/dev/news/4607.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fix a bug that prevented certain types of lemma to be verified in the IDE 
\ No newline at end of file
diff --git a/docs/dev/news/4619.feat b/docs/dev/news/4619.feat
deleted file mode 100644
index 58ea4b3b2b3..00000000000
--- a/docs/dev/news/4619.feat
+++ /dev/null
@@ -1 +0,0 @@
-Implemented support for workspace/symbol request to allow IDE navigation by symbol.
\ No newline at end of file
diff --git a/docs/dev/news/4625.feat b/docs/dev/news/4625.feat
deleted file mode 100644
index 23ce498a469..00000000000
--- a/docs/dev/news/4625.feat
+++ /dev/null
@@ -1 +0,0 @@
-The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.
diff --git a/docs/dev/news/4635.fix b/docs/dev/news/4635.fix
deleted file mode 100644
index 383501f13c6..00000000000
--- a/docs/dev/news/4635.fix
+++ /dev/null
@@ -1 +0,0 @@
-Dot completion now works on values the type of which is a type synonym.
\ No newline at end of file
diff --git a/docs/dev/news/4658.feat b/docs/dev/news/4658.feat
deleted file mode 100644
index 3b5d8f0ad8c..00000000000
--- a/docs/dev/news/4658.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
-instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.
\ No newline at end of file
diff --git a/docs/dev/news/4673.feat b/docs/dev/news/4673.feat
deleted file mode 100644
index 2867fa8ef31..00000000000
--- a/docs/dev/news/4673.feat
+++ /dev/null
@@ -1 +0,0 @@
-The new `--only-label` option to `merge-coverage-reports` includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification.
diff --git a/docs/dev/news/4675.fix b/docs/dev/news/4675.fix
deleted file mode 100644
index 1e27cb0cc92..00000000000
--- a/docs/dev/news/4675.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fix a case where the document symbol API would return incorrect data when working on a file with parse errors
\ No newline at end of file
diff --git a/docs/dev/news/4678.feat b/docs/dev/news/4678.feat
deleted file mode 100644
index fd8774dfbdd..00000000000
--- a/docs/dev/news/4678.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-The Dafny distribution now includes standard libraries, available with the `--standard-libraries` option.
-See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
diff --git a/docs/dev/news/4681.feat b/docs/dev/news/4681.feat
deleted file mode 100644
index f1fe34a91af..00000000000
--- a/docs/dev/news/4681.feat
+++ /dev/null
@@ -1 +0,0 @@
-Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages.
\ No newline at end of file
diff --git a/docs/dev/news/4683.fix b/docs/dev/news/4683.fix
deleted file mode 100644
index 15255038ad6..00000000000
--- a/docs/dev/news/4683.fix
+++ /dev/null
@@ -1 +0,0 @@
-Emit less nested target code in match-case expressions (nice for readability, and necessary for Java)
diff --git a/docs/dev/news/4693.fix b/docs/dev/news/4693.fix
deleted file mode 100644
index 888414d4112..00000000000
--- a/docs/dev/news/4693.fix
+++ /dev/null
@@ -1 +0,0 @@
-Ghost diagnostics are now correctly updated when they become empty
\ No newline at end of file
diff --git a/docs/dev/news/4703.fix b/docs/dev/news/4703.fix
deleted file mode 100644
index 38ae79dae93..00000000000
--- a/docs/dev/news/4703.fix
+++ /dev/null
@@ -1 +0,0 @@
-Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server  
\ No newline at end of file
diff --git a/docs/dev/news/4710.fix b/docs/dev/news/4710.fix
deleted file mode 100644
index 87a62b03007..00000000000
--- a/docs/dev/news/4710.fix
+++ /dev/null
@@ -1 +0,0 @@
-Prevent double-counting of covered/uncovered lines in test coverage reports
diff --git a/docs/dev/news/4724.fix b/docs/dev/news/4724.fix
deleted file mode 100644
index 404c0704326..00000000000
--- a/docs/dev/news/4724.fix
+++ /dev/null
@@ -1 +0,0 @@
-fix: correction of type inference for default expressions 
\ No newline at end of file
diff --git a/docs/dev/news/4733.fix b/docs/dev/news/4733.fix
deleted file mode 100644
index 22691509665..00000000000
--- a/docs/dev/news/4733.fix
+++ /dev/null
@@ -1 +0,0 @@
-The new type checker now also supports static reveals for instance functions
diff --git a/docs/dev/news/4734.fix b/docs/dev/news/4734.fix
deleted file mode 100644
index 82341d9eb4b..00000000000
--- a/docs/dev/news/4734.fix
+++ /dev/null
@@ -1 +0,0 @@
-Resolve :- expressions with void outcomes in new resolver
diff --git a/docs/dev/news/4755.feat b/docs/dev/news/4755.feat
deleted file mode 100644
index 5e5021687d5..00000000000
--- a/docs/dev/news/4755.feat
+++ /dev/null
@@ -1 +0,0 @@
-The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime.
diff --git a/docs/dev/news/4768.fix b/docs/dev/news/4768.fix
deleted file mode 100644
index ca2398374c4..00000000000
--- a/docs/dev/news/4768.fix
+++ /dev/null
@@ -1 +0,0 @@
-Crash in the resolver on type parameters of opaque functions in refined modules
\ No newline at end of file
diff --git a/docs/dev/news/4773.feat b/docs/dev/news/4773.feat
deleted file mode 100644
index 7da43ccadc9..00000000000
--- a/docs/dev/news/4773.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute `{:disable-nonlinear-arithmetic}`, 
-which optionally takes the value false to enable nonlinear arithmetic.
\ No newline at end of file
diff --git a/docs/dev/news/4787.fix b/docs/dev/news/4787.fix
deleted file mode 100644
index 9f1684c9949..00000000000
--- a/docs/dev/news/4787.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fix error messages being printed after their context snippets
diff --git a/docs/dev/news/4812.fix b/docs/dev/news/4812.fix
deleted file mode 100644
index 502c387efc7..00000000000
--- a/docs/dev/news/4812.fix
+++ /dev/null
@@ -1 +0,0 @@
-Override checks no longer crashing when substituting type parameters and equality
\ No newline at end of file
diff --git a/docs/dev/news/4833.fix b/docs/dev/news/4833.fix
deleted file mode 100644
index 557bf88202f..00000000000
--- a/docs/dev/news/4833.fix
+++ /dev/null
@@ -1 +0,0 @@
-Removed one cause of need for restarting the IDE.
\ No newline at end of file
diff --git a/docs/dev/news/4843.fix b/docs/dev/news/4843.fix
deleted file mode 100644
index be55b74964a..00000000000
--- a/docs/dev/news/4843.fix
+++ /dev/null
@@ -1 +0,0 @@
-The Python compiler emits reserved names for datatypes
diff --git a/docs/dev/news/4855.feat b/docs/dev/news/4855.feat
deleted file mode 100644
index 917f31c41ee..00000000000
--- a/docs/dev/news/4855.feat
+++ /dev/null
@@ -1 +0,0 @@
-Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors.
\ No newline at end of file