-
Notifications
You must be signed in to change notification settings - Fork 8
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Support Dafny tests on test models for Rust #460
Conversation
…thy-lang/smithy-dafny into robin-aws/dafny-tests-on-rust # Conflicts: # TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch # TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs # TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/client.rs # TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs # TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/implementation_from_dafny.rs # TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs # TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch # codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The error handling code in here is all over the map, please help me use some cleaner idioms :) I can't use ?
in general since r#_Wrappers_Compile::Result
is not a Rust Result
, but perhaps we can use Result.map_err
somehow?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Did the best I could with this. :)
Issue #, if available:
Resolves #458
Description of changes:
Supports compiling the common Dafny tests in a test model for Rust. This involved having to change some properties of how we lay out the Rust crates:
Removed thedafny_impl
sub-crate and movedimplementation_from_dafny.rs
into the mainsrc
directory - hence replacing::simple_boolean_dafny
withcrate::implementation_from_dafny
everywhere. I originally had this separated to better divide Dafny-generated code from Smithy-generated code, but it made implementing externs hard/impossible, and Dafny tests make use of "wrapped services" which are essentially testing-only extern shims.use ::simple_boolean_dafny::*;
anduse simple_boolean::*;
imports into the compiled tests. This is equivalent to thepub use dafny_standard_library::implementation_from_dafny::*;
import the Makefile is adding, and will be replaced by a Dafny feature named something like--rust-module-name
as some other other supported languages already have.tests/tests_from_dafny/_wrapped.rs
wrapped::client::Client
with the implementation of the "wrapped service", which is implementing the Dafny-client interface using the Rust idiomatic client.wrapped-client
feature which the Dafny-compiled integration test enables, as per Activating features for tests/benchmarks rust-lang/cargo#2911 (comment)Removedasync
from the client interfaces - we'd originally kept these for better forwards-compatibility, but AFAICT it's impossible to implement the synchronous Dafny-generated trait methods with async methods. This just means that in the future we'll eventually have to provide separate async clients, but that's happened with the AWS SDKs frequently as well.current_thread
TokioRuntime
as per https://tokio.rs/tokio/topics/bridging instead.Raised the visibility of a few things in the main crate topub
so that thedafny_tests
integration test crate can see them - open to feedback here on whether it's reasonable or we should find a better solution.Not ready to merge yet because this relies on a newer Dafny feature branch commit, which I'll tackle in a separate PR first since it will be noisy to update all the patch files.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.