chore(ci): Add tiny Rust test case to CI (#328)

Adding the very first bit of CI to regression test what Rust support is working: just verifying we can build UInt.dfy from StandardLibrary. See StandardLibrary's Makefile for comments about the current scope and TODOs to expand it. Dry-run of nightly build: https://github.com/smithy-lang/smithy-dafny/actions/runs/8303185805/job/22726859333. Note Java is failing because Dafny is in the middle of releasing 4.5 but hasn't released the 4.5 Java runtime yet.
smithy-lang · Mar 19, 2024 · a43a6da · a43a6da
1 parent 2029f8b
commit a43a6da
Show file tree

Hide file tree

Showing 8 changed files with 188 additions and 2 deletions.
diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml
@@ -24,3 +24,7 @@ jobs:
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: ${{ inputs.dafny }}
+  manual-ci-rust:
+    uses: ./.github/workflows/test_models_rust_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
diff --git a/.github/workflows/nightly_dafny.yml b/.github/workflows/nightly_dafny.yml
@@ -27,3 +27,8 @@ jobs:
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: 'nightly-latest'
+  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'
diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
@@ -41,3 +41,15 @@ jobs:
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  pr-ci-rust:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+        # The Rust backend didn't exist yet in Dafny 4.2
+        exclude:
+          - dafny-version: 4.2.0
+    uses: ./.github/workflows/test_models_rust_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -43,3 +43,15 @@ jobs:
     uses: ./.github/workflows/test_models_net_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  push-ci-rust:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+        # The Rust backend didn't exist yet in Dafny 4.2
+        exclude:
+          - dafny-version: 4.2.0
+    uses: ./.github/workflows/test_models_rust_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
diff --git a/.github/workflows/test_models_java_tests.yml b/.github/workflows/test_models_java_tests.yml
@@ -11,8 +11,6 @@ on:
 
 jobs:
   testJava:
-    # Don't run the nightly build on forks
-    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     strategy:
       fail-fast: false
       matrix:

diff --git a/.github/workflows/test_models_rust_tests.yml b/.github/workflows/test_models_rust_tests.yml
@@ -0,0 +1,104 @@
+# This workflow performs tests in Rust.
+name: Library Rust tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: 'The Dafny version to run'
+        required: true
+        type: string
+
+jobs:
+  testRust:
+    strategy:
+      fail-fast: false
+      matrix:
+        library: [
+          TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
+          # TestModels/Aggregate,
+          # TestModels/AggregateReferences,
+          # TestModels/CodegenPatches,
+          # TestModels/Constraints,
+          # TestModels/Constructor,
+          # TestModels/Dependencies,
+          # TestModels/Errors,
+          # TestModels/Extendable,
+          # TestModels/Extern,
+          # TestModels/LanguageSpecificLogic,
+          # TestModels/LocalService,
+          # TestModels/MultipleModels,
+          # TestModels/Refinement,
+          # TestModels/Resource,
+          # TestModels/SimpleTypes/BigDecimal,
+          # TestModels/SimpleTypes/BigInteger,
+          # TestModels/SimpleTypes/SimpleBlob,
+          # TestModels/SimpleTypes/SimpleBoolean,
+          # TestModels/SimpleTypes/SimpleByte,
+          # TestModels/SimpleTypes/SimpleDouble,
+          # TestModels/SimpleTypes/SimpleEnum,
+          # TestModels/SimpleTypes/SimpleEnumV2,
+          # TestModels/SimpleTypes/SimpleFloat,
+          # TestModels/SimpleTypes/SimpleInteger,
+          # TestModels/SimpleTypes/SimpleLong,
+          # TestModels/SimpleTypes/SimpleShort,
+          # TestModels/SimpleTypes/SimpleString,
+          # TestModels/SimpleTypes/SimpleTimestamp,
+          # TestModels/Union,
+          # TestModels/aws-sdks/ddb,
+          # TestModels/aws-sdks/kms,
+        ]
+    runs-on: "ubuntu-latest"
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v1
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-PolymorphTestModels-Role-us-west-2
+          role-session-name: JavaTests
+
+      - uses: actions/checkout@v3
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Set up Rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+        with:
+          toolchain: '1.74.1'
+
+      # TODO - not implemented yet, and not relevant for the only library we're testing so far (StandardLibrary)
+      # - name: Generate Polymorph Dafny and Rust code
+      #   shell: bash
+      #   working-directory: ./${{ matrix.library }}
+      #   # Use $DAFNY_VERSION from setup-dafny-action to handle nightlies correctly
+      #   run: |
+      #     make polymorph_dafny DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
+      #     make polymorph_rust DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
+
+      - name: Compile ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_rust CORES=$CORES
+
+      # TODO - not implemented yet, and no test files work yet in the only library we're testing so far (StandardLibrary)
+      # - name: Test ${{ matrix.library }}
+      #   working-directory: ./${{ matrix.library }}
+      #   shell: bash
+      #   run: |
+      #     make test_rust
diff --git a/TestModels/.gitignore b/TestModels/.gitignore
@@ -9,6 +9,10 @@
 **/runtimes/java/src/main/dafny-generated/
 **/runtimes/java/src/test/dafny-generated/
 
+# Dafny Generated Rust
+**/runtimes/rust
+**/runtimes/rust
+
 # Polymorph Generated Dafny
 **/Model/*Types.dfy
 **/Model/*TypesWrapped.dfy

diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile
@@ -44,6 +44,53 @@ transpile_net: | transpile_implementation_net transpile_test_net
 # StandardLibrary as a dependency
 transpile_java: | transpile_implementation_java transpile_test_java
 
+########################## Rust targets
+
+# Starting to add makefile targets for Rust, but only in this library for now
+# since Rust support in Dafny is not yet complete.
+# But we want to lock down what IS working to ensure we don't have regressions
+# and gradually expand the scope of what we're testing.
+
+# TODO:
+#  1. Only building UInt.dfy to start because other files use unsupported features
+#     (e.g. the variance specifiers in Option<+T>).
+#     This scope should be expanded over time.
+#  2. Using -compile:1 instead of -compile:0 because the Rust backend incorrectly
+#     only outputs the runtime source when compiling the target program.
+#     See https://github.com/dafny-lang/dafny/issues/5203.
+#  3. Unlike other backends, the Rust backend emits full Rust projects,
+#     including Cargo.toml.
+#     This runs contrary to the smithy-dafny philosophy
+#     of translating code into predefined projects
+#     and combining it with smithy-generated and hand-written code.
+#     We'll need some Dafny-side design discussion to support both use cases.
+
+transpile_rust: | _transpile_implementation_just_uint_rust _mv_implementation_rust
+
+_transpile_implementation_just_uint_rust:
+	find ./src -name 'UInt.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
+		-stdin \
+		-noVerify \
+		-vcsCores:$(CORES) \
+		-compileTarget:rs \
+		-spillTargetCode:3 \
+		-compile:1 \
+		-optimizeErasableDatatypeWrapper:0 \
+		-compileSuffix:1 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
+		-out ImplementationFromDafny \
+
+_mv_implementation_rust:
+	rm -rf runtimes/rust
+	mv ImplementationFromDafny-rust runtimes/rust
+
+build_rust: transpile_rust
+	cd runtimes/rust; \
+	cargo build
+
+##########################
+
 transpile_dependencies:
 	echo "Skipping transpile_dependencies for StandardLibrary"