chore: fix dafny interop build steps (#1293)

.github/workflows/dafny-interop.yml

@@ -21,23 +21,33 @@ on:
         type: string
 
 jobs:
+  getMplHeadVersion:
+    uses: ./.github/workflows/mpl_head_version.yml
+    with:
+      mpl-head: ${{inputs.mpl-commit}}
   dafny-interop-java:
+    needs: getMplHeadVersion
     uses: ./.github/workflows/dafny_interop_java.yml
     with:
       mpl-dafny: ${{inputs.mpl-dafny}}
       mpl-commit: ${{inputs.mpl-commit}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
       dbesdk-dafny: ${{inputs.dbesdk-dafny}}
   dafny-interop-java-test-vectors:
+    needs: getMplHeadVersion
     uses: ./.github/workflows/dafny_interop_test_vector_java.yml
     with:
       mpl-dafny: ${{inputs.mpl-dafny}}
       mpl-commit: ${{inputs.mpl-commit}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
       dbesdk-dafny: ${{inputs.dbesdk-dafny}}
   dafny-interop-java-examples:
+    needs: getMplHeadVersion
     uses: ./.github/workflows/dafny_interop_examples_java.yml
     with:
       mpl-dafny: ${{inputs.mpl-dafny}}
       mpl-commit: ${{inputs.mpl-commit}}
+      mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
       dbesdk-dafny: ${{inputs.dbesdk-dafny}}
   dafny-interop-net:
     uses: ./.github/workflows/dafny_interop_test_net.yml

.github/workflows/dafny_interop_examples_java.yml

@@ -13,6 +13,10 @@ on:
         required: false
         default: "main"
         type: string
+      mpl-version:
+        description: "The MPL version to use"
+        required: true
+        type: string
       dbesdk-dafny:
         description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
         required: true
@@ -74,6 +78,10 @@ jobs:
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
+      - name: Update project.properties if using MPL HEAD
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       - name: Build implementation
         shell: bash
         working-directory: ./DynamoDbEncryption

.github/workflows/dafny_interop_java.yml

@@ -13,6 +13,10 @@ on:
         required: false
         default: "main"
         type: string
+      mpl-version:
+        description: "The MPL version to use"
+        required: true
+        type: string
       dbesdk-dafny:
         description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
         required: true
@@ -74,6 +78,10 @@ jobs:
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
+      - name: Update project.properties if using MPL HEAD
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
       - name: Build ${{ matrix.library }} implementation
         shell: bash
         working-directory: ./${{ matrix.library }}

.github/workflows/dafny_interop_test_vector_java.yml

@@ -13,6 +13,10 @@ on:
         required: false
         default: "main"
         type: string
+      mpl-version:
+        description: "The MPL version to use"
+        required: true
+        type: string
       dbesdk-dafny:
         description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
         required: true
@@ -22,7 +26,7 @@ jobs:
   testJava:
     strategy:
       matrix:
-        library: [DynamoDbEncryption, TestVectors]
+        library: [TestVectors]
         java-version: [8, 11, 16, 17]
         os: [
             # Run on ubuntu image that comes pre-configured with docker
@@ -84,6 +88,18 @@ jobs:
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
+      - name: Update project.properties if using MPL HEAD
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
+      - name: Build DynamoDbEncryption implementation
+        shell: bash
+        working-directory: DynamoDbEncryption
+        run: |
+          make transpile_implementation_java
+          make transpile_test_java
+          make mvn_local_deploy
+
       - name: Build TestVectors implementation
         shell: bash
         working-directory: ${{matrix.library}}

.github/workflows/dafny_interop_test_vector_net.yml

@@ -24,7 +24,7 @@ jobs:
       matrix:
         library: [TestVectors]
         dotnet-version: ["6.0.x"]
-        os: [macos-12, ubuntu-latest, windows-latest]
+        os: [ubuntu-latest]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
@@ -85,6 +85,14 @@ jobs:
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
+      - name: Build DynamoDbEncryption implementation
+        shell: bash
+        working-directory: DynamoDbEncryption
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          make transpile_implementation_net 
+          make transpile_test_net
+
       - name: Build TestVectors implementation
         shell: bash
         working-directory: ${{matrix.library}}

.github/workflows/mpl-head.yml

@@ -16,6 +16,8 @@ jobs:
   getMplHeadVersion:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/mpl_head_version.yml
+    with:
+      mpl-head: true
   mpl-head-ci-format:
     needs: getVersion
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'

.github/workflows/mpl_head_version.yml

@@ -5,6 +5,12 @@ name: MPL HEAD Version
 
 on:
   workflow_call:
+    inputs:
+      mpl-head:
+        description: "Using MPL HEAD?"
+        required: true
+        default: main
+        type: string
     outputs:
       version:
         description: "The dafny version for verify"
@@ -19,11 +25,12 @@ jobs:
       - uses: actions/checkout@v4
         with:
           submodules: recursive
+          fetch-depth: 0
       - name: Update MPL submodule locally if requested
         working-directory: submodules/MaterialProviders
         shell: bash
         run: |
-          git checkout main
+          git checkout ${{inputs.mpl-head}}
           git pull
           git submodule update --init --recursive
           git rev-parse HEAD