Skip to content

Commit

Permalink
chore: add polymorphDafny and polymorphDotnet tasks to Smithy Build P…
Browse files Browse the repository at this point in the history
…lugin-based SQS TestModel (#395)

*Issue #, if available:* #356 (related)

*Description of changes:* This PR allows the Smithy Build Plugin-based SQS TestModel to be built and structured similarly to the Makefile/CLI based models used elsewhere. This enables some Smithy features which are not supported by the CLI, such as [Projections](https://smithy.io/2.0/guides/smithy-build-json.html#projections). 

Instead of running `make polymorph_dafny` and `make polymorph_dotnet`, run `./gradlew polymorphDafny` and `./gradlew polymorphDotnet` to generate types for the respective languages. A Makefile is included, as it is needed to run `make transpile_net` and `make test_net`, which work as expected when the above commands are executed.
  • Loading branch information
kessplas authored Jun 11, 2024
1 parent d436b55 commit b7cec71
Show file tree
Hide file tree
Showing 11 changed files with 225 additions and 125 deletions.
19 changes: 0 additions & 19 deletions .github/workflows/smithy-polymorph.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,24 +37,5 @@ jobs:
arguments: :smithy-dafny-codegen:test
build-root-directory: codegen

# Required for building the SQS model
- name: Locally cache smithy-dafny-codegen
uses: gradle/gradle-build-action@v2
with:
arguments: :smithy-dafny-codegen:publishToMavenLocal
build-root-directory: codegen

- name: Sanity-check SQS test model via plugin
uses: gradle/gradle-build-action@v2
with:
arguments: build --info
build-root-directory: TestModels/aws-sdks/sqs

- name: Execute codegen build
uses: gradle/gradle-build-action@v2
with:
arguments: build
build-root-directory: codegen

- name: not-grep
uses: mattsb42-meta/not-grep@1.0.0
7 changes: 7 additions & 0 deletions .github/workflows/test_models_dafny_verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ jobs:
TestModels/aws-sdks/ddb,
TestModels/aws-sdks/glue,
TestModels/aws-sdks/kms,
TestModels/aws-sdks/sqs,
TestModels/aws-sdks/lakeformation,
TestModels/aws-sdks/sqs-via-cli,
]
Expand Down Expand Up @@ -88,6 +89,12 @@ jobs:
with:
dafny-version: ${{ matrix.dafny-version }}

- name: Setup Java 17 for codegen
uses: actions/setup-java@v3
with:
distribution: "corretto"
java-version: "17"

- name: Generate Polymorph Wrapper Dafny code
working-directory: ./${{ matrix.library }}
run: |
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/test_models_net_tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ jobs:
TestModels/aws-sdks/ddb,
TestModels/aws-sdks/glue,
TestModels/aws-sdks/kms,
TestModels/aws-sdks/sqs,
TestModels/aws-sdks/lakeformation,
TestModels/aws-sdks/sqs-via-cli,
]
Expand Down
32 changes: 16 additions & 16 deletions TestModels/aws-sdks/sqs-via-cli/runtimes/net/Extern/SQSClient.cs
Original file line number Diff line number Diff line change
Expand Up @@ -10,23 +10,23 @@
// that refines the AWS SDK SQS Model
namespace software.amazon.cryptography.services.sqs.internaldafny
{
public partial class __default
{

public static
_IResult<
types.ISQSClient,
types._IError
>
SQSClient()
public partial class __default
{
var client = new AmazonSQSClient();

return Result<
types.ISQSClient,
types._IError
>
.create_Success(new SQSShim(client));
public static
_IResult<
types.ISQSClient,
types._IError
>
SQSClient()
{
var client = new AmazonSQSClient();

return Result<
types.ISQSClient,
types._IError
>
.create_Success(new SQSShim(client));
}
}
}
}
44 changes: 44 additions & 0 deletions TestModels/aws-sdks/sqs/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0

# For this project, the Makefile should ONLY be used for:
# - make transpile_net
# - make test_net
# The polymorph commands should be done using gradle instead.

CORES=2

include ../../SharedMakefile.mk

NAMESPACE=com.amazonaws.sqs

PROJECT_SERVICES := \
ComAmazonawsSqs \

SERVICE_NAMESPACE_ComAmazonawsSqs=com.amazonaws.sqs

SERVICE_DEPS_ComAmazonawsSqs :=

SMITHY_DEPS=dafny-dependencies/Model/traits.smithy

AWS_SDK_CMD=--aws-sdk

# This project has no dependencies
# DEPENDENT-MODELS:=


SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/model

# Override calling the polymorph CLI to invoke the Smithy build instead
_polymorph_dafny:
./gradlew polymorphDafny

_polymorph_dotnet:
./gradlew polymorphDotnet


# There is no wrapped target for aws-sdk types
_polymorph_wrapped: ;
_polymorph_wrapped_dafny: ;
_polymorph_wrapped_net: ;
_polymorph_wrapped_java: ;
7 changes: 7 additions & 0 deletions TestModels/aws-sdks/sqs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,14 @@ in the same way that other `smithy-<language>` tools support.

NOTE: The `sqs.json` in this project was copied unmodified from https://github.com/aws/aws-sdk-js-v3/blob/main/codegen/sdk-codegen/aws-models/sqs.json on March 6, 2023.
Part of the requirements of this workflow is that you shouldn't have to manually modify models.

You should be able to use the standard [projections](https://smithy.io/2.0/guides/building-models/build-config.html#projections) feature of the Smithy Gradle plugin
to trim-down or modify a model as needed before code generation instead.

The use of projections is demo'd by this test model; currently the projection `list-queues-and-add-permission-only` is being used.
This projection reduces the SQS model to a minimum set of shapes required in order for the ListQueues sanity test to pass.
The `AddPermission` operation is included due to a bug where models without errors do not generate valid .NET code (see [Github Issue 439](https://github.com/smithy-lang/smithy-dafny/issues/439) for more details).

## Build

### Dafny + .NET
Expand All @@ -25,6 +30,8 @@ gradle build

The generated client package will appear in `build/smithyprojections/sqs/source/dafny-client-codegen`.

You can also use the traditional `make polymorph_dafny` and `make polymorph_dotnet` commands instead.

## Development

To implement <https://github.com/awslabs/polymorph/issues/151>, we provide a similar
Expand Down
33 changes: 33 additions & 0 deletions TestModels/aws-sdks/sqs/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,39 @@ configure<software.amazon.smithy.gradle.SmithyExtension> {
// Uncomment to disable creating a JAR.
tasks["jar"].enabled = false

tasks.register("polymorphDafny") {
dependsOn("build")
doLast {
// if needed, specify a projection to use instead
// default (no projection) is "source"
val projectionName = "list-queues-and-add-permission-only"
copy {
from(layout.buildDirectory.dir("smithyprojections/" + project.name + "/" + projectionName + "/dafny-client-codegen/Model/"))
into("model")
}
exec {
// need to adjust the relative import, since we're copying it away
// the commandLine method does not play nice with sed,
// so we have to execute it through bash :(
commandLine("bash", "-c", "sed '4s|../../../../../../../../dafny-dependencies/StandardLibrary/src/Index.dfy|../../../dafny-dependencies/StandardLibrary/src/Index.dfy|' model/ComAmazonawsSqsTypes.dfy > model/tmp && mv model/tmp model/ComAmazonawsSqsTypes.dfy")
}
}
}

tasks.register("polymorphDotnet") {
dependsOn("build")
doLast {
// if needed, specify a projection to use instead
// default (no projection) is "source"
val projectionName = "list-queues-and-add-permission-only"
copy {
// build plugin calls it "dotnet" and CLI calls it "net"
from(layout.buildDirectory.dir("smithyprojections/" + project.name + "/" + projectionName + "/dafny-client-codegen/runtimes/dotnet"))
into("runtimes/net")
}
}
}

buildscript {
val smithyVersion: String by project

Expand Down
178 changes: 89 additions & 89 deletions TestModels/aws-sdks/sqs/gradlew.bat
Original file line number Diff line number Diff line change
@@ -1,89 +1,89 @@
@rem
@rem Copyright 2015 the original author or authors.
@rem
@rem Licensed under the Apache License, Version 2.0 (the "License");
@rem you may not use this file except in compliance with the License.
@rem You may obtain a copy of the License at
@rem
@rem https://www.apache.org/licenses/LICENSE-2.0
@rem
@rem Unless required by applicable law or agreed to in writing, software
@rem distributed under the License is distributed on an "AS IS" BASIS,
@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@rem See the License for the specific language governing permissions and
@rem limitations under the License.
@rem

@if "%DEBUG%" == "" @echo off
@rem ##########################################################################
@rem
@rem Gradle startup script for Windows
@rem
@rem ##########################################################################

@rem Set local scope for the variables with windows NT shell
if "%OS%"=="Windows_NT" setlocal

set DIRNAME=%~dp0
if "%DIRNAME%" == "" set DIRNAME=.
set APP_BASE_NAME=%~n0
set APP_HOME=%DIRNAME%

@rem Resolve any "." and ".." in APP_HOME to make it shorter.
for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi

@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m"

@rem Find java.exe
if defined JAVA_HOME goto findJavaFromJavaHome

set JAVA_EXE=java.exe
%JAVA_EXE% -version >NUL 2>&1
if "%ERRORLEVEL%" == "0" goto execute

echo.
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.

goto fail

:findJavaFromJavaHome
set JAVA_HOME=%JAVA_HOME:"=%
set JAVA_EXE=%JAVA_HOME%/bin/java.exe

if exist "%JAVA_EXE%" goto execute

echo.
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.

goto fail

:execute
@rem Setup the command line

set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar


@rem Execute Gradle
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %*

:end
@rem End local scope for the variables with windows NT shell
if "%ERRORLEVEL%"=="0" goto mainEnd

:fail
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
rem the _cmd.exe /c_ return code!
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
exit /b 1

:mainEnd
if "%OS%"=="Windows_NT" endlocal

:omega
@rem
@rem Copyright 2015 the original author or authors.
@rem
@rem Licensed under the Apache License, Version 2.0 (the "License");
@rem you may not use this file except in compliance with the License.
@rem You may obtain a copy of the License at
@rem
@rem https://www.apache.org/licenses/LICENSE-2.0
@rem
@rem Unless required by applicable law or agreed to in writing, software
@rem distributed under the License is distributed on an "AS IS" BASIS,
@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@rem See the License for the specific language governing permissions and
@rem limitations under the License.
@rem

@if "%DEBUG%" == "" @echo off
@rem ##########################################################################
@rem
@rem Gradle startup script for Windows
@rem
@rem ##########################################################################

@rem Set local scope for the variables with windows NT shell
if "%OS%"=="Windows_NT" setlocal

set DIRNAME=%~dp0
if "%DIRNAME%" == "" set DIRNAME=.
set APP_BASE_NAME=%~n0
set APP_HOME=%DIRNAME%

@rem Resolve any "." and ".." in APP_HOME to make it shorter.
for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi

@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m"

@rem Find java.exe
if defined JAVA_HOME goto findJavaFromJavaHome

set JAVA_EXE=java.exe
%JAVA_EXE% -version >NUL 2>&1
if "%ERRORLEVEL%" == "0" goto execute

echo.
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.

goto fail

:findJavaFromJavaHome
set JAVA_HOME=%JAVA_HOME:"=%
set JAVA_EXE=%JAVA_HOME%/bin/java.exe

if exist "%JAVA_EXE%" goto execute

echo.
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.

goto fail

:execute
@rem Setup the command line

set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar


@rem Execute Gradle
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %*

:end
@rem End local scope for the variables with windows NT shell
if "%ERRORLEVEL%"=="0" goto mainEnd

:fail
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
rem the _cmd.exe /c_ return code!
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
exit /b 1

:mainEnd
if "%OS%"=="Windows_NT" endlocal

:omega
2 changes: 2 additions & 0 deletions TestModels/aws-sdks/sqs/runtimes/net/SQS.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@
<TargetFrameworks>net6.0</TargetFrameworks>
<LangVersion>10</LangVersion>
<EnableDefaultCompileItems>false</EnableDefaultCompileItems>
<GenerateAssemblyInfo>false</GenerateAssemblyInfo>
<GenerateTargetFrameworkAttribute>false</GenerateTargetFrameworkAttribute>
</PropertyGroup>

<ItemGroup>
Expand Down
Loading

0 comments on commit b7cec71

Please sign in to comment.