Skip to content

Commit 790bd4c

Browse files
robin-awsalex-chewtexastony
authored
chore: (tasty vegetarian option)-up codegen README.md file (#214)
Now provides documentation about how to build a Dafny SDK client using the Smithy plugin, along with some of the limitations and caveats therein, including how to use projection transforms to filter out unsupported features. Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Tony Knapp <[email protected]>
1 parent 118804b commit 790bd4c

File tree

2 files changed

+166
-2
lines changed

2 files changed

+166
-2
lines changed

‎codegen/README.md

+164-2
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,173 @@ This library supports the standard Smithy workflow
44
for generating a Dafny client for a given Smithy model,
55
as described in the
66
[Smithy codegen docs](https://smithy.io/2.0/guides/using-code-generation/generating-a-client.html).
7-
For now the library will only support AWS service models,
7+
8+
*WARNING: All internal and external interfaces are considered unstable and subject to change without notice.
9+
This includes the interfaces in the code generated by this library.*
10+
11+
## Limitations
12+
13+
1. Dafny supports compilation to multiple other target programming languages,
14+
but of those targets, this plugin currently only supports .NET.
15+
Experimental support for Java exists
16+
but does not yet work for arbitrary service models.
17+
2. This plugin does not yet handle all Smithy features,
18+
and may hit errors or generate incorrect code for some models.
19+
See the section below on "Using projections" for details
20+
on how to cleanly avoid unsupported features.
21+
22+
## Generating a client
23+
24+
This repository builds Dafny declarations and Dafny clients from Smithy
25+
models.
26+
27+
For now the library only supports AWS service models,
828
since the implementation will generate both Dafny code and target language code
929
to wrap existing AWS SDKs.
30+
This means only services with the `aws.api#service` trait are supported.
31+
32+
The `TestModel/sqs` package in this repo is an example of
33+
how to build a Dafny client. The steps needed to build a Dafny client
34+
are as follows:
35+
36+
1. Create a new directory for your package. For example, "foo-client".
37+
38+
2. Create a `build.gradle.kts` file with the following contents:
39+
40+
```kotlin
41+
buildscript {
42+
repositories {
43+
mavenCentral()
44+
}
45+
dependencies {
46+
"classpath"("software.amazon.smithy:smithy-cli:1.28.1")
47+
}
48+
}
49+
50+
plugins {
51+
id("software.amazon.smithy").version("0.6.0")
52+
}
53+
54+
repositories {
55+
mavenLocal()
56+
mavenCentral()
57+
}
58+
59+
dependencies {
60+
implementation("software.amazon.smithy:smithy-model:1.28.1")
61+
implementation("software.amazon.smithy:smithy-aws-traits:1.28.1")
62+
implementation("software.amazon.smithy.dafny:smithy-dafny-codegen:0.1.0")
63+
}
64+
```
65+
66+
You may need additional Smithy dependencies depending on what Smithy features
67+
your service model depends on, such as AWS-specific traits.
68+
See https://smithy.io/2.0/guides/using-code-generation/index.html for more examples.
69+
70+
Note the exact version of the `software.amazon.smithy` dependencies MAY NOT need to be
71+
`1.28.1` exactly, but MUST be consistent.
72+
73+
3. Clone the GitHub repository for [smithy-dafny](https://github.com/awslabs/smithy-dafny)
74+
somewhere nearby, being sure to initialize submodules.
75+
If this repository is still private, reach out to [email protected]
76+
for access.
77+
78+
This is necessary because it contains reusable Dafny code that
79+
the generated client will depend on, but is not yet independently distributed for
80+
shared use.
81+
82+
4. Create a `smithy-build.json` file with the following contents,
83+
substituting "smithy.example#ExampleService" with the name of the service
84+
to generate a client for, and specifying the set of target languages
85+
to support in the generated client:
86+
87+
```json
88+
{
89+
"version": "1.0",
90+
"plugins": {
91+
"dafny-client-codegen": {
92+
"edition": "2023",
93+
"service": "smithy.example#ExampleService",
94+
"targetLanguages": ["dotnet"],
95+
"includeDafnyPath": "[relative]/[path]/[to]/smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy"
96+
}
97+
}
98+
}
99+
```
100+
101+
See [`DafnyClientCodegenPluginSettings.java`](https://github.com/awslabs/smithy-dafny/blob/main-1.x/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java) for more details about plugin settings.
102+
103+
5. Create a directory named `model`. This is where all of your Smithy models
104+
will go.
105+
106+
6. Copy the model for the service into the `model` directory.
107+
The Smithy models for AWS services can be found in several Smithy-based SDK projects,
108+
such as
109+
https://github.com/aws/aws-sdk-js-v3/tree/main/codegen/sdk-codegen/aws-models.
110+
111+
7. Run `gradle build` (alternatively, you can use a
112+
[Gradle wrapper](https://docs.gradle.org/current/userguide/gradle_wrapper.html)).
113+
114+
8. The generated client can be found in `build/smithyprojections/foo-client/source/dafny-client-codegen`.
115+
116+
See [the Smithy documentation](https://smithy.io/2.0/guides/building-models/gradle-plugin.html)
117+
for more information on building Smithy projects with Gradle.
118+
119+
Note there are some caveats related to building the generated client code:
120+
121+
1. If you specified Java as a target language,
122+
the result will depend on the [dafny-java-conversion](https://github.com/awslabs/smithy-dafny/tree/main-1.x/dafny-java-conversion)
123+
library, which is also not yet published.
124+
The easiest workaround is to first run the `publishToLocalMaven` gradle task on a copy of the source for that library.
125+
126+
## Using projections
127+
128+
This plugin does not yet handle all Smithy features, especially since
129+
at the time of writing this, Dafny itself does not have a strongly
130+
idiomatic representation for concepts such as Timestamps.
131+
Fortunately, the Smithy Gradle plugin provides several
132+
["transforms"](https://smithy.io/2.0/guides/building-models/build-config.html#transforms)
133+
that can be used to filter a service model
134+
to remove unsupported shapes.
135+
136+
The following example removes all operations that transitively refer
137+
to some of the shape types that this plugin does not yet support:
138+
139+
```json
140+
{
141+
"version": "1.0",
142+
"projections": {
143+
"dafny-supported": {
144+
"transforms": [
145+
{
146+
"name": "excludeShapesBySelector",
147+
"args": {
148+
"selector": "operation :test(~> timestamp, double, float, resource)"
149+
}
150+
}
151+
],
152+
"plugins": {
153+
"dafny-client-codegen": {
154+
"service": "smithy.example#ExampleService",
155+
"targetLanguages": ["dotnet"],
156+
"includeDafnyPath": "[relative]/[path]/[to]/smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy"
157+
}
158+
}
159+
}
160+
},
161+
}
162+
```
163+
164+
Note that if you are using transformations to avoid unsupported features,
165+
the plugin has to be applied specifically to projections that use such transformations,
166+
and not at the top level were it will be applied to all projections.
167+
Otherwise the built-in "source" projection will still hit errors.
168+
169+
Refer to the Smithy documentation for more information about other transforms
170+
that might be useful, but bear in mind that removing arbitrary shapes may lead
171+
to a client that will fail to compile or not function correctly.
10172

11-
*WARNING: All internal and external interfaces are considered unstable and subject to change without notice.*
173+
## Development
12174

13175
The file layout of the library follows the
14176
[Codegen repo layout](https://smithy.io/2.0/guides/building-codegen/creating-codegen-repo.html#codegen-repo-layout)

‎dafny-java-conversion/README.md

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ idiomatic Java types to Dafny-Java types and vice versa.
55
This library assumes that Dafny will not introduce breaking changes
66
to the Dafny Runtime jar inside a major version.
77

8+
*WARNING: All internal and external interfaces are considered unstable and subject to change without notice.*
9+
810
## Set Up
911
This library depends on the `DafnyRuntime.jar`.
1012

0 commit comments

Comments
 (0)