Merge pull request #10 from ShubhamChaturvedi7/scchatur/dev

chore(CI): enable aws-kms models

.github/actions/build_dafny_from_source/action.yml

@@ -53,3 +53,11 @@ runs:
       shell: bash
       run: |
         echo "DAFNY_VERSION=4.7.0" >> $GITHUB_ENV
+
+    # update the copy of the Rust runtime we have inside TestModels
+    # (since it's not published yet)
+    - name: Update dafny_runtime_rust
+      shell: bash
+      run: |
+        rm -rf TestModels/dafny-dependencies/dafny_runtime_rust
+        cp -r dafny/Source/DafnyRuntime/DafnyRuntimeRust TestModels/dafny-dependencies/dafny_runtime_rust

.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -0,0 +1,21 @@
+#
+# This local action sets up code dependencies
+# to run Smithy-Dafny CI in GitHub Actions workflows.
+#
+
+name: "Install Smithy-Dafny codegen dependencies"
+description: "Install Java package dependencies required to run Smithy-Dafny codegen"
+runs:
+  using: "composite"
+  steps:
+    - name: Install smithy-dafny-codegen Rust 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 Python dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :smithy-python-codegen:pTML
+        build-root-directory: codegen/smithy-dafny-codegen-modules/smithy-python/codegen

.github/not-grep.toml

@@ -1,13 +1,13 @@
 [prefix]
-"**/*.smithy" = """
+"**/[!smithy-dafny-codegen-modules]/**/*.smithy" = """
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 """
-"**/*.java" = """
+"**/[!smithy-dafny-codegen-modules]/**/*.java" = """
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 """
-"**/[!/obj/]*.cs" = """
+"**/[!smithy-dafny-codegen-modules]/**/[!/obj/]*.cs" = """
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 """
@@ -16,15 +16,15 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 """
-"**/*.kts" = """
+"**/[!smithy-dafny-codegen-modules]/**/*.kts" = """
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
 """
-"**/*.mk" = """
+"**/[!smithy-dafny-codegen-modules]/**/*.mk" = """
 # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0
 """
-"**/Makefile" = """
+"**/[!smithy-dafny-codegen-modules]/**/Makefile" = """
 # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0
-"""
+"""

.github/workflows/manual.yml

@@ -28,3 +28,7 @@ jobs:
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ inputs.dafny }}
+  manual-ci-python:
+    uses: ./.github/workflows/test_models_python_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}

.github/workflows/nightly_dafny.yml

@@ -27,21 +27,29 @@ 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"
+  dafny-nightly-python:
+    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
+    uses: ./.github/workflows/test_models_python_tests.yml
+    with:
+      dafny: "nightly-latest"
 
   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

@@ -11,8 +11,12 @@ jobs:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
         run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
+      - name: Populate Dafny versions list for "only new versions" languages (Python)
+        id: populate-only-new-dafny-versions-list
+        run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
     outputs:
       dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+      only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
 
   pr-ci-verification:
     needs: pr-populate-dafny-versions
@@ -49,7 +53,16 @@ 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
+          - ab5af65d33b7d44905807f6598b0fbccd5fc39c9
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  pr-ci-python:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
+    uses: ./.github/workflows/test_models_python_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}

.github/workflows/push.yml

@@ -13,8 +13,12 @@ jobs:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
         run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
+      - name: Populate Dafny versions list for "only new versions" languages (Python)
+        id: populate-only-new-dafny-versions-list
+        run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
     outputs:
       dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+      only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
 
   push-ci-verification:
     needs: pr-populate-dafny-versions
@@ -51,7 +55,16 @@ 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
+          - ab5af65d33b7d44905807f6598b0fbccd5fc39c9
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  push-ci-python:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
+    uses: ./.github/workflows/test_models_python_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,9 @@ jobs:
           # Matching the hard-coded version for the "2023" edition for now
           dafny-version: 4.1.0
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - 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/setup-dafny-action@v1.7.0
@@ -56,6 +58,9 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_go_tests.yml

@@ -39,7 +39,7 @@ jobs:
           # TestModels/SimpleTypes/SimpleTimestamp,
           TestModels/Union,
           # TestModels/aws-sdks/ddb,
-          # TestModels/aws-sdks/kms
+          TestModels/aws-sdks/kms
         ]
     runs-on: "macos-12"
     steps:

.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/setup-dafny-action@v1.7.0
@@ -66,6 +68,9 @@ jobs:
           arguments: publishToMavenLocal
           build-root-directory: smithy-dafny-conversion
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - 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/setup-dafny-action@v1.7.0
@@ -76,6 +78,9 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_python_tests.yml

@@ -0,0 +1,98 @@
+# This workflow performs tests in Python.
+name: Library Python tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      num_shards:
+        required: false
+        type: number
+        default: 5
+
+jobs:
+  populate-matrix-dimensions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Populate shard list
+        id: populate-shard-list
+        run: echo "shard-list=[`seq -s , 1 ${{ inputs.num_shards }}`]" >> $GITHUB_OUTPUT
+    outputs:
+      shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
+
+  testPython:
+    needs: populate-matrix-dimensions
+    strategy:
+      fail-fast: false # at least for development; see all errors
+      matrix:
+        shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }}
+    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: PythonTests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/setup-dafny-action@v1.7.0
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Setup Python for running tests
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.11
+          architecture: x64
+      - run: |
+          python -m pip install --upgrade pip
+          pip install --upgrade tox
+          pip install poetry
+
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 17
+
+      - name: Setup smithy-dafny-conversion
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: publishToMavenLocal
+          build-root-directory: smithy-dafny-conversion
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      - name: Install smithy-dafny-codegen locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :smithy-dafny-codegen:pTML
+          build-root-directory: codegen
+
+      - name: Execute smithy-dafny-codegen-test tests
+        uses: gradle/gradle-build-action@v2
+        env:
+          JUNIT_SHARD: ${{ matrix.shard }}
+          JUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
+        with:
+          arguments: :smithy-dafny-codegen-test:test --tests '*smithypython*' --info
+          build-root-directory: codegen

.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,9 @@ jobs:
           distribution: "corretto"
           java-version: "17"
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Install smithy-dafny-codegen locally
         uses: gradle/gradle-build-action@v2
         with: