Release Dafny 3.10.0 (#3201)

<small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Dec 16, 2022 · 510b679 · 510b679
1 parent 96042ff
commit 510b679
Show file tree

Hide file tree

Showing 36 changed files with 80 additions and 38 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -2,6 +2,85 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 3.10.0
+
+## New features
+
+- Emit warnings about possibly missing parentheses, based on operator precedence and unusual identation (https://github.com/dafny-lang/dafny/pull/2783)
+
+- The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks. (https://github.com/dafny-lang/dafny/pull/2795)
+
+- Counterexamples involving sequences present elements in ascending order by index. (https://github.com/dafny-lang/dafny/pull/2975)
+
+- The definition of the `char` type will change in Dafny version 4, to represent any Unicode scalar value instead of any UTF-16 code unit.
+  The new command-line option `--unicode-char` allows early adoption of this mode.
+  See section [7.5](http://dafny.org/dafny/DafnyRef/DafnyRef#sec-characters) of the Reference Manual for more details.
+  (https://github.com/dafny-lang/dafny/pull/3016)
+
+- `dafny run` now consistently requests UTF-8 output from compiled code.
+  Use `chcp 65501` if you see garbled output on Windows.
+  (https://github.com/dafny-lang/dafny/pull/3049)
+
+- feat: support for traits as type arguments by fully allowing variance on datatypes in Java (https://github.com/dafny-lang/dafny/pull/3072)
+
+## Bug fixes
+
+- Function by method with the same name as a method won't crash resolver (https://github.com/dafny-lang/dafny/pull/2019)
+
+- Better reporting if 'this' used in a subset type - and no crash (https://github.com/dafny-lang/dafny/pull/2068)
+
+- Support for aliases in module resolution without crashing on imports (https://github.com/dafny-lang/dafny/pull/2108)
+
+- Added missing check to prevent crash during resolution (https://github.com/dafny-lang/dafny/pull/2111)
+
+- No more resolver crash on pattern match with incompatible types (https://github.com/dafny-lang/dafny/pull/2139)
+
+- Refinements get errors at the correct place in LSP (https://github.com/dafny-lang/dafny/pull/2402)
+
+- Resolution errors in the left-hand sign of an assign-such-that statement do not crash Dafny anymore (https://github.com/dafny-lang/dafny/pull/2496)
+
+- old() cannot be inferred as a trigger alone (https://github.com/dafny-lang/dafny/pull/2593)
+
+- Labels are no longer compiled in the case of variable declarations (https://github.com/dafny-lang/dafny/pull/2608)
+
+- No more mention of reveal lemmas when implementing opaque functions in traits (https://github.com/dafny-lang/dafny/pull/2612)
+
+- Verification of abstract modules not duplicated when imported (https://github.com/dafny-lang/dafny/pull/2703)
+
+- Dafny now compiles functions that mix tail- and non-tail-recursive calls without crashing (https://github.com/dafny-lang/dafny/pull/2726)
+
+- substitution of binding guards does not crash if splits present (https://github.com/dafny-lang/dafny/pull/2748)
+
+- No more crash when constraining type synonyms (https://github.com/dafny-lang/dafny/pull/2829)
+
+- Returning a tuple when it should be two variables does not crash Dafny anymore (https://github.com/dafny-lang/dafny/pull/2878)
+
+- Default generic values no longer cause compilation error (https://github.com/dafny-lang/dafny/pull/2885)
+
+- Now publishing Dafny Binary for MacOS Arm64 architecture (https://github.com/dafny-lang/dafny/pull/2889)
+
+- Added a missing case in the Translator (pattern matching for variable declarations) (https://github.com/dafny-lang/dafny/pull/2920)
+
+- The Python and Go backends now encode non-ASCII characters in string literals correctly (https://github.com/dafny-lang/dafny/pull/2926)
+
+- Added a missing case of TypeSynonymDecl in the resolver that caused a crash (https://github.com/dafny-lang/dafny/pull/2927)
+
+- Fix malformed Boogie generated for extreme predicates (https://github.com/dafny-lang/dafny/pull/2984)
+
+- Counter-examples with non-integer sequence indices do not crash Dafny anymore. (https://github.com/dafny-lang/dafny/pull/3048)
+
+- Use correct type for map update expression (https://github.com/dafny-lang/dafny/pull/3059)
+
+- Language server no longer crashing in special case (https://github.com/dafny-lang/dafny/pull/3062)
+
+- Resolved an instance in which the Dafny language server could enter a broken state. (https://github.com/dafny-lang/dafny/pull/3065)
+
+- Do not refer to an implicit assignment in error messages on return statements (https://github.com/dafny-lang/dafny/pull/3125)
+
+- Multiple exact same failing assertions do not crash the Boogie counter-example engine anymore (https://github.com/dafny-lang/dafny/pull/3136)
+
+- Duplicate declarations caused by resolver do not crash the language server anymore (https://github.com/dafny-lang/dafny/pull/3155)
+
 # 3.9.1
 
 ## New features

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -1,7 +1,7 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>3.10.0</VersionPrefix>
+    <VersionPrefix>3.10.0.41215<!--Version 3.10.0, year 2018+4, month 12, day 15.--></VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
 

diff --git a/docs/dev/news/2019.fix b/docs/dev/news/2019.fix
diff --git a/docs/dev/news/2068.fix b/docs/dev/news/2068.fix
diff --git a/docs/dev/news/2108.fix b/docs/dev/news/2108.fix
diff --git a/docs/dev/news/2111.fix b/docs/dev/news/2111.fix
diff --git a/docs/dev/news/2139.fix b/docs/dev/news/2139.fix
diff --git a/docs/dev/news/2402.fix b/docs/dev/news/2402.fix
diff --git a/docs/dev/news/2496.fix b/docs/dev/news/2496.fix
diff --git a/docs/dev/news/2593.fix b/docs/dev/news/2593.fix
diff --git a/docs/dev/news/2608.fix b/docs/dev/news/2608.fix
diff --git a/docs/dev/news/2612.fix b/docs/dev/news/2612.fix
diff --git a/docs/dev/news/2703.fix b/docs/dev/news/2703.fix
diff --git a/docs/dev/news/2726.fix b/docs/dev/news/2726.fix
diff --git a/docs/dev/news/2748.fix b/docs/dev/news/2748.fix
diff --git a/docs/dev/news/2783.feat b/docs/dev/news/2783.feat
diff --git a/docs/dev/news/2795.feat b/docs/dev/news/2795.feat
diff --git a/docs/dev/news/2829.fix b/docs/dev/news/2829.fix
diff --git a/docs/dev/news/2878.fix b/docs/dev/news/2878.fix
diff --git a/docs/dev/news/2885.fix b/docs/dev/news/2885.fix
diff --git a/docs/dev/news/2889.fix b/docs/dev/news/2889.fix
diff --git a/docs/dev/news/2920.fix b/docs/dev/news/2920.fix
diff --git a/docs/dev/news/2926.fix b/docs/dev/news/2926.fix
diff --git a/docs/dev/news/2927.fix b/docs/dev/news/2927.fix
diff --git a/docs/dev/news/2975.feat b/docs/dev/news/2975.feat
diff --git a/docs/dev/news/2984.fix b/docs/dev/news/2984.fix
diff --git a/docs/dev/news/3016.feat b/docs/dev/news/3016.feat
diff --git a/docs/dev/news/3048.fix b/docs/dev/news/3048.fix
diff --git a/docs/dev/news/3049.feat b/docs/dev/news/3049.feat
diff --git a/docs/dev/news/3059.fix b/docs/dev/news/3059.fix
diff --git a/docs/dev/news/3062.fix b/docs/dev/news/3062.fix
diff --git a/docs/dev/news/3065.fix b/docs/dev/news/3065.fix
diff --git a/docs/dev/news/3072.feat b/docs/dev/news/3072.feat
diff --git a/docs/dev/news/3125.fix b/docs/dev/news/3125.fix
diff --git a/docs/dev/news/3136.fix b/docs/dev/news/3136.fix
diff --git a/docs/dev/news/3155.fix b/docs/dev/news/3155.fix