Skip to content

Commit d59ef8b

Browse files
lucasmcdonald3lucasmcdonald3
authored
docs: Create developer guide for Python, remove leading whitespace from designs folder name (#783)
1 parent 385a6e8 commit d59ef8b

File tree

6 files changed

+318
-0
lines changed

6 files changed

+318
-0
lines changed

‎ designs/README.MD renamed to ‎designs/README.MD

File renamed without changes.

‎designs/codegen/python/design-codegen.md

+67
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
# Concepts
2+
3+
## Differences between Smithy-Dafny Python projects and other languages
4+
5+
### Interpreted vs. Compiled
6+
7+
Languages like Java and .NET are compiled, but Python is interpreted. This results in some important differences in Python:
8+
9+
1. Python imports modules based on filepath.
10+
If a module is located at `my_project/internaldafny/generated/SomeModule.py`, it must be imported as `my_project.internaldafny.generated.SomeModule`. (There are some hacks to work around this, but these are hacks.)
11+
This contrasts with Java/.NET, which import modules based on declared namespace. (ex.) Java might have a file at `dafny-generated/SomeModule/SomeClass.java` , but that class declares `package SomeModule` . To import this class, you would write `import SomeModule.SomeClass`.
12+
2. Python links externs to generated code at runtime.
13+
When a Dafny-Python module is imported, it runs initialization glue code that will 1) import all of its generated Dafny (in a topological order to avoid circular dependencies), 2) import all of its externs.
14+
Then, each extern class must 1) extend the generated class, 2) override the generated class with the extern class.
15+
This contrasts with Java/.NET, where the externs extend partial/base generated classes, and link together at compile time.
16+
17+
## Smithy-Python Integration
18+
19+
### Smithy-Python “Hard Fork”
20+
21+
Smithy-Dafny relies on a “hard fork” of Smithy-Python.
22+
23+
Alternatives rejected include:
24+
25+
- **Submodule; create a regular fork of Smithy-Python.**
26+
- `smithy-lang` can’t create its own fork of Smithy-Python because `smithy-lang/smithy-python` is the real Smithy-Python
27+
- It would be improper to add some prefix/suffix to make the names not collide because `smithy-lang` is a shared AWS resource, and doing this would pollute the org’s repositories
28+
- It would be improper to have Smithy-Dafny reference some other owner’s fork of Smithy-Python because both projects are under `smithy-lang`.
29+
- **Submodule; create a non-main branch on Smithy-Python**. This would add churn to Smithy-Dafny’s development process. Developers would need to get a change reviewed by the Smithy-Python team before they can deploy a change through Smithy-Dafny. It would also be improper to refer to a non-main branch.
30+
31+
### Smithy-Dafny code integration with Smithy-Python
32+
33+
Smithy-Dafny generates Python code by integrating with [Smithy-Python](https://github.com/smithy-lang/smithy-python/tree/develop/codegen).
34+
Smithy-Dafny integrates with Smithy-Python via two integration mechanisms:
35+
36+
1. Smithy’s [plugin Integration](https://smithy.io/2.0/guides/building-codegen/making-codegen-pluggable.html) interface. This is used by code in a protocol’s `customize/` directory. See [LocalService’s customize directory](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize) as an example.
37+
Codegen that uses this integration includes:
38+
1. Override the HTTP protocol in Smithy-Python and generate protocols for local services, wrapped local services, and Dafny AWS SDK shims
39+
2. Write custom content to some files from the `customize` directive
40+
2. Extending Smithy-Python classes and overriding its methods. This is used by code in a protocol’s `extensions/` directory. See [LocalService’s extensions directory](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions) as an example.
41+
Codegen that uses this integration includes:
42+
1. Overriding Smithy-Python’s client class generation to generate a synchronous client
43+
2. Overriding Smithy-Python’s shape writer to handle Smithy-Dafny-specific shapes (Positional shapes, Reference shapes, etc)
44+
45+
Smithy-Dafny’s Python integration uses both mechanisms, but could probably be refactored to only use one or the other. A refactor to only extend Smithy-Python’s classes would be lower-lift than only implementing the plugin interface. There isn’t a pressing need to do this refactor, other than simplification.
46+
47+
#### **Limitations of the Plugin Interface**
48+
49+
The plugin interface has some gaps that prevent Smithy-Dafny’s Python codegen from exclusively using it. This is a non-exhaustive list:
50+
51+
1. **Doesn’t support changing shape generation.** Smithy-Python doesn’t recognize certain shapes, like shapes with Positional and Reference traits. (We wouldn’t expect it to; these are Smithy-Dafny-specific traits.) The plugin interface doesn’t let a plugin override a codegen’s shape generation to change how shapes are generated.
52+
2. **Doesn’t support changing symbol generation.** Smithy-Python doesn’t understand how to generate references to symbols in other namespaces (what Smithy-Dafny calls “Dependencies”). The plugin interface doesn’t let a plugin override a codegen’s symbol generation to change how shapes are referenced.
53+
3. **Doesn’t support overriding client generation.** Smithy-Python generates an async client, while Smithy-Dafny-Python requires a synchronous client. The plugin interface doesn’t let a plugin override a codegen’s client generation.
54+
4. **Protocols without shapes.** Smithy-Dafny generates shims for AWS SDKs and wrapped local services. These protocols don’t require shape generation. Smithy-Python always generates all shapes it visits.
55+
56+
The workarounds to these involve extending Smithy-Python’s classes to work around these limitations.
57+
58+
#### **Extending Smithy-Python’s implementation**
59+
60+
Where Smithy-Dafny directly extends Smithy-Python, it prefers to do so by modifying access levels in Smithy-Python (e.g., making private methods protected or public), or by refactoring to introduce a new method that can be overridden via class extension.
61+
62+
This appears to be discouraged by Smithy. Smithy code generators tend to declare classes as `private` and/or `final` , suggesting class extensions aren’t preferred.
63+
64+
#### Future Work
65+
66+
1. Upstreaming changes from Smithy-Dafny’s Smithy-Python fork; relying on Smithy-Python upstream
67+
1. This should probably wait until Smithy-Python’s interfaces are finalized. Right now, Smithy-Python notes “WARNING: All interfaces are subject to change”. It might cause unneeded churn to integrate with Smithy-Python more closely now if Smithy-Dafny needs to update again later.

‎ designs/detailed-diagrams.md renamed to ‎designs/detailed-diagrams.md

File renamed without changes.

‎docs/getting-started.md

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
# Makefile Variables
2+
3+
To create a Smithy-Dafny project, you will need a Makefile with the following variables defined.
4+
These variables apply to all languages.
5+
Some languages have additional required variables.
6+
7+
- `PROJECT_SERVICES`: List of names of each local service in the project.
8+
- `PROJECT_INDEX`: This is a space-delimited list of `Index.dfy` files for your dependencies.
9+
- `PROJECT_DEPENDENCIES`: List of top-level directory names for dependencies for the project.
10+
- `SERVICE_NAMESPACE_<service>`: For each service in `PROJECT_SERVICES`, this is the Smithy namespace for shapes attached to that local service.
11+
- `SERVICE_DEPS_<service>`: For each service in `PROJECT_SERVICES`, this is the list of paths to `Model/` directories for dependencies of that service.
12+
13+
Examples:
14+
15+
- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project sets all of these variables with multiple dependencies.

‎docs/nested-externs.md

+78
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
#### Modules with “nested” extern attributes
2+
3+
The content in this file is relevant for Smithy-Dafny Python and Go projects.
4+
5+
Modules with a “nested” extern attribute (“nested extern modules”) can’t be used with Python or Go.
6+
A "nested" extern attribute has `.`s in it. (e.g. `{:extern "my.namespace.my.project.internaldafny}`).
7+
8+
Ideally, one wouldn’t define nested extern modules.
9+
However, some projects that build for Java, NET, and Rust use nested extern attributes to prefix generated Dafny code with an "internal" prefix.
10+
For legacy support, Smithy-Dafny supports using `sed` to strip away the nested extern attribute.
11+
12+
**Simple “nested” externs**
13+
For an existing project `MyProject` that uses a nested extern string like `"my.namespace.my.project.internaldafny"` , the Makefile for the project should be updated as follows:
14+
15+
```
16+
ENABLE_EXTERN_PROCESSING=1 # This MUST go before `include ``../``SharedMakefileV2``.``mk
17+
18+
include ../SharedMakefileV2.mk`
19+
20+
...
21+
22+
TYPES_FILE_PATH=Model/MyProject.dfy
23+
TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.project.internaldafny.types\" } MyProjectTypes"
24+
TYPES_FILE_WITHOUT_EXTERN_STRING="module MyProjectTypes"
25+
26+
INDEX_FILE_PATH=src/Index.dfy
27+
INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.project.internaldafny\" } MyProject refines AbstractMyProjectService {"
28+
INDEX_FILE_WITHOUT_EXTERN_STRING="module MyProject refines MyProject {"
29+
```
30+
31+
This setup will work for “simple” projects that only define nested extern modules in `Index.dfy` and the types file.
32+
33+
Examples:
34+
35+
- [Constraints TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/Constraints/Makefile). Almost all TestModels are “simple.”
36+
- [DDB TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/aws-sdks/ddb/Makefile). All AWS SDK projects should be simple.
37+
38+
**Complex “nested” externs**
39+
Some projects use nested extern modules in files other than `Index.dfy` and the types file.
40+
For these “complex” projects, you will need to define new sed strings _and_ override the default Makefile targets.
41+
If you have a file `MySpecialFile.dfy` that requires sed replacement, you will need to override some targets:
42+
43+
```
44+
ENABLE_EXTERN_PROCESSING=1
45+
46+
...
47+
48+
MY_SPECIAL_FILE_FILE_PATH=src/MySpecialFile.dfy
49+
MY_SPECIAL_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.special.file.internaldafny\" } MySpecialFile"
50+
MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING="module MySpecialFile"
51+
52+
...
53+
54+
# Override target; handle both the Index.dfy file and the new file
55+
_sed_index_file_add_extern:
56+
$(MAKE) _sed_file SED_FILE_PATH=$(MY_SPECIAL_FILE_FILE_PATH) SED_BEFORE_STRING=$(MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MY_SPECIAL_FILE_WITH_EXTERN_STRING)
57+
$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITH_EXTERN_STRING)
58+
59+
_sed_index_file_remove_extern:
60+
$(MAKE) _sed_file SED_FILE_PATH=$(MY_SPECIAL_FILE_FILE_PATH) SED_BEFORE_STRING=$(MY_SPECIAL_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING)
61+
$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING)
62+
```
63+
64+
Examples:
65+
66+
- [MultipleModels TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/MultipleModels/Makefile). Any Smithy-Dafny project with multiple local services is “Complex.”
67+
- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project has multiple local services, but also applies nested extern attributes to some of its other modules (SynchronizedLocalCMC and StormTrackingCMC).
68+
69+
The following Makefile targets exist and can be overridden:
70+
71+
```
72+
_sed_types_file_remove_extern
73+
_sed_index_file_remove_extern
74+
_sed_wrapped_types_file_remove_extern
75+
_sed_types_file_add_extern
76+
_sed_index_file_add_extern
77+
_sed_wrapped_types_file_add_extern
78+
```

‎docs/python/getting-started.md

+158
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
# Getting Started
2+
3+
To install dependencies to build a Smithy-Dafny project in Python, first run
4+
5+
```
6+
make setup_python
7+
```
8+
9+
# Makefile Variables
10+
11+
To build a Smithy-Dafny Python project, you will need to add the following variables to your Makefile.
12+
13+
- `PYTHON_MODULE_NAME`: The name of the Python module for generated code.
14+
- `TRANSLATION_RECORD_PYTHON` : For each dependency (including StandardLibrary), the path to the generated `.dtr` file for that dependency’s generated Dafny code.
15+
- `PYTHON_DEPENDENCY_MODULE_NAMES`: For each dependency, this is a map from a Smithy namespace to the `PYTHON_MODULE_NAME` variable for that dependency.
16+
17+
Examples:
18+
19+
- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project sets all of these variables with multiple dependencies.
20+
21+
### Smithy-Dafny Python Project Structure
22+
23+
(Assuming you have made the Makefile updates specified above, then:)
24+
25+
These commands will set up the base file structure for a Python project:
26+
27+
1. `make polymorph_dafny`
28+
2. `make polymorph_python`
29+
3. `make transpile_python`
30+
31+
This structure follows:
32+
33+
```
34+
MyProject/runtimes/python/
35+
├── src/
36+
│ └── my_project/
37+
│ ├── __init__.py
38+
│ ├── internaldafny/
39+
│ │ ├── generated/
40+
│ │ │ ├── [all Dafny-generated source code from `make transpile_python`]
41+
│ │ │ └── dafny_src-py.dtr
42+
│ │ └── extern/
43+
│ │ ├── __init__.py
44+
│ │ └── [all manually written externs]
45+
│ └── smithygenerated/
46+
│ └── my_project/
47+
│ └── [all Smithy-Dafny-generated source code from `make polymorph_python`]
48+
├── test/
49+
│ ├── __init__.py # empty
50+
│ └── internaldafny/
51+
│ ├── __init__.py # empty
52+
│ ├── test_dafny_wrapper.py
53+
│ ├── generated/
54+
│ │ ├── [all Dafny-generated test code from `make transpile_python`]
55+
│ └── extern/
56+
│ ├── __init__.py
57+
│ └── [all manually test written externs]
58+
├── pyproject.toml
59+
├── tox.ini
60+
└── .gitignore
61+
```
62+
63+
- `src/` : Project source code.
64+
- `my_project/` : Python module that will be distributed to end users. This is the top-level name of the package that is imported by users. (ex. `import my_project`). The top-level name is defined by the Smithy-Dafny project’s Makefile’s `PYTHON_MODULE_NAME` variable; see [Makefile Updates](https://quip-amazon.com/SahBABLOQkya#temp:C:KIXe7b270945e2b419180867c04e).
65+
- `__init__.py`: Initializes generated Dafny code and performs optional project setup. See Appendix.
66+
- `internaldafny/`: Dafny-generated code and externs.
67+
- `generated/`: Dafny-generated code.
68+
- `dafny_src-py.dtr`: [Dafny translation record](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dtr-files) for this project’s generated code. This is critical to let other projects use this project as a dependency. Other projects will read this file to determine how to refer to this project’s generated Dafny code.
69+
- `extern/`: Holds manually-written externs. You don’t need this if you don’t have any source externs.
70+
- `__init__.py` : Initializes externs. See Appendix.
71+
- `smithygenerated/`: Smithy-Dafny generated code.
72+
- `my_project/`: Smithy-generated code for a LocalService’s namespace.
73+
- Note: If a Smithy-Dafny project has multiple LocalServices, there will be multiple folders in this directory. Each folder will named be the LocalService’s Smithy namespace converted to snakecase. For an example, see [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/tree/main/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_materialproviders/smithygenerated).
74+
- `test/`: Project test code.
75+
- `internaldafny/`: Dafny tests.
76+
- `test_dafny_wrapper.py`: See Appendix.
77+
- `generated/` : Dafny-generated test code.
78+
- `extern/`: Holds manually-written test externs. You don’t need this if you don’t have any test externs.
79+
- Any other test groupings, ex. `functional/`: Other tests for the project that aren’t Dafny-generated. For an example, See [Crypto Tools’ AwsCryptographyPrimitives](https://github.com/aws/aws-cryptographic-material-providers-library/tree/main/AwsCryptographyPrimitives/runtimes/python/test).
80+
- `pyproject.toml` : Project configuration and dependencies file. See Appendix.
81+
- `tox.ini` : Test configuration file. See Appendix.
82+
83+
# Externs
84+
85+
In Python, Dafny externs are not loaded at compile time because "compile time" doesn't exist in Python. Python code is interpreted, not compiled.
86+
Smithy-Dafny Python projects use this pattern to link extern code when the Smithy-Dafny module is loaded.
87+
88+
Smithy-Dafny Python extern implementations must:
89+
90+
1. Extend the generated class, if there is one
91+
2. “Export” itself to the generated class
92+
1. **Why?** The Dafny-generated code expects that generated code behaves like it has extern code. The extern class that extends the generated class has this behavior. Overwriting the generated class with the extern class matches Dafny’s expectation.
93+
94+
Annotated sample implementation:
95+
96+
```
97+
# If this is generated by `transpile_python`
98+
import my_project.internaldafny.generated.ModuleWithExtern.SomeExternCLass
99+
# Your extern might need code from the generated module
100+
from my_project.internaldafny.generated.ModuleWithExtern import *
101+
102+
# Extern should extend generated class, if one is generated
103+
class SomeExternClass(my_project.internaldafny.generated.SomeExternClass):
104+
...
105+
106+
# Export extern class to generated class
107+
my_project.internaldafny.generated.ModuleWithExtern.SomeExternClass = SomeExternClass
108+
```
109+
110+
This extern file should be placed at `my_project/internaldafny/extern`.
111+
112+
Every project that has externs must also have an `__init__.py` located at `my_project/internaldafny/extern` with the code at [TODO].
113+
114+
Examples:
115+
116+
- [Extern TestModel](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern).
117+
118+
# Appendix
119+
120+
## Code Samples
121+
122+
### Project Initialization Files
123+
124+
Every Smithy-Dafny project should have a file at `src/your_project/__init__.py` with the following content:
125+
126+
```
127+
# Initialize generated Dafny
128+
from .internaldafny.generated import module_
129+
130+
# Initialize externs
131+
# (If you don't have externs, omit this import)
132+
from .internaldafny import extern
133+
```
134+
135+
This file is executed when your project is imported.
136+
137+
This file primarily exists to initialize a project’s Dafny code.
138+
139+
First, this file initializes generated Dafny by importing the generated `module_.py`.
140+
`module_.py` is a Dafny-generated file that imports a project’s generated Dafny topologically (i.e. avoiding circular dependencies in import dependencies).
141+
142+
Second, this file initializes externs.
143+
(This order is important; externs rely on generated code, and the generated code must be imported first to avoid circular dependencies.)
144+
145+
To use externs in source code, you must add a file at `my_project/internaldafny/extern/__init__.py`.
146+
This file is executed by the root `__init__.py` when the project is imported.
147+
This file will import externs.
148+
149+
```
150+
from . import (
151+
MyExtern
152+
)
153+
```
154+
155+
Examples:
156+
157+
- [Constraints TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/Constraints/runtimes/python/src/simple_constraints/__init__.py). This has no externs, so the `import extern` line is omitted.
158+
- [Extern TestModel](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/Extern/runtimes/python/src/simple_dafnyextern). This has both generated and extern code.

0 commit comments

Comments
 (0)