feat: Python MPL #360

lucasmcdonald3 · 2024-05-29T23:50:40Z

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

* feat: remove quantifier-syntax and pin prettier version

#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches

Bumps software.amazon.awssdk:bom from 2.19.1 to 2.25.1. --- updated-dependencies: - dependency-name: software.amazon.awssdk:bom dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Replaces nearly all of `SharedMakefileV2.mk` with the new `SmithyDafnyMakefile.mk` from the `smithy-dafny` submodule. What's left is just the repo-specific configuration of variables. See #233 for a more readable diff of the existing `SharedMakefileV2.mk` with `SmithyDafnyMakefile.mk`, showing what targets are changing (which is very little as the extra target/improvements in the former were mostly carried over to the latter already).

* chore: add example of tail recursion

… type patches (#267) Uses a newer version of smithy-dafny that corrects the service constructor result type in the same way that #256 fixed it with manual patches. See smithy-lang/smithy-dafny#331 for details on why the helper functions switched back to the trait type.

Co-authored-by: Tony Knapp <[email protected]>

…747)

github-actions · 2024-10-01T19:50:35Z