Skip to content

Commit

Permalink
Update fixed feat-rust commit in CI, test tip of feat-rust in nightly (
Browse files Browse the repository at this point in the history
…#506)

Dafny's `feat-rust` branch made forwards-thinking changes to the Rust code generator, mainly to assume for now that all generated code is contained in a single crate. This breaks our current design for how smithy-dafny libraries are constructed. This change refactors the structure of smithy-dafny `runtimes/rust` generated projects to fit this limitation, at least for now.

* Because Dafny outputs Rust code assuming that it will live at the top-level namespace, `Cargo.toml` files now specify that `implementation_from_dafny.rs` is the main `lib` file instead of the manually-written `lib.rs` files so far. Instead we apply a patch to `implementation_from_dafny.rs` to declare the additional modules.
* Rather than depend on the smithy-dafny StandardLibrary code as a separate crate, modified the shared makefile to not use `-library` when compiling to Rust, so that included Dafny code is just inlined as it is transpiled.
  * This also unfortunately means we have to include the `conversions` module from the StandardLibrary inline in each library.
* As a side-effect of the one-crate assumption, compiling Dafny tests to Rust integration tests no longer works (since those are implicitly separate crates). Instead we make use of the new feature on `feat-rust` to compile Dafny `{:test}` attributes directly to Rust `#[test]` attributes.
  * This required customizing the shared makefile further for Rust, to (optionally) include the Dafny test files as well as source when transpiling to Rust.

Also improved the Dafny nightly build to test on Rust using the latest commit from `feat-rust`, so that any other similar breaking changes are caught in the future.

To review this PR, it should suffice to focus on the SmithyDafnyMakefile.mk changes and skim the search-and-replace changes to `kms-lite` and one other non-SDK test model.
  • Loading branch information
robin-aws authored Aug 13, 2024
1 parent a1603bd commit 89cbe7f
Show file tree
Hide file tree
Showing 267 changed files with 49,269 additions and 4,999 deletions.
21 changes: 12 additions & 9 deletions .github/workflows/nightly_dafny.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,21 +27,24 @@ jobs:
uses: ./.github/workflows/test_models_net_tests.yml
with:
dafny: "nightly-latest"
# This workflow is pinned to a specific commit from a feature branch
# that's "ahead" of master, so there's no point in testing against nightly prereleases for now.
# dafny-nightly-rust:
# if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
# uses: ./.github/workflows/test_models_rust_tests.yml
# with:
# dafny: "nightly-latest"
# This workflow is normally pinned to a specific commit from the feat-rust feature branch.
# In the spirit of nightly, here we test against the tip of feat-rust
# (built from source instead of downloaded from nuget as a prerelease)
# to catch pending regressions.
dafny-nightly-rust:
if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
uses: ./.github/workflows/test_models_rust_tests.yml
with:
dafny: "feat-rust"

cut-issue-on-failure:
runs-on: ubuntu-latest
needs: [
needs:
[
dafny-nightly-verification,
dafny-nightly-java,
dafny-nightly-net,
# dafny-nightly-rust,
dafny-nightly-rust,
]
if: ${{ always() && contains(needs.*.result, 'failure') }}
env:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/pull.yml
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ jobs:
# Rust code generation is under development and depends on pending changes to the
# Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
dafny-version:
- f82ce12a800efddb22c987be0adb559752c7b6b9
- 2412e865d1d04ea70711f4dfaf885fcdc5c338c8
uses: ./.github/workflows/test_models_rust_tests.yml
with:
dafny: ${{ matrix.dafny-version }}
2 changes: 1 addition & 1 deletion .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ jobs:
# Rust code generation is under development and depends on pending changes to the
# Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
dafny-version:
- f82ce12a800efddb22c987be0adb559752c7b6b9
- 2412e865d1d04ea70711f4dfaf885fcdc5c338c8
uses: ./.github/workflows/test_models_rust_tests.yml
with:
dafny: ${{ matrix.dafny-version }}
37 changes: 10 additions & 27 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -516,48 +516,31 @@ test_java:

########################## Rust targets

# Note that transpile_dependencies_test_rust is necessary
# only because we are patching test code in the StandardLibrary,
# so we don't transpile that code then the recursive call to polymorph_rust
# on the StandardLibrary will fail because the patch does not apply.
transpile_rust: | transpile_implementation_rust transpile_test_rust transpile_dependencies_rust transpile_dependencies_test_rust
# TODO: blah blah Rust only supports a single crate for everything
transpile_rust: | transpile_implementation_rust transpile_dependencies_rust

transpile_implementation_rust: TARGET=rs
transpile_implementation_rust: OUT=implementation_from_dafny
transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX)
transpile_implementation_rust: TEST_INDEX=$(RUST_TEST_INDEX)
# The Dafny Rust code generator is not complete yet,
# so we want to emit code even if there are unsupported features in the input.
transpile_implementation_rust: DAFNY_OPTIONS=-emitUncompilableCode
transpile_implementation_rust: _transpile_implementation_all _mv_implementation_rust

transpile_test_rust: TARGET=rs
transpile_test_rust: OUT=tests_from_dafny
transpile_test_rust: SRC_INDEX=$(RUST_SRC_INDEX)
transpile_test_rust: TEST_INDEX=$(RUST_TEST_INDEX)
# The Dafny Rust code generator is not complete yet,
# so we want to emit code even if there are unsupported features in the input.
transpile_test_rust: DAFNY_OPTIONS=-emitUncompilableCode
transpile_test_rust: _transpile_test_all _mv_test_rust
# TODO:
transpile_implementation_rust: TRANSPILE_DEPENDENCIES=
transpile_implementation_rust: STD_LIBRARY=
transpile_implementation_rust: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
transpile_implementation_rust: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust

transpile_dependencies_rust: LANG=rust
transpile_dependencies_rust: transpile_dependencies

transpile_dependencies_test_rust: LANG=rust
transpile_dependencies_test_rust: transpile_dependencies_test

_mv_implementation_rust:
mkdir -p runtimes/rust/src
# TODO: Currently need to insert an import of the the StandardLibrary.
python -c "import sys; data = sys.stdin.buffer.read(); sys.stdout.buffer.write(data.replace(b'\npub mod', b'\npub use dafny_standard_library::implementation_from_dafny::*;\n\npub mod', 1) if b'\npub mod' in data else data)" \
< implementation_from_dafny-rust/src/implementation_from_dafny.rs > runtimes/rust/src/implementation_from_dafny.rs
mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs
rustfmt runtimes/rust/src/implementation_from_dafny.rs
rm -rf implementation_from_dafny-rust
_mv_test_rust:
rm -f runtimes/rust/tests/tests_from_dafny/mod.rs
mkdir -p runtimes/rust/tests/tests_from_dafny
mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/tests/tests_from_dafny/mod.rs
rustfmt runtimes/rust/tests/tests_from_dafny/mod.rs
rm -rf tests_from_dafny-rust

build_rust:
cd runtimes/rust; \
Expand Down
1 change: 0 additions & 1 deletion TestModels/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@
# Dafny Generated Rust
# (Rust code generation is incomplete so we're patching and checking in for now)
#**/runtimes/rust
**/implementation_from_dafny.rs
# Cargo.lock files should only be committed for binaries, not libraries
**/Cargo.lock

Expand Down
Loading

0 comments on commit 89cbe7f

Please sign in to comment.