Skip to content

Commit 10e908e

Browse files
authored
chore(ci): Update Rust CI to use tip of Dafny's feat-rust branch (#472)
Updates the Rust CI to use the tip of Dafny's `feat-rust` branch. To make this work: * Reverts all patches to `implementation_from_dafny.rs` as the latest commit fixes all the bugs we were working around. * Also removes those files from git and ignores them from hence forth! * Also tweaks polymorph to not delete this file from StandardLibrary (which is why the patch file was creating it from scratch) * Updates the snapshot of `dafny_runtime_rust` to match. * Replaces various uses of `dafny_runtime_rust::UpcastTo` with `dafny_runtime_rust::upcast_object()(...)` * Also implements `UpcastObject` for some of our types as neeeded. * Updates all patch files (using a local edit to the `RustTestModels` test runner!)
1 parent 4afe950 commit 10e908e

93 files changed

Lines changed: 798 additions & 14846 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/workflows/pull.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ jobs:
4949
# Rust code generation is under development and depends on pending changes to the
5050
# Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
5151
dafny-version:
52-
- ebe9aa5592bea6c0a7ed3fc204db2fb8addf0661
52+
- f82ce12a800efddb22c987be0adb559752c7b6b9
5353
uses: ./.github/workflows/test_models_rust_tests.yml
5454
with:
5555
dafny: ${{ matrix.dafny-version }}

.github/workflows/push.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ jobs:
5151
# Rust code generation is under development and depends on pending changes to the
5252
# Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
5353
dafny-version:
54-
- ebe9aa5592bea6c0a7ed3fc204db2fb8addf0661
54+
- f82ce12a800efddb22c987be0adb559752c7b6b9
5555
uses: ./.github/workflows/test_models_rust_tests.yml
5656
with:
5757
dafny: ${{ matrix.dafny-version }}

TestModels/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
# Dafny Generated Rust
1313
# (Rust code generation is incomplete so we're patching and checking in for now)
1414
#**/runtimes/rust
15+
**/implementation_from_dafny.rs
1516
# Cargo.lock files should only be committed for binaries, not libraries
1617
**/Cargo.lock
1718

TestModels/Aggregate/codegen-patches/rust/dafny-4.5.0.patch

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
diff --git b/TestModels/Aggregate/runtimes/rust/src/client.rs a/TestModels/Aggregate/runtimes/rust/src/client.rs
22
new file mode 100644
3-
index 00000000..d5fef505
3+
index 00000000..96a89e4d
44
--- /dev/null
55
+++ a/TestModels/Aggregate/runtimes/rust/src/client.rs
66
@@ -0,0 +1,43 @@
@@ -39,7 +39,7 @@ index 00000000..d5fef505
3939
+ ));
4040
+ }
4141
+ Ok(Self {
42-
+ dafny_client: ::dafny_runtime::UpcastTo::<dafny_runtime::Object<(dyn ::simple_aggregate_dafny::r#_simple_daggregate_dinternaldafny_dtypes::ISimpleAggregateClient + 'static)>>::upcast_to(inner.Extract()),
42+
+ dafny_client: ::dafny_runtime::upcast_object()(inner.Extract()),
4343
+ })
4444
+ }
4545
+}
@@ -109,7 +109,7 @@ index 00000000..b5acb2be
109109
+pub mod structure_list_element;
110110
diff --git b/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate.rs a/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate.rs
111111
new file mode 100644
112-
index 00000000..1918663b
112+
index 00000000..8db680b5
113113
--- /dev/null
114114
+++ a/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate.rs
115115
@@ -0,0 +1,32 @@
@@ -123,7 +123,7 @@ index 00000000..1918663b
123123
+) -> ::std::rc::Rc<::simple_aggregate_dafny::r#_simple_daggregate_dinternaldafny_dtypes::Error> {
124124
+ match value {
125125
+ crate::operation::get_aggregate::GetAggregateError::Unhandled(unhandled) =>
126-
+ ::std::rc::Rc::new(::simple_aggregate_dafny::r#_simple_daggregate_dinternaldafny_dtypes::Error::Opaque { obj: ::dafny_runtime::UpcastTo::<::dafny_runtime::Object<dyn Any>>::upcast_to(::dafny_runtime::object::new(unhandled)) })
126+
+ ::std::rc::Rc::new(::simple_aggregate_dafny::r#_simple_daggregate_dinternaldafny_dtypes::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
127127
+ }
128128
+}
129129
+
@@ -401,7 +401,7 @@ index 00000000..0a0bee21
401401
+}
402402
diff --git b/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate_known_value_test.rs a/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate_known_value_test.rs
403403
new file mode 100644
404-
index 00000000..e013077c
404+
index 00000000..a128f451
405405
--- /dev/null
406406
+++ a/TestModels/Aggregate/runtimes/rust/src/conversions/get_aggregate_known_value_test.rs
407407
@@ -0,0 +1,39 @@
@@ -418,7 +418,7 @@ index 00000000..e013077c
418418
+ unhandled,
419419
+ ) => ::std::rc::Rc::new(
420420
+ ::simple_aggregate_dafny::r#_simple_daggregate_dinternaldafny_dtypes::Error::Opaque {
421-
+ obj: ::dafny_runtime::UpcastTo::<::dafny_runtime::Object<dyn Any>>::upcast_to(
421+
+ obj: ::dafny_runtime::upcast_object()(
422422
+ ::dafny_runtime::object::new(unhandled),
423423
+ ),
424424
+ },
@@ -1007,10 +1007,10 @@ index 00000000..ec89cbec
10071007
+pub(crate) mod sealed_unhandled;
10081008
diff --git b/TestModels/Aggregate/runtimes/rust/src/error/sealed_unhandled.rs a/TestModels/Aggregate/runtimes/rust/src/error/sealed_unhandled.rs
10091009
new file mode 100644
1010-
index 00000000..9d21fbd6
1010+
index 00000000..cce22d1c
10111011
--- /dev/null
10121012
+++ a/TestModels/Aggregate/runtimes/rust/src/error/sealed_unhandled.rs
1013-
@@ -0,0 +1,22 @@
1013+
@@ -0,0 +1,26 @@
10141014
+// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
10151015
+/// This struct is not intended to be used.
10161016
+///
@@ -1033,6 +1033,10 @@ index 00000000..9d21fbd6
10331033
+ pub(crate) source: ::aws_smithy_runtime_api::box_error::BoxError,
10341034
+ pub(crate) meta: ::aws_smithy_types::error::metadata::ErrorMetadata,
10351035
+}
1036+
+
1037+
+impl ::dafny_runtime::UpcastObject<dyn ::std::any::Any> for Unhandled {
1038+
+ ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
1039+
+}
10361040
diff --git b/TestModels/Aggregate/runtimes/rust/src/lib.rs a/TestModels/Aggregate/runtimes/rust/src/lib.rs
10371041
new file mode 100644
10381042
index 00000000..89dacaff

0 commit comments

Comments
 (0)