generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Description
Since Dafny itself doesn't support building code into separate crates, smithy-dafny works around this by translating and generating all code from all library dependencies at once. This is an issue for --local-service-test: all of the smithy-dafny TestModels always pass this when building each model, but some downstream projects like https://github.com/aws/aws-encryption-sdk only pass this option on separate projects like "TestVectors".
(TODO: more details, but that might go better under designs/rust instead)
To workaround these limitations, there are two separate hacks necessary (using https://github.com/aws/aws-encryption-sdk as a working example):
- Because the separate testing project reuses the source project Smithy model, there's no opportunity to provide extra
@localService#dependencies, which is how the Rust code generation fills in the right Dafny include statements. Therefore they have to be patched onto the generated code: https://github.com/aws/aws-encryption-sdk/blob/mainline/TestVectors/dafny/TestVectors/Model/AwsCryptographyEncryptionSdkTypesWrapped.dfy#L5-L8 - Because all transitive dependencies are built at once,
--local-service-testgets applied to all dependent Smithy models, which doesn't work in general because the wrapped clients depend on externs that won't be present on the root project. To work around this, the ESDK uses sed to comment out the wrapped clients on the dependent clients: https://github.com/aws/aws-encryption-sdk/blob/mainline/TestVectors/Makefile#L156-L157
Metadata
Metadata
Assignees
Labels
No labels