From 5a0c1dfe83254a62e6a42412d2589de0579f93d5 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 15:19:31 -0700 Subject: [PATCH 01/12] chore: fix dafny interop build steps --- .github/workflows/dafny_interop_test_vector_java.yml | 8 ++++++++ .github/workflows/dafny_interop_test_vector_net.yml | 8 ++++++++ 2 files changed, 16 insertions(+) diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml index d011430cd..f770eb8cd 100644 --- a/.github/workflows/dafny_interop_test_vector_java.yml +++ b/.github/workflows/dafny_interop_test_vector_java.yml @@ -83,6 +83,14 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.2 with: dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Build DynamoDbEncrytpion implementation + shell: bash + working-directory: ./${{ matrix.library }} + run: | + make transpile_implementation_java + make transpile_test_java + make mvn_local_deploy - name: Build TestVectors implementation shell: bash diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index a6de57f63..64ab27dc7 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -84,6 +84,14 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.2 with: dafny-version: ${{ inputs.dbesdk-dafny}} + + - name: Build DynamoDbEncryption implementation + shell: bash + working-directory: ./DyanmoDbEncryption + 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 From e02c10c64225d102df384247f40f5c207470ca26 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 15:36:15 -0700 Subject: [PATCH 02/12] fix --- .github/workflows/dafny_interop_test_vector_java.yml | 2 +- .github/workflows/dafny_interop_test_vector_net.yml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml index f770eb8cd..26891c097 100644 --- a/.github/workflows/dafny_interop_test_vector_java.yml +++ b/.github/workflows/dafny_interop_test_vector_java.yml @@ -83,7 +83,7 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.2 with: dafny-version: ${{ inputs.dbesdk-dafny}} - + - name: Build DynamoDbEncrytpion implementation shell: bash working-directory: ./${{ matrix.library }} diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 64ab27dc7..2d9ea7d86 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -84,10 +84,10 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.2 with: dafny-version: ${{ inputs.dbesdk-dafny}} - + - name: Build DynamoDbEncryption implementation shell: bash - working-directory: ./DyanmoDbEncryption + working-directory: DyanmoDbEncryption run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net From 907749bc88ca6188d12f6ea9195c1a937ea54a0b Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 15:40:56 -0700 Subject: [PATCH 03/12] a --- .github/workflows/dafny_interop_test_vector_net.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 2d9ea7d86..74140ff81 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -87,7 +87,7 @@ jobs: - name: Build DynamoDbEncryption implementation shell: bash - working-directory: DyanmoDbEncryption + working-directory: ../DyanmoDbEncryption run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net From 539225b3b5b0ab94afd836968cd78195de2b4d81 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 15:49:01 -0700 Subject: [PATCH 04/12] another --- .github/workflows/dafny_interop_test_vector_net.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 74140ff81..79fc51889 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -87,7 +87,7 @@ jobs: - name: Build DynamoDbEncryption implementation shell: bash - working-directory: ../DyanmoDbEncryption + working-directory: DynamoDbEncryption run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net From 7013e78c53bdf314e3911028621aac4e6e4c3fb6 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:06:06 -0700 Subject: [PATCH 05/12] another fix --- .github/workflows/dafny_interop_test_vector_java.yml | 6 +++--- .github/workflows/dafny_interop_test_vector_net.yml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml index 26891c097..104141488 100644 --- a/.github/workflows/dafny_interop_test_vector_java.yml +++ b/.github/workflows/dafny_interop_test_vector_java.yml @@ -22,7 +22,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,9 +84,9 @@ jobs: with: dafny-version: ${{ inputs.dbesdk-dafny}} - - name: Build DynamoDbEncrytpion implementation + - name: Build DynamoDbEncryption implementation shell: bash - working-directory: ./${{ matrix.library }} + working-directory: DynamoDbEncryption run: | make transpile_implementation_java make transpile_test_java diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 79fc51889..6d8127afa 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.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 From 712c58647ae00556aa159b58230beae5d509980c Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:16:24 -0700 Subject: [PATCH 06/12] one more? --- project.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project.properties b/project.properties index 47f297e65..5f79e8f97 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ projectJavaVersion=3.6.1-SNAPSHOT -mplDependencyJavaVersion=1.5.1 +mplDependencyJavaVersion=1.5.1-SNAPSHOT dafnyVersion=4.2.0 dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0 From cfafcefe6c40976466b262f39ce0315d41dfe89b Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:28:20 -0700 Subject: [PATCH 07/12] better --- .github/workflows/dafny-interop.yml | 8 ++++++++ .github/workflows/dafny_interop_examples_java.yml | 8 ++++++++ .github/workflows/dafny_interop_java.yml | 8 ++++++++ .github/workflows/dafny_interop_test_vector_java.yml | 8 ++++++++ project.properties | 2 +- 5 files changed, 33 insertions(+), 1 deletion(-) diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml index 93f81b012..e9e0e99d6 100644 --- a/.github/workflows/dafny-interop.yml +++ b/.github/workflows/dafny-interop.yml @@ -21,23 +21,31 @@ on: type: string jobs: + getMplHeadVersion: + uses: ./.github/workflows/mpl_head_version.yml 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 diff --git a/.github/workflows/dafny_interop_examples_java.yml b/.github/workflows/dafny_interop_examples_java.yml index 92aea2202..c691218be 100644 --- a/.github/workflows/dafny_interop_examples_java.yml +++ b/.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 diff --git a/.github/workflows/dafny_interop_java.yml b/.github/workflows/dafny_interop_java.yml index 457f64d1d..75036f78d 100644 --- a/.github/workflows/dafny_interop_java.yml +++ b/.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 }} diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml index 104141488..3a4bb4636 100644 --- a/.github/workflows/dafny_interop_test_vector_java.yml +++ b/.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 @@ -84,6 +88,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 DynamoDbEncryption implementation shell: bash working-directory: DynamoDbEncryption diff --git a/project.properties b/project.properties index 5f79e8f97..47f297e65 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ projectJavaVersion=3.6.1-SNAPSHOT -mplDependencyJavaVersion=1.5.1-SNAPSHOT +mplDependencyJavaVersion=1.5.1 dafnyVersion=4.2.0 dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0 From 1ee0b8d1995d620ba65465936d1d128ec3746174 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:41:25 -0700 Subject: [PATCH 08/12] update --- .github/workflows/dafny-interop.yml | 2 ++ .github/workflows/mpl-head.yml | 2 ++ .github/workflows/mpl_head_version.yml | 6 ++++++ 3 files changed, 10 insertions(+) diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml index e9e0e99d6..ef29e5ace 100644 --- a/.github/workflows/dafny-interop.yml +++ b/.github/workflows/dafny-interop.yml @@ -23,6 +23,8 @@ on: jobs: getMplHeadVersion: uses: ./.github/workflows/mpl_head_version.yml + with: + mpl-head: false dafny-interop-java: needs: getMplHeadVersion uses: ./.github/workflows/dafny_interop_java.yml diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 6bb7e1b7c..c2fb13503 100644 --- a/.github/workflows/mpl-head.yml +++ b/.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' diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index 094825a9a..81c871b35 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -5,6 +5,11 @@ name: MPL HEAD Version on: workflow_call: + inputs: + mpl-head: + description: "Using MPL HEAD?" + required: true + type: boolean outputs: version: description: "The dafny version for verify" @@ -20,6 +25,7 @@ jobs: with: submodules: recursive - name: Update MPL submodule locally if requested + if: ${{inputs.mpl-head}} == 'true' working-directory: submodules/MaterialProviders shell: bash run: | From 27091c52ab2490898a7798ed5f23baf92416cdd5 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:44:51 -0700 Subject: [PATCH 09/12] a --- .github/workflows/mpl_head_version.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index 81c871b35..07d6507cf 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -25,7 +25,7 @@ jobs: with: submodules: recursive - name: Update MPL submodule locally if requested - if: ${{inputs.mpl-head}} == 'true' + if: ${{inputs.mpl-head}} == true working-directory: submodules/MaterialProviders shell: bash run: | From 5dec195e302d00a8f22f7df5dafc772d72956a83 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:48:01 -0700 Subject: [PATCH 10/12] a --- .github/workflows/mpl_head_version.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index 07d6507cf..d5b3b33ef 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -25,7 +25,7 @@ jobs: with: submodules: recursive - name: Update MPL submodule locally if requested - if: ${{inputs.mpl-head}} == true + if: ${{inputs.mpl-head == true }} working-directory: submodules/MaterialProviders shell: bash run: | From 4089f55ec488f1c860fbaa205203c1f5a94c64a9 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:54:53 -0700 Subject: [PATCH 11/12] a --- .github/workflows/dafny-interop.yml | 2 +- .github/workflows/mpl_head_version.yml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny-interop.yml b/.github/workflows/dafny-interop.yml index ef29e5ace..da395dbfa 100644 --- a/.github/workflows/dafny-interop.yml +++ b/.github/workflows/dafny-interop.yml @@ -24,7 +24,7 @@ jobs: getMplHeadVersion: uses: ./.github/workflows/mpl_head_version.yml with: - mpl-head: false + mpl-head: ${{inputs.mpl-commit}} dafny-interop-java: needs: getMplHeadVersion uses: ./.github/workflows/dafny_interop_java.yml diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index d5b3b33ef..11decfa3f 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -9,7 +9,8 @@ on: mpl-head: description: "Using MPL HEAD?" required: true - type: boolean + default: main + type: string outputs: version: description: "The dafny version for verify" @@ -25,11 +26,10 @@ jobs: with: submodules: recursive - name: Update MPL submodule locally if requested - if: ${{inputs.mpl-head == true }} 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 From 056c9e8ea4526b9aee572f6324f2c52e811805aa Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 20 Aug 2024 16:57:35 -0700 Subject: [PATCH 12/12] a --- .github/workflows/mpl_head_version.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index 11decfa3f..f94200cda 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -25,6 +25,7 @@ jobs: - uses: actions/checkout@v4 with: submodules: recursive + fetch-depth: 0 - name: Update MPL submodule locally if requested working-directory: submodules/MaterialProviders shell: bash