From e4248db7cd54f841b07f25b8152b7d9847c60fc1 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 30 Nov 2022 11:37:27 -0800 Subject: [PATCH] chore: Add missing release notes, remove feature all compilers support now (#3141) Ideally the feature would have been removed in the PR that implemented it in Java (https://github.com/dafny-lang/dafny/pull/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! 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). --- Source/DafnyCore/Compilers/Compiler-java.cs | 1 - Source/DafnyCore/Feature.cs | 3 --- docs/DafnyRef/Features.md | 1 - docs/dev/news/2795.feat | 1 + docs/dev/news/3016.feat | 3 +++ 5 files changed, 4 insertions(+), 5 deletions(-) create mode 100644 docs/dev/news/2795.feat create mode 100644 docs/dev/news/3016.feat diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs index c180f4c03ee..3e5d4df9db3 100644 --- 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 UnsupportedFeatures => new HashSet { Feature.Iterators, Feature.SubsetTypeTests, - Feature.TraitTypeParameters, Feature.MethodSynthesis, Feature.TuplesWiderThan20 }; diff --git a/Source/DafnyCore/Feature.cs b/Source/DafnyCore/Feature.cs index fcb2c86a3cd..ada6c255039 100644 --- 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 index 822f638902a..be5351b2c7b 100644 --- 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 new file mode 100644 index 00000000000..b5908ae5818 --- /dev/null +++ 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. \ No newline at end of file diff --git a/docs/dev/news/3016.feat b/docs/dev/news/3016.feat new file mode 100644 index 00000000000..3a697a4a99a --- /dev/null +++ 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.