chore: Add missing release notes, remove feature all compilers suppor…

…t now (#3141) Ideally the feature would have been removed in the PR that implemented it in Java (#3072), but unfortunately the `Feature` mechanism only allows a compiler to cleanly opt-out of supporting a feature, and we don't yet have a complementary mechanism to test that a compiler that claims to not support a feature does not in fact support that feature! <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 · Nov 30, 2022 · e4248db · e4248db
1 parent 50c2c99
commit e4248db
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 5 deletions.
diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -43,7 +43,6 @@ public string TransformToClassName(string baseName) =>
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.Iterators,
       Feature.SubsetTypeTests,
-      Feature.TraitTypeParameters,
       Feature.MethodSynthesis,
       Feature.TuplesWiderThan20
     };

diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs
@@ -57,9 +57,6 @@ public enum Feature {
   [FeatureDescription("Collections with trait element types", "sec-collection-types")]
   CollectionsOfTraits,
 
-  [FeatureDescription("User-defined types with traits as type parameters", "sec-trait-types")]
-  TraitTypeParameters,
-
   [FeatureDescription("External module names with only underscores", "sec-extern-decls")]
   AllUnderscoreExternalModuleNames,
 

diff --git a/docs/DafnyRef/Features.md b/docs/DafnyRef/Features.md
@@ -6,7 +6,6 @@
 | [Function values](#sec-arrow-subset-types) |  X  |  X  |  X  |  X  |  X  |  |
 | [Iterators](#sec-iterator-types) |  X  |  X  |  X  |  |  X  |  |
 | [Collections with trait element types](#sec-collection-types) |  X  |  X  |  X  |  X  |  X  |  |
-| [User-defined types with traits as type parameters](#sec-trait-types) |  X  |  X  |  X  |  |  X  |  X  |
 | [External module names with only underscores](#sec-extern-decls) |  X  |  X  |  |  X  |  X  |  X  |
 | [Co-inductive datatypes](#sec-co-inductive-datatypes) |  X  |  X  |  X  |  X  |  X  |  |
 | [Multisets](#sec-multisets) |  X  |  X  |  X  |  X  |  X  |  |

diff --git a/docs/dev/news/2795.feat b/docs/dev/news/2795.feat
@@ -0,0 +1 @@
+The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks.
diff --git a/docs/dev/news/3016.feat b/docs/dev/news/3016.feat
@@ -0,0 +1,3 @@
+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.