merge

.github/workflows/nightly_dafny.yml

@@ -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:

.github/workflows/pull.yml

@@ -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 }}

.github/workflows/push.yml

@@ -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 }}

.github/workflows/smithy-dafny-conversion.yml

@@ -11,6 +11,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
       - uses: actions/setup-java@v3
         with:
           distribution: "corretto"

.github/workflows/smithy-polymorph.yml

@@ -15,6 +15,8 @@ jobs:
     runs-on: ${{matrix.os}}
     steps:
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
       - uses: actions/setup-java@v3
         with:
           distribution: "corretto"
@@ -29,6 +31,12 @@ jobs:
           # Matching the hard-coded version for the "2023" edition for now
           dafny-version: 4.1.0
 
+      - name: Install smithy-dafny-codegen dependencies locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+          build-root-directory: smithy-dafny-codegen-modules/smithy-rs
+
       - name: Execute smithy-dafny-codegen-cli tests
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_dafny_verification.yml

@@ -44,6 +44,8 @@ jobs:
           git config --global core.longpaths true
 
       - uses: actions/checkout@v2
+        with:
+          submodules: recursive
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
@@ -56,6 +58,12 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install smithy-dafny-codegen dependencies locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+          build-root-directory: smithy-dafny-codegen-modules/smithy-rs
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_java_tests.yml

@@ -48,6 +48,8 @@ jobs:
           role-session-name: JavaTests
 
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
@@ -66,6 +68,12 @@ jobs:
           arguments: publishToMavenLocal
           build-root-directory: smithy-dafny-conversion
 
+      - name: Install smithy-dafny-codegen dependencies locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+          build-root-directory: smithy-dafny-codegen-modules/smithy-rs
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_net_tests.yml

@@ -52,6 +52,8 @@ jobs:
           role-session-name: NetTests
 
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
@@ -76,6 +78,12 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install smithy-dafny-codegen dependencies locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+          build-root-directory: smithy-dafny-codegen-modules/smithy-rs
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_rust_tests.yml

@@ -48,6 +48,8 @@ jobs:
           role-session-name: JavaTests
 
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Setup Dafny (build from source)
         uses: ./.github/actions/build_dafny_from_source
@@ -67,6 +69,12 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install smithy-dafny-codegen dependencies locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+          build-root-directory: smithy-dafny-codegen-modules/smithy-rs
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "smithy-dafny-codegen-modules/smithy-rs"]
+	path = smithy-dafny-codegen-modules/smithy-rs
+	url = [email protected]:smithy-lang/smithy-rs.git

SmithyDafnyMakefile.mk

@@ -439,7 +439,10 @@ polymorph_rust:
 	done
 
 _polymorph_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
-_polymorph_rust: _polymorph
+# For several TestModels we've just manually written the code generation target,
+# So we just want to ensure we can transpile and pass the tests in CI.
+# For those, make polymorph_rust should just be a no-op.
+_polymorph_rust: $(if $(RUST_BENERATED), , _polymorph)
 
 ########################## .NET targets
 
@@ -538,49 +541,58 @@ 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
+# The Dafny Rust code generator only supports a single crate for everything,
+# so (among other consequences) we compile src and test code together.
+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
+# The Dafny Rust code generator only supports a single crate for everything,
+# so we inline all dependencies by not passing `-library` to Dafny.
+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: DAFNY_OTHER_FILES=$(RUST_OTHER_FILES)
+transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust patch_after_transpile_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:
-	rm -rf runtimes/rust/dafny_impl/src
-	mkdir -p runtimes/rust/dafny_impl/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
+	mkdir -p runtimes/rust/src
+	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
+
+patch_after_transpile_rust:
+	set -e; for service in $(PROJECT_SERVICES) ; do \
+		export service_deps_var=SERVICE_DEPS_$${service} ; \
+		export namespace_var=SERVICE_NAMESPACE_$${service} ; \
+		export SERVICE=$${service} ; \
+		$(MAKE) _patch_after_transpile_rust ; \
+	done
+
+_patch_after_transpile_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
+_patch_after_transpile_rust:
+	cd $(CODEGEN_CLI_ROOT); \
+	./../gradlew run --args="\
+	patch-after-transpile \
+	--dafny-version $(DAFNY_VERSION) \
+	--library-root $(LIBRARY_ROOT) \
+	$(OUTPUT_RUST) \
+	--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \
+	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
+	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	--namespace $($(namespace_var)) \
+	$(AWS_SDK_CMD) \
+	$(POLYMORPH_OPTIONS) \
+	";
 
 build_rust:
 	cd runtimes/rust; \

TestModels/.gitignore

@@ -14,9 +14,7 @@
 **/runtimes/python/test/internaldafny/generated/*.py
 
 # Dafny Generated Rust
-# (Rust code generation is incomplete so we're patching and checking in for now)
-#**/runtimes/rust
-**/implementation_from_dafny.rs
+**/runtimes/rust/src/implementation_from_dafny.rs
 # Cargo.lock files should only be committed for binaries, not libraries
 **/Cargo.lock
 

TestModels/Aggregate/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+RUST_BENERATED=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \