Release Dafny 4.0.0

dafny-lang · Mar 2, 2023 · dea0133 · dea0133
1 parent f522955
commit dea0133
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 9 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -2,6 +2,24 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.0.0
+
+## Breaking changes
+
+- Remove deprecated countVerificationErrors option (https://github.com/dafny-lang/dafny/pull/3165)
+
+- The default version of Z3 Dafny uses for verification is now 4.12.1. (https://github.com/dafny-lang/dafny/pull/3400)
+
+- The default values of several options has changed in Dafny 4.0. See `--help` for details.
+     - `--function-syntax` changed from `3` to `4`
+     - `--quantifier-syntax` changed from `3` to `4`
+     - `--unicode-char` changed from `false` to `true`
+  (https://github.com/dafny-lang/dafny/pull/3623)
+
+- The default value of the `/allocated` option is now `4`, and the option itself is deprecated. (https://github.com/dafny-lang/dafny/pull/3637)
+
+- Compilation to Go no longer attempts to use the Dafny `string` type and the Go `string` type interchangably when calling external methods (which was buggy and unsound). (https://github.com/dafny-lang/dafny/pull/3647)
+
 # 3.13.1
 
 ## New features

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -1,7 +1,7 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>4.0.0.50302<!--Version 3.13.1, year 2018+5, month 3, day 2.--></VersionPrefix>
+    <VersionPrefix>4.0.0.50302<!--Version 4.0.0, year 2018+5, month 3, day 2.--></VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
 

diff --git a/docs/dev/news/3165.break b/docs/dev/news/3165.break
diff --git a/docs/dev/news/3400.break b/docs/dev/news/3400.break
diff --git a/docs/dev/news/3623.break b/docs/dev/news/3623.break
diff --git a/docs/dev/news/3637.break b/docs/dev/news/3637.break
diff --git a/docs/dev/news/3647.break b/docs/dev/news/3647.break