You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
fix: Remove 4.4 DDB and KMS patches, abstract test to work on later Dafny versions (#611)
These `dafny-4.4.0.patch` files only forced the generated code back to the Dafny 4.2 style of not passing type descriptors to generic data constructors. This was intended to help address the incompatibility between the MPL and consuming libraries when built with a newer Dafny version, but there are two better options available:
1. smithy-dafny emits the right code if given the right `--dafny-version` argument. This doesn't address the incompatibility, but does ensure type descriptors are set correctly which enables more features in the future such as `--general-traits`.
2. Dafny itself now has a `--legacy-data-constructors` flag that makes it emit deprecated overloads that just set type descriptors to null. This is the actual plan for upgrading the MPL, but it is more complicated to set conditionally in the project build system.
On that note, also refactored a unit test slightly to let Dafny generate the relevant code.
0 commit comments