Merge branch 'main' into tony/fix-prettier

.github/workflows/library_codegen.yml

@@ -53,7 +53,7 @@ jobs:
       # and to translate version strings such as "nightly-latest"
       # to an actual DAFNY_VERSION.
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_dafny_verification.yml

@@ -48,7 +48,7 @@ jobs:
       - run: git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_format.yml

@@ -49,7 +49,7 @@ jobs:
       - run: git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_go_tests.yml

@@ -64,7 +64,7 @@ jobs:
       - run: git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_interop_tests.yml

@@ -81,20 +81,6 @@ jobs:
         uses: actions-rust-lang/[email protected]
         with:
           components: rustfmt
-      # TODO - uncomment this after Rust formatter works
-      # - name: Rustfmt Check
-      #   uses: actions-rust-lang/rustfmt@v1
-
-      # TODO: Remove this after the formatting in Rust starts working
-      - name: smithy-dafny Rust hacks
-        if: matrix.language == 'rust'
-        shell: bash
-        run: |
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          else
-            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          fi
 
       - name: Setup Go
         uses: actions/setup-go@v5
@@ -109,8 +95,15 @@ jobs:
         if: matrix.language == 'rust' && matrix.os == 'windows-latest'
         uses: ilammy/setup-nasm@v1
 
-      - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+      - name: Setup Dafny Rust
+        if: matrix.language == 'rust'
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: nightly-2025-01-30-7db1e5f
+
+      - name: Setup Dafny Not Rust
+        if: matrix.language != 'rust'
+        uses: dafny-lang/[email protected]
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -154,7 +147,7 @@ jobs:
         if: matrix.language == 'rust'
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
-      # TODO: Remove this after checking in Rust polymorph code
+      # We do not check in Rust polymorph code
       - name: Run make polymorph_rust
         if: matrix.language == 'rust'
         shell: bash
@@ -274,20 +267,6 @@ jobs:
         uses: actions-rust-lang/[email protected]
         with:
           components: rustfmt
-      # TODO - uncomment this after Rust formatter works
-      # - name: Rustfmt Check
-      #   uses: actions-rust-lang/rustfmt@v1
-
-      # TODO: Remove this after the formatting in Rust starts working
-      - name: smithy-dafny Rust hacks
-        if: matrix.decrypting_language == 'rust'
-        shell: bash
-        run: |
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          else
-            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          fi
 
       - name: Setup Go
         uses: actions/setup-go@v5
@@ -302,8 +281,15 @@ jobs:
         if: matrix.decrypting_language == 'rust' && matrix.os == 'windows-latest'
         uses: ilammy/setup-nasm@v1
 
-      - name: Setup Dafny
-        uses: dafny-lang/[email protected]
+      - name: Setup Dafny 2 Rust
+        if: matrix.decrypting_language == 'rust'
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: nightly-2025-01-30-7db1e5f
+
+      - name: Setup Dafny 2 Not Rust
+        if: matrix.decrypting_language != 'rust'
+        uses: dafny-lang/[email protected]
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_java_tests.yml

@@ -61,7 +61,7 @@ jobs:
       - run: git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_net_tests.yml

@@ -64,7 +64,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_python_tests.yml

@@ -64,7 +64,7 @@ jobs:
       - run: git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
           dafny-version: ${{ inputs.dafny }}
 

.github/workflows/library_rust_tests.yml

@@ -58,25 +58,11 @@ jobs:
         uses: actions-rust-lang/[email protected]
         with:
           components: rustfmt
-      # TODO - uncomment this after Rust formatter works
-      # - name: Rustfmt Check
-      #   uses: actions-rust-lang/rustfmt@v1
 
-      # TODO: Use setup-dafny-actions with correct version when Dafny releases 4.8.2
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
-          dafny-version: 4.9.0
-
-      # TODO: Remove this after the formatting in Rust starts working
-      - name: smithy-dafny Rust hacks
-        shell: bash
-        run: |
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          else
-            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
-          fi
+          dafny-version: nightly-2025-01-30-7db1e5f
 
       - name: Setup Java 17 for codegen
         uses: actions/setup-java@v3
@@ -110,3 +96,4 @@ jobs:
         working-directory: ./${{ matrix.library }}
         run: |
           make test_rust
+          make test_rust_debug