From a7f3c5b3caf74b683306ac18f2cda5d46ef8ca99 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 15 May 2024 11:26:09 -0700
Subject: [PATCH] Fix CI, csproj

---
 .github/workflows/ci_examples_java.yml        |  9 +++++++
 .github/workflows/ci_test_java.yml            |  2 +-
 .github/workflows/ci_test_net.yml             |  2 +-
 .github/workflows/ci_verification.yml         |  2 +-
 .../runtimes/net/DynamoDbEncryption.csproj    | 26 ++++++++++++++++++-
 5 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml
index 8ff093e74..5e5cbc333 100644
--- a/.github/workflows/ci_examples_java.yml
+++ b/.github/workflows/ci_examples_java.yml
@@ -62,6 +62,15 @@ jobs:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: DynamoDbEncryption
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+    
       - name: Build and locally deploy dependencies for examples
         shell: bash
         working-directory: ./DynamoDbEncryption
diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml
index d6186c2fb..a55e0b015 100644
--- a/.github/workflows/ci_test_java.yml
+++ b/.github/workflows/ci_test_java.yml
@@ -59,7 +59,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}
diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml
index c48cb853e..76f15b09c 100644
--- a/.github/workflows/ci_test_net.yml
+++ b/.github/workflows/ci_test_net.yml
@@ -66,7 +66,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}
diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml
index ef7366e27..abfa56397 100644
--- a/.github/workflows/ci_verification.yml
+++ b/.github/workflows/ci_verification.yml
@@ -54,7 +54,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
       
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}
diff --git a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
index 0ac4c9330..c634d5a62 100644
--- a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
+++ b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
@@ -31,11 +31,35 @@
     <NoWarn>CS0105,CS0618</NoWarn>
   </PropertyGroup>
 
+  <PropertyGroup>
+    <!-- This is somewhat brittle,
+         but having the value in a properties file
+         that can be shared is worth it.
+         See: https://learn.microsoft.com/en-us/visualstudio/msbuild/property-functions?view=vs-2022
+         for more details on property functions
+         
+         This takes a properties file (a=b)
+         1. Loads the file
+         2. Splits on `dafnyVersion=` and takes everything to the right of that
+           e.g. the version + any trailing data
+         3. Splits on newline and takes the second element.
+           This SHOULD be the value of `dafnyVersion` and not contain any trailing data
+     -->
+    <projectProperties>
+      $([System.IO.File]::ReadAllText('$(MSBuildProjectDirectory)/../../../project.properties'))
+    </projectProperties>
+    <dropBeforeDafnyVersionProperty>
+      $([System.Text.RegularExpressions.Regex]::Split("$(projectProperties)", "dafnyVersion=")[1])
+    </dropBeforeDafnyVersionProperty>
+    <DafnyVersion>
+      $([System.Text.RegularExpressions.Regex]::Split("$(dropBeforeDafnyVersionProperty)", "\n")[1])
+    </DafnyVersion>
+  </PropertyGroup>
 
   <ItemGroup>
     <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.300.2"/>
     <PackageReference Include="AWSSDK.Core" Version="3.7.300.2"/>
-    <PackageReference Include="DafnyRuntime" Version="4.2.0" />
+    <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--
               System.Collections.Immutable can be removed once dafny.msbuild is updated with