diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml new file mode 100644 index 000000000..da00a4c70 --- /dev/null +++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml @@ -0,0 +1,21 @@ +# +# This local action sets up code dependencies +# to run Smithy-Dafny CI in GitHub Actions workflows. +# + +name: "Install Smithy-Dafny codegen dependencies" +description: "Install Java package dependencies required to run Smithy-Dafny codegen" +runs: + using: "composite" + steps: + - name: Install smithy-dafny-codegen Rust dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML + build-root-directory: smithy-dafny/smithy-dafny-codegen-modules/smithy-rs + + - name: Install smithy-dafny-codegen Python dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :smithy-python-codegen:pTML + build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 08c5fbd51..2c984d57d 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -42,7 +42,7 @@ jobs: # The specification submodule is private so we don't have access, but we don't need # it to verify the Dafny code. Instead we manually pull the submodules we DO need. - run: git submodule update --init libraries - - run: git submodule update --init smithy-dafny + - run: git submodule update --init --recursive smithy-dafny # Only used to format generated code # and to translate version strings such as "nightly-latest" @@ -57,6 +57,15 @@ jobs: with: dotnet-version: ${{ matrix.dotnet-version }} + - name: Setup Java 17 for codegen + uses: actions/setup-java@v3 + with: + distribution: "corretto" + java-version: "17" + + - name: Install Smithy-Dafny codegen dependencies + uses: ./.github/actions/install_smithy_dafny_codegen_dependencies + - uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch index 27a455a72..06e00d005 100644 --- a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch @@ -1,8 +1,8 @@ diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs -index b10e603c..89561181 100644 +index e05ad66e..7b6ad3a7 100644 --- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs -@@ -3436,7 +3436,9 @@ namespace AWS.Cryptography.MaterialProviders +@@ -3872,7 +3872,9 @@ namespace AWS.Cryptography.MaterialProviders dafnyVal._ComAmazonawsDynamodb ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch index f9ee0bc55..77b056727 100644 --- a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch @@ -1,8 +1,8 @@ diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs -index f5ef0458..f846a946 100644 +index 95c9eba1..bcd537fb 100644 --- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs -@@ -629,7 +629,9 @@ namespace AWS.Cryptography.KeyStore +@@ -732,7 +732,9 @@ namespace AWS.Cryptography.KeyStore dafnyVal._ComAmazonawsDynamodb ); case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal: @@ -13,7 +13,7 @@ index f5ef0458..f846a946 100644 dafnyVal._ComAmazonawsKms ); case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal: -@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore +@@ -755,7 +757,9 @@ namespace AWS.Cryptography.KeyStore { case "Com.Amazonaws.KMS": return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms( diff --git a/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch index 10981d791..e7837dd3d 100644 --- a/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch +++ b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch @@ -1,8 +1,8 @@ diff --git b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs -index 72738b20..83ba3510 100644 +index 43bf1a88..76f8023e 100644 --- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +++ a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs -@@ -10809,7 +10809,13 @@ namespace Com.Amazonaws.Dynamodb +@@ -11000,7 +11000,13 @@ namespace Com.Amazonaws.Dynamodb } public static Wrappers_Compile._IOption>> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_Projection__M16_NonKeyAttributes(System.Collections.Generic.List value) { diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch index b5db0712e..7ed7a98c4 100644 --- a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch @@ -1,7 +1,7 @@ -diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java -index 171a36d3..3964b7cb 100644 ---- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java -+++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +index c30e7cdf..3964b7cb 100644 +--- a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java ++++ b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java @@ -8040,6 +8040,126 @@ public class ToNative { return builder.build(); } @@ -129,20 +129,9 @@ index 171a36d3..3964b7cb 100644 public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) { return ((Shim) dafnyValue).impl(); } -@@ -8054,17 +8174,9 @@ public class ToNative { - return (DynamoDbException) dafnyValue.dtor_obj(); +@@ -8055,6 +8175,8 @@ public class ToNative { } else if (dafnyValue.dtor_obj() instanceof Exception) { return (RuntimeException) dafnyValue.dtor_obj(); -- } else if (dafnyValue.dtor_message().is_Some()) { -- final String suffix = dafnyValue.dtor_obj() != null -- ? String.format(" Unknown Object: %s", dafnyValue.dtor_obj()) -- : ""; -- final String message = -- software.amazon.smithy.dafny.conversion.ToNative.Simple.String( -- dafnyValue.dtor_message().dtor_value() -- ) + -- suffix; -- return new RuntimeException(message); } + // BEGIN MANUAL EDIT + // END MANUAL EDIT diff --git a/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch index c30c759d3..0c4751be4 100644 --- a/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch +++ b/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch @@ -1,7 +1,7 @@ -diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java index 52abd119..9d02d333 100644 ---- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java -+++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +--- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java ++++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java @@ -2300,7 +2300,13 @@ public class ToDafny { public static DafnySequence< @@ -50,10 +50,10 @@ index 52abd119..9d02d333 100644 { return SigningAlgorithmSpec.create_SM2DSA(); } -diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java -index 56979da2..59df5196 100644 ---- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java -+++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +index e8eddd3c..59df5196 100644 +--- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java ++++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java @@ -4542,6 +4542,196 @@ public class ToNative { return builder.build(); } @@ -251,20 +251,9 @@ index 56979da2..59df5196 100644 public static KmsClient TrentService(IKMSClient dafnyValue) { return ((Shim) dafnyValue).impl(); } -@@ -4556,17 +4746,9 @@ public class ToNative { - return (KmsException) dafnyValue.dtor_obj(); +@@ -4557,6 +4747,8 @@ public class ToNative { } else if (dafnyValue.dtor_obj() instanceof Exception) { return (RuntimeException) dafnyValue.dtor_obj(); -- } else if (dafnyValue.dtor_message().is_Some()) { -- final String suffix = dafnyValue.dtor_obj() != null -- ? String.format(" Unknown Object: %s", dafnyValue.dtor_obj()) -- : ""; -- final String message = -- software.amazon.smithy.dafny.conversion.ToNative.Simple.String( -- dafnyValue.dtor_message().dtor_value() -- ) + -- suffix; -- return new RuntimeException(message); } + // BEGIN MANUAL EDIT + // END MANUAL EDIT diff --git a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch index e55782a7a..d49f05733 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch +++ b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch @@ -1,8 +1,8 @@ diff --git b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs -index 87b39a81..e57de1dd 100644 +index 7b556e25..5cf59ac4 100644 --- b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +++ a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs -@@ -3399,7 +3399,9 @@ namespace AWS.Cryptography.MaterialProviders.Wrapped +@@ -3835,7 +3835,9 @@ namespace AWS.Cryptography.MaterialProviders.Wrapped dafnyVal._ComAmazonawsDynamodb ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: diff --git a/libraries b/libraries index dbb1949da..e9b898d0e 160000 --- a/libraries +++ b/libraries @@ -1 +1 @@ -Subproject commit dbb1949da0e610bd0cc0dfe1ecc751808e928dc4 +Subproject commit e9b898d0ec08e129b8e61306b2617b36c4ce5d3e diff --git a/smithy-dafny b/smithy-dafny index 2baebfbcb..768014fe5 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit 2baebfbcb4b62ed0949c185610316725019a6dae +Subproject commit 768014fe5870b5e6da3f9c2f2881deca72e55be5