From 2cb1bb5575a25fbe278c822dca72963631d28552 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 16:19:50 -0700 Subject: [PATCH 01/20] chore(GHA): add action for testing against MPL HEAD --- .github/actions/mpl-head/mpl_head_codegen.yml | 70 ++++++++++++++++++ .github/workflows/daily_ci.yml | 34 ++++++--- .github/workflows/mpl-head.yml | 71 +++++++++++++++++++ 3 files changed, 167 insertions(+), 8 deletions(-) create mode 100644 .github/actions/mpl-head/mpl_head_codegen.yml create mode 100644 .github/workflows/mpl-head.yml diff --git a/.github/actions/mpl-head/mpl_head_codegen.yml b/.github/actions/mpl-head/mpl_head_codegen.yml new file mode 100644 index 000000000..feaf81edc --- /dev/null +++ b/.github/actions/mpl-head/mpl_head_codegen.yml @@ -0,0 +1,70 @@ +# This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in +# with the latest mpl head +name: Library-MPL-HEAD Code Generation +on: + workflow_call: + inputs: + dafny: + description: "The dafny version to run" + required: true + type: string + +jobs: + code-generation: + strategy: + fail-fast: false + matrix: + library: [DynamoDbEncryption, TestVectors] + # Note dotnet is only used for formatting generated code + # in this workflow + dotnet-version: ["6.0.x"] + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths + run: | + git config --global core.longpaths true + + - uses: actions/checkout@v3 + with: + submodules: recursive + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + shell: bash + run: | + git checkout main + git pull + git submodule update --init --recursive + + - name: Read MPL Version from its properties file + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "submodules/MaterialProviders/project.properties" + properties: "mplVersion" + + # Only used to format generated code + # and to translate version strings such as "nightly-latest" + # to an actual DAFNY_VERSION. + - name: Setup Dafny + uses: dafny-lang/setup-dafny-action@v1.7.0 + with: + dafny-version: ${{ inputs.dafny }} + + - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} + uses: actions/setup-dotnet@v4 + with: + dotnet-version: ${{ matrix.dotnet-version }} + + - uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: true diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index d7248e0d2..93fc73df2 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -9,10 +9,10 @@ jobs: getVersion: # Don't run the cron builds on forks if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/dafny_version.yaml + uses: ./.github/workflows/dafny_version.yml getVerifyVersion: if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/dafny_verify_version.yaml + uses: ./.github/workflows/dafny_verify_version.yml daily-ci-format: needs: getVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' @@ -22,7 +22,7 @@ jobs: daily-ci-codegen: needs: getVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/library_codegen.yml + uses: ./.github/workflows/ci_codegen.yml with: dafny: ${{needs.getVersion.outputs.version}} daily-ci-verification: @@ -31,15 +31,33 @@ jobs: uses: ./.github/workflows/library_dafny_verification.yml with: dafny: ${{needs.getVerifyVersion.outputs.version}} - daily-ci-java: + daily-ci-test-vector-verification: + needs: getVerifyVersion + uses: ./.github/workflows/test_vector_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + daily-ci-java-test-vectors: needs: getVersion - if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/library_java_tests.yml + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + daily-ci-java-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_java.yml with: dafny: ${{needs.getVersion.outputs.version}} daily-ci-net: needs: getVersion - if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/library_net_tests.yml + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + daily-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml with: dafny: ${{needs.getVersion.outputs.version}} + daily-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} \ No newline at end of file diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml new file mode 100644 index 000000000..97d31ae2c --- /dev/null +++ b/.github/workflows/mpl-head.yml @@ -0,0 +1,71 @@ +# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT) +name: MPL HEAD Integration + +on: + pull_request: + # schedule: + # # Although this is triggered daily the MPL may not get daily commits, which + # # means that some builds MAY get the same MPL HEAD. + # - cron: "00 14 * * 1-5" +jobs: + getVersion: + # Don't run the cron builds on forks + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/dafny_version.yml + getVerifyVersion: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/dafny_verify_version.yml + mpl-head-ci-format: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head-ci-codegen: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/actions/mpl-head/mpl_head_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + # mpl-head-ci-verification: + # needs: getVerifyVersion + # if: github.event_name != 'schedule' || github.repository_owner == 'aws' + # uses: ./.github/workflows/library_dafny_verification.yml + # with: + # dafny: ${{needs.getVerifyVersion.outputs.version}} + # mpl-head-ci-test-vector-verification: + # needs: getVerifyVersion + # uses: ./.github/workflows/test_vector_verification.yml + # with: + # dafny: ${{needs.getVerifyVersion.outputs.version}} + # mpl-head: true + # mpl-head-ci-java-test-vectors: + # needs: getVersion + # uses: ./.github/workflows/ci_test_vector_java.yml + # with: + # dafny: ${{needs.getVersion.outputs.version}} + # mpl-head: true + # mpl-headci-java-examples: + # needs: getVersion + # uses: ./.github/workflows/ci_examples_java.yml + # with: + # dafny: ${{needs.getVersion.outputs.version}} + # mpl-head: true + # mpl-head-ci-net: + # needs: getVersion + # uses: ./.github/workflows/ci_test_net.yml + # with: + # dafny: ${{needs.getVersion.outputs.version}} + # mpl-head: true + # mpl-head-ci-net-test-vectors: + # needs: getVersion + # uses: ./.github/workflows/ci_test_vector_net.yml + # with: + # dafny: ${{needs.getVersion.outputs.version}} + # mpl-head: true + # mpl-head-ci-net-examples: + # needs: getVersion + # uses: ./.github/workflows/ci_examples_net.yml + # with: + # dafny: ${{needs.getVersion.outputs.version}} + # mpl-head: true \ No newline at end of file From 30cf4552fe1e2fafe30b0dc04feb906b9d39d9f3 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 16:27:12 -0700 Subject: [PATCH 02/20] format --- .github/actions/mpl-head/mpl_head_codegen.yml | 30 +++++++++---------- .github/workflows/daily_ci.yml | 2 +- .github/workflows/mpl-head.yml | 21 ++++++------- 3 files changed, 25 insertions(+), 28 deletions(-) diff --git a/.github/actions/mpl-head/mpl_head_codegen.yml b/.github/actions/mpl-head/mpl_head_codegen.yml index feaf81edc..79022dade 100644 --- a/.github/actions/mpl-head/mpl_head_codegen.yml +++ b/.github/actions/mpl-head/mpl_head_codegen.yml @@ -34,21 +34,21 @@ jobs: - uses: actions/checkout@v3 with: submodules: recursive - - - name: Update MPL submodule - working-directory: submodules/MaterialProviders - shell: bash - run: | - git checkout main - git pull - git submodule update --init --recursive - - - name: Read MPL Version from its properties file - id: read_property - uses: christian-draeger/read-properties@1.1.1 - with: - path: "submodules/MaterialProviders/project.properties" - properties: "mplVersion" + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + shell: bash + run: | + git checkout main + git pull + git submodule update --init --recursive + + - name: Read MPL Version from its properties file + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "submodules/MaterialProviders/project.properties" + properties: "mplVersion" # Only used to format generated code # and to translate version strings such as "nightly-latest" diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index 93fc73df2..2edd6273a 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -60,4 +60,4 @@ jobs: needs: getVersion uses: ./.github/workflows/ci_examples_net.yml with: - dafny: ${{needs.getVersion.outputs.version}} \ No newline at end of file + dafny: ${{needs.getVersion.outputs.version}} diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 97d31ae2c..ecb2544fa 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -1,12 +1,9 @@ -# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT) -name: MPL HEAD Integration +# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT) +name: CI MPL HEAD on: pull_request: - # schedule: - # # Although this is triggered daily the MPL may not get daily commits, which - # # means that some builds MAY get the same MPL HEAD. - # - cron: "00 14 * * 1-5" + jobs: getVersion: # Don't run the cron builds on forks @@ -38,34 +35,34 @@ jobs: # uses: ./.github/workflows/test_vector_verification.yml # with: # dafny: ${{needs.getVerifyVersion.outputs.version}} - # mpl-head: true + # mpl-head: true # mpl-head-ci-java-test-vectors: # needs: getVersion # uses: ./.github/workflows/ci_test_vector_java.yml # with: # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + # mpl-head: true # mpl-headci-java-examples: # needs: getVersion # uses: ./.github/workflows/ci_examples_java.yml # with: # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + # mpl-head: true # mpl-head-ci-net: # needs: getVersion # uses: ./.github/workflows/ci_test_net.yml # with: # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + # mpl-head: true # mpl-head-ci-net-test-vectors: # needs: getVersion # uses: ./.github/workflows/ci_test_vector_net.yml # with: # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + # mpl-head: true # mpl-head-ci-net-examples: # needs: getVersion # uses: ./.github/workflows/ci_examples_net.yml # with: # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true \ No newline at end of file + # mpl-head: true From efe69df6e321618d50dfd8ff50b833ba76713b3e Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 16:54:18 -0700 Subject: [PATCH 03/20] test --- .github/actions/mpl-head/action.yml | 45 +++++++++++++++++++++++++++++ .github/workflows/ci_codegen.yml | 10 +++++++ .github/workflows/mpl-head.yml | 3 +- 3 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 .github/actions/mpl-head/action.yml diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml new file mode 100644 index 000000000..8a819a37c --- /dev/null +++ b/.github/actions/mpl-head/action.yml @@ -0,0 +1,45 @@ +name: "Check Out and update files with MPL-HEAD" +description: "Updates the MPL submodule to point at HEAD and updates the files that depend on the version defined in project.properties" +inputs: + update-and-regenerate-mpl: + description: "Locally update MPL to the tip of master and regenerate its code" + required: true + default: false + type: boolean +runs: + using: "composite" + steps: + - name: Update MPL submodule locally if requested + if: inputs.update-and-regenerate-mpl == 'true' + working-directory: submodules/MaterialProviders + shell: bash + run: | + git fetch + git checkout main + git pull + git submodule update --init --recursive + + - name: Update top-level project.properties file in MPL + if: inputs.update-and-regenerate-mpl == 'true' + shell: bash + working-directory: submodules/MaterialProviders + run: | + make generate_properties_file + + # Update the project.properties file so that we pick up the right runtimes etc., + # in cases where inputs.dafny is different from the current value in that file. + - name: Generate smithy-dafny-project.properties file + if: inputs.update-and-regenerate-mpl == 'true' + env: + DAFNY_VERSION: ${{ inputs.dafny }} + shell: bash + run: | + make generate_properties_file + + - name: Update top-level project.properties file + if: inputs.update-and-regenerate-mpl == 'true' + shell: bash + run: | + awk -F= '!a[$1]++' smithy-dafny-project.properties project.properties > merged.properties + mv merged.properties project.properties + cat project.properties diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index d81cd2a00..73b2eb0aa 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -7,6 +7,11 @@ on: description: "The dafny version to run" required: true type: string + mpl-head: + description: "Using MPL HEAD" + required: false + default: false + type: boolean jobs: code-generation: @@ -34,6 +39,11 @@ jobs: with: submodules: recursive + - uses: ./.github/actions/mpl-head + if: ${{ inputs.mpl-head == true }} + with: + update-and-regenerate-mpl: true + # Only used to format generated code # and to translate version strings such as "nightly-latest" # to an actual DAFNY_VERSION. diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index ecb2544fa..9f49bd6ed 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -21,9 +21,10 @@ jobs: mpl-head-ci-codegen: needs: getVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/actions/mpl-head/mpl_head_codegen.yml + uses: ./.github/workflows/ci_codegen.yml with: dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true # mpl-head-ci-verification: # needs: getVerifyVersion # if: github.event_name != 'schedule' || github.repository_owner == 'aws' From 8a325e8f273357d889759032d3fc947de7a39df6 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 16:58:01 -0700 Subject: [PATCH 04/20] pass in dafny version --- .github/actions/mpl-head/action.yml | 4 ++ .github/actions/mpl-head/mpl_head_codegen.yml | 70 ------------------- .github/workflows/ci_codegen.yml | 1 + 3 files changed, 5 insertions(+), 70 deletions(-) delete mode 100644 .github/actions/mpl-head/mpl_head_codegen.yml diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index 8a819a37c..00ac90506 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -1,6 +1,10 @@ name: "Check Out and update files with MPL-HEAD" description: "Updates the MPL submodule to point at HEAD and updates the files that depend on the version defined in project.properties" inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string update-and-regenerate-mpl: description: "Locally update MPL to the tip of master and regenerate its code" required: true diff --git a/.github/actions/mpl-head/mpl_head_codegen.yml b/.github/actions/mpl-head/mpl_head_codegen.yml deleted file mode 100644 index 79022dade..000000000 --- a/.github/actions/mpl-head/mpl_head_codegen.yml +++ /dev/null @@ -1,70 +0,0 @@ -# This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in -# with the latest mpl head -name: Library-MPL-HEAD Code Generation -on: - workflow_call: - inputs: - dafny: - description: "The dafny version to run" - required: true - type: string - -jobs: - code-generation: - strategy: - fail-fast: false - matrix: - library: [DynamoDbEncryption, TestVectors] - # Note dotnet is only used for formatting generated code - # in this workflow - dotnet-version: ["6.0.x"] - os: [ubuntu-latest] - runs-on: ${{ matrix.os }} - defaults: - run: - shell: bash - env: - DOTNET_CLI_TELEMETRY_OPTOUT: 1 - DOTNET_NOLOGO: 1 - steps: - - name: Support longpaths - run: | - git config --global core.longpaths true - - - uses: actions/checkout@v3 - with: - submodules: recursive - - - name: Update MPL submodule - working-directory: submodules/MaterialProviders - shell: bash - run: | - git checkout main - git pull - git submodule update --init --recursive - - - name: Read MPL Version from its properties file - id: read_property - uses: christian-draeger/read-properties@1.1.1 - with: - path: "submodules/MaterialProviders/project.properties" - properties: "mplVersion" - - # Only used to format generated code - # and to translate version strings such as "nightly-latest" - # to an actual DAFNY_VERSION. - - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 - with: - dafny-version: ${{ inputs.dafny }} - - - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} - uses: actions/setup-dotnet@v4 - with: - dotnet-version: ${{ matrix.dotnet-version }} - - - uses: ./.github/actions/polymorph_codegen - with: - dafny: ${{ env.DAFNY_VERSION }} - library: ${{ matrix.library }} - diff-generated-code: true diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index 73b2eb0aa..e8d034539 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -42,6 +42,7 @@ jobs: - uses: ./.github/actions/mpl-head if: ${{ inputs.mpl-head == true }} with: + dafny: ${{ env.DAFNY_VERSION }} update-and-regenerate-mpl: true # Only used to format generated code From 986d73564ee525385931d3889041462545aa7303 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 17:01:05 -0700 Subject: [PATCH 05/20] update --- .github/workflows/ci_codegen.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index e8d034539..3002d5d5f 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -30,6 +30,7 @@ jobs: env: DOTNET_CLI_TELEMETRY_OPTOUT: 1 DOTNET_NOLOGO: 1 + DAFNY_VERSION: ${{inputs.dafny}} steps: - name: Support longpaths run: | From 85d0f6984182b011a7c29f3636901d0b9f44523f Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 17:11:48 -0700 Subject: [PATCH 06/20] a --- .github/actions/mpl-head/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index 00ac90506..a90838e63 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -18,10 +18,10 @@ runs: working-directory: submodules/MaterialProviders shell: bash run: | - git fetch git checkout main git pull git submodule update --init --recursive + cat project.properties - name: Update top-level project.properties file in MPL if: inputs.update-and-regenerate-mpl == 'true' From 989acc245059766e27e30f0d580cb8695c3c3f04 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 17:19:49 -0700 Subject: [PATCH 07/20] a --- .github/actions/mpl-head/action.yml | 28 ++++++++-------------------- 1 file changed, 8 insertions(+), 20 deletions(-) diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index a90838e63..a5a6edf75 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -22,28 +22,16 @@ runs: git pull git submodule update --init --recursive cat project.properties - - - name: Update top-level project.properties file in MPL - if: inputs.update-and-regenerate-mpl == 'true' - shell: bash - working-directory: submodules/MaterialProviders - run: | - make generate_properties_file - - # Update the project.properties file so that we pick up the right runtimes etc., - # in cases where inputs.dafny is different from the current value in that file. - - name: Generate smithy-dafny-project.properties file - if: inputs.update-and-regenerate-mpl == 'true' - env: - DAFNY_VERSION: ${{ inputs.dafny }} - shell: bash - run: | - make generate_properties_file + + - name: Get the MPL version from the MPL submodule + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "submodules/MaterialProviders//project.properties" + properties: "mplVersion" - name: Update top-level project.properties file - if: inputs.update-and-regenerate-mpl == 'true' shell: bash run: | - awk -F= '!a[$1]++' smithy-dafny-project.properties project.properties > merged.properties - mv merged.properties project.properties + echo ${{ steps.read_property.outputs.mplVersion }} cat project.properties From 64dfa0e3034ade2307f954e03d19f5e619e307ce Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 10 Jul 2024 17:40:08 -0700 Subject: [PATCH 08/20] ? --- .github/actions/mpl-head/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index a5a6edf75..05fc8ef3a 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -33,5 +33,5 @@ runs: - name: Update top-level project.properties file shell: bash run: | - echo ${{ steps.read_property.outputs.mplVersion }} + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties cat project.properties From 321387919dc01ba4e489162722a4d148205d71bb Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 11:28:08 -0700 Subject: [PATCH 09/20] update --- .github/actions/mpl-head/action.yml | 4 +--- .github/workflows/ci_codegen.yml | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index 05fc8ef3a..b3ba86e82 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -21,7 +21,6 @@ runs: git checkout main git pull git submodule update --init --recursive - cat project.properties - name: Get the MPL version from the MPL submodule id: read_property @@ -33,5 +32,4 @@ runs: - name: Update top-level project.properties file shell: bash run: | - sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties - cat project.properties + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties \ No newline at end of file diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index 3002d5d5f..e8d034539 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -30,7 +30,6 @@ jobs: env: DOTNET_CLI_TELEMETRY_OPTOUT: 1 DOTNET_NOLOGO: 1 - DAFNY_VERSION: ${{inputs.dafny}} steps: - name: Support longpaths run: | From 1ed256599c488c8715d7fa21b625c95c55f25f5d Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 12:15:43 -0700 Subject: [PATCH 10/20] no codegen for mpl head tests --- .github/actions/mpl-head/action.yml | 6 +++--- .github/workflows/ci_codegen.yml | 11 ----------- .github/workflows/library_dafny_verification.yml | 11 +++++++++++ .github/workflows/mpl-head.yml | 14 ++++---------- 4 files changed, 18 insertions(+), 24 deletions(-) diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml index b3ba86e82..dc5e0d6ce 100644 --- a/.github/actions/mpl-head/action.yml +++ b/.github/actions/mpl-head/action.yml @@ -21,15 +21,15 @@ runs: git checkout main git pull git submodule update --init --recursive - + - name: Get the MPL version from the MPL submodule id: read_property uses: christian-draeger/read-properties@1.1.1 with: - path: "submodules/MaterialProviders//project.properties" + path: "submodules/MaterialProviders/project.properties" properties: "mplVersion" - name: Update top-level project.properties file shell: bash run: | - sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties \ No newline at end of file + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml index e8d034539..d81cd2a00 100644 --- a/.github/workflows/ci_codegen.yml +++ b/.github/workflows/ci_codegen.yml @@ -7,11 +7,6 @@ on: description: "The dafny version to run" required: true type: string - mpl-head: - description: "Using MPL HEAD" - required: false - default: false - type: boolean jobs: code-generation: @@ -39,12 +34,6 @@ jobs: with: submodules: recursive - - uses: ./.github/actions/mpl-head - if: ${{ inputs.mpl-head == true }} - with: - dafny: ${{ env.DAFNY_VERSION }} - update-and-regenerate-mpl: true - # Only used to format generated code # and to translate version strings such as "nightly-latest" # to an actual DAFNY_VERSION. diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index dda360ec6..ba4eac77c 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Using MPL HEAD" + required: false + default: false + type: boolean jobs: verification: @@ -47,6 +52,12 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - uses: ./.github/actions/mpl-head + if: ${{ inputs.mpl-head == true }} + with: + dafny: ${{ env.DAFNY_VERSION }} + update-and-regenerate-mpl: true + # dafny-reportgenerator requires next6 # but only 7.0 is installed on macos-12-large - name: Setup .NET Core SDK '6.0.x' diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 9f49bd6ed..06dc4d42b 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -18,19 +18,13 @@ jobs: uses: ./.github/workflows/library_format.yml with: dafny: ${{needs.getVersion.outputs.version}} - mpl-head-ci-codegen: - needs: getVersion + mpl-head-ci-verification: + needs: getVerifyVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' - uses: ./.github/workflows/ci_codegen.yml + uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: ${{needs.getVersion.outputs.version}} + dafny: ${{needs.getVerifyVersion.outputs.version}} mpl-head: true - # mpl-head-ci-verification: - # needs: getVerifyVersion - # if: github.event_name != 'schedule' || github.repository_owner == 'aws' - # uses: ./.github/workflows/library_dafny_verification.yml - # with: - # dafny: ${{needs.getVerifyVersion.outputs.version}} # mpl-head-ci-test-vector-verification: # needs: getVerifyVersion # uses: ./.github/workflows/test_vector_verification.yml From e6fd8e97b105866170478d384aa72ba819f11f07 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 13:50:37 -0700 Subject: [PATCH 11/20] update verification --- .../workflows/library_dafny_verification.yml | 25 ++++++++++---- .github/workflows/mpl-head.yml | 7 ++-- .github/workflows/mpl_head_version.yml | 34 +++++++++++++++++++ 3 files changed, 57 insertions(+), 9 deletions(-) create mode 100644 .github/workflows/mpl_head_version.yml diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index ba4eac77c..f30420fa5 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -13,8 +13,12 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string mpl-head: - description: "Using MPL HEAD" + description: "Running on MPL HEAD" required: false default: false type: boolean @@ -52,11 +56,18 @@ jobs: with: dafny-version: ${{ inputs.dafny }} - - uses: ./.github/actions/mpl-head + - name: Update MPL submodule if using MPL HEAD if: ${{ inputs.mpl-head == true }} - with: - dafny: ${{ env.DAFNY_VERSION }} - update-and-regenerate-mpl: true + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties # dafny-reportgenerator requires next6 # but only 7.0 is installed on macos-12-large @@ -74,7 +85,7 @@ jobs: diff-generated-code: false - name: Verify ${{ matrix.library }} Dafny code - working-directory: ./DynamoDbEncryption + working-directory: DynamoDbEncryption run: | # This works because `node` is installed by default on GHA runners CORES=$(node -e 'console.log(os.cpus().length)') @@ -82,6 +93,6 @@ jobs: - name: Check solver resource use if: success() || failure() - working-directory: ./DynamoDbEncryption + working-directory: DynamoDbEncryption run: | make dafny-reportgenerator diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 06dc4d42b..8cbdddb43 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -12,6 +12,9 @@ jobs: getVerifyVersion: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/dafny_verify_version.yml + getMplHeadVersion: + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/mpl_head_version.yml mpl-head-ci-format: needs: getVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' @@ -19,12 +22,12 @@ jobs: with: dafny: ${{needs.getVersion.outputs.version}} mpl-head-ci-verification: - needs: getVerifyVersion + needs: [getVerifyVersion, getMplHeadVersion] if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_dafny_verification.yml with: dafny: ${{needs.getVerifyVersion.outputs.version}} - mpl-head: true + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} # mpl-head-ci-test-vector-verification: # needs: getVerifyVersion # uses: ./.github/workflows/test_vector_verification.yml diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml new file mode 100644 index 000000000..c4f9c73d1 --- /dev/null +++ b/.github/workflows/mpl_head_version.yml @@ -0,0 +1,34 @@ +# This workflow reads the project.properties +# into the environment variables +# and then creates an output variable for `dafnyVerifyVersion ` +name: MPL HEAD Version + +on: + workflow_call: + outputs: + version: + description: "The dafny version for verify" + value: ${{ jobs.getMplHeadVersion.outputs.version }} + +jobs: + getMplHeadVersion: + runs-on: ubuntu-latest + outputs: + version: ${{ steps.read_property.outputs.mplVersion }} + steps: + - uses: actions/checkout@v4 + - name: Update MPL submodule locally if requested + if: inputs.update-and-regenerate-mpl == 'true' + working-directory: submodules/MaterialProviders + shell: bash + run: | + git checkout main + git pull + git submodule update --init --recursive + + - name: Get the MPL version from the MPL submodule + id: read_property + uses: christian-draeger/read-properties@1.1.1 + with: + path: "submodules/MaterialProviders/project.properties" + properties: "mplVersion" From 23f37be7a1b8f9ec88644e407da374961b88c115 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 13:55:50 -0700 Subject: [PATCH 12/20] update --- .github/workflows/mpl_head_version.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index c4f9c73d1..d99baf9de 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -18,7 +18,6 @@ jobs: steps: - uses: actions/checkout@v4 - name: Update MPL submodule locally if requested - if: inputs.update-and-regenerate-mpl == 'true' working-directory: submodules/MaterialProviders shell: bash run: | From 04fb95368d2eaa06694a3ade21222298551fa7ac Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 13:58:21 -0700 Subject: [PATCH 13/20] recurse submodules --- .github/workflows/mpl_head_version.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index d99baf9de..4b2692b63 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -17,6 +17,8 @@ jobs: version: ${{ steps.read_property.outputs.mplVersion }} steps: - uses: actions/checkout@v4 + with: + submodules: recursive - name: Update MPL submodule locally if requested working-directory: submodules/MaterialProviders shell: bash From 7030c571583e61134ae239218351a4cd31c48849 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 14:00:25 -0700 Subject: [PATCH 14/20] use mpl head --- .github/workflows/mpl-head.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 8cbdddb43..01a0b724d 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -28,6 +28,7 @@ jobs: with: dafny: ${{needs.getVerifyVersion.outputs.version}} mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true # mpl-head-ci-test-vector-verification: # needs: getVerifyVersion # uses: ./.github/workflows/test_vector_verification.yml From e57354fe6202f9d03028f9bf6121d70a559d344d Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 14:23:38 -0700 Subject: [PATCH 15/20] a --- .github/actions/mpl-head/action.yml | 35 ------------------- .../workflows/library_dafny_verification.yml | 1 + .github/workflows/mpl-head.yml | 13 +++---- .github/workflows/mpl_head_version.yml | 1 + .../workflows/test_vector_verification.yml | 23 ++++++++++++ 5 files changed, 32 insertions(+), 41 deletions(-) delete mode 100644 .github/actions/mpl-head/action.yml diff --git a/.github/actions/mpl-head/action.yml b/.github/actions/mpl-head/action.yml deleted file mode 100644 index dc5e0d6ce..000000000 --- a/.github/actions/mpl-head/action.yml +++ /dev/null @@ -1,35 +0,0 @@ -name: "Check Out and update files with MPL-HEAD" -description: "Updates the MPL submodule to point at HEAD and updates the files that depend on the version defined in project.properties" -inputs: - dafny: - description: "The Dafny version to run" - required: true - type: string - update-and-regenerate-mpl: - description: "Locally update MPL to the tip of master and regenerate its code" - required: true - default: false - type: boolean -runs: - using: "composite" - steps: - - name: Update MPL submodule locally if requested - if: inputs.update-and-regenerate-mpl == 'true' - working-directory: submodules/MaterialProviders - shell: bash - run: | - git checkout main - git pull - git submodule update --init --recursive - - - name: Get the MPL version from the MPL submodule - id: read_property - uses: christian-draeger/read-properties@1.1.1 - with: - path: "submodules/MaterialProviders/project.properties" - properties: "mplVersion" - - - name: Update top-level project.properties file - shell: bash - run: | - sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{steps.read_property.outputs.mplVersion}}/g" project.properties > project.properties2; mv project.properties2 project.properties diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index f30420fa5..f25a216b2 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -63,6 +63,7 @@ jobs: git checkout main git pull git submodule update --init --recursive + git rev-parse HEAD - name: Update project.properties if using MPL HEAD if: ${{ inputs.mpl-head == true }} diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 01a0b724d..790ff3057 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -29,12 +29,13 @@ jobs: dafny: ${{needs.getVerifyVersion.outputs.version}} mpl-version: ${{needs.getMplHeadVersion.outputs.version}} mpl-head: true - # mpl-head-ci-test-vector-verification: - # needs: getVerifyVersion - # uses: ./.github/workflows/test_vector_verification.yml - # with: - # dafny: ${{needs.getVerifyVersion.outputs.version}} - # mpl-head: true + mpl-head-ci-test-vector-verification: + needs: getVerifyVersion + uses: ./.github/workflows/test_vector_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true # mpl-head-ci-java-test-vectors: # needs: getVersion # uses: ./.github/workflows/ci_test_vector_java.yml diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml index 4b2692b63..094825a9a 100644 --- a/.github/workflows/mpl_head_version.yml +++ b/.github/workflows/mpl_head_version.yml @@ -26,6 +26,7 @@ jobs: git checkout main git pull git submodule update --init --recursive + git rev-parse HEAD - name: Get the MPL version from the MPL submodule id: read_property diff --git a/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml index e6de4b5f6..a787c9b8a 100644 --- a/.github/workflows/test_vector_verification.yml +++ b/.github/workflows/test_vector_verification.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: verification: @@ -37,6 +46,20 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} + + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties # dafny-reportgenerator requires next6 # but only 7.0 is installed on macos-12-large From 039735310c7a4d6f0a212ee65313c38d213745bb Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 14:48:58 -0700 Subject: [PATCH 16/20] check out mpl head for java testing --- .github/workflows/ci_examples_java.yml | 23 ++++++++++++ .github/workflows/ci_test_java.yml | 23 ++++++++++++ .github/workflows/ci_test_vector_java.yml | 23 ++++++++++++ .github/workflows/daily_ci.yml | 5 +++ .github/workflows/mpl-head.yml | 35 ++++++++++++------- .../workflows/test_vector_verification.yml | 2 +- 6 files changed, 97 insertions(+), 14 deletions(-) diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml index 48d51d356..558b2b583 100644 --- a/.github/workflows/ci_examples_java.yml +++ b/.github/workflows/ci_examples_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -48,6 +57,20 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml index a4e9a26be..f96748878 100644 --- a/.github/workflows/ci_test_java.yml +++ b/.github/workflows/ci_test_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -42,6 +51,20 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml index 707fd1a16..13549d90d 100644 --- a/.github/workflows/ci_test_vector_java.yml +++ b/.github/workflows/ci_test_vector_java.yml @@ -13,6 +13,15 @@ on: required: false default: false type: boolean + mpl-version: + description: "MPL version to use" + required: false + type: string + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testJava: @@ -51,6 +60,20 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Update project.properties if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + run: | + sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index 2edd6273a..cc047fcab 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -36,6 +36,11 @@ jobs: uses: ./.github/workflows/test_vector_verification.yml with: dafny: ${{needs.getVerifyVersion.outputs.version}} + daily-ci-java: + needs: getVersion + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} daily-ci-java-test-vectors: needs: getVersion uses: ./.github/workflows/ci_test_vector_java.yml diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 790ff3057..97601f8dc 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -30,24 +30,33 @@ jobs: mpl-version: ${{needs.getMplHeadVersion.outputs.version}} mpl-head: true mpl-head-ci-test-vector-verification: - needs: getVerifyVersion + needs: [getVerifyVersion, getMplHeadVersion] uses: ./.github/workflows/test_vector_verification.yml with: dafny: ${{needs.getVerifyVersion.outputs.version}} mpl-version: ${{needs.getMplHeadVersion.outputs.version}} mpl-head: true - # mpl-head-ci-java-test-vectors: - # needs: getVersion - # uses: ./.github/workflows/ci_test_vector_java.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true - # mpl-headci-java-examples: - # needs: getVersion - # uses: ./.github/workflows/ci_examples_java.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + mpl-head-ci-java: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-head-ci-java-test-vectors: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true + mpl-headci-java-examples: + needs: [getVersion, getMplHeadVersion] + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-version: ${{needs.getMplHeadVersion.outputs.version}} + mpl-head: true # mpl-head-ci-net: # needs: getVersion # uses: ./.github/workflows/ci_test_net.yml diff --git a/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml index a787c9b8a..118808829 100644 --- a/.github/workflows/test_vector_verification.yml +++ b/.github/workflows/test_vector_verification.yml @@ -46,7 +46,7 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} - + - name: Update MPL submodule if using MPL HEAD if: ${{ inputs.mpl-head == true }} working-directory: submodules/MaterialProviders From 21755919c1c33b08b6ef3ee926affc4c9c8d0583 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 16:37:08 -0700 Subject: [PATCH 17/20] u --- TestVectors/runtimes/java/build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/runtimes/java/build.gradle.kts b/TestVectors/runtimes/java/build.gradle.kts index ee1439b90..a00006e2d 100644 --- a/TestVectors/runtimes/java/build.gradle.kts +++ b/TestVectors/runtimes/java/build.gradle.kts @@ -90,7 +90,7 @@ dependencies { implementation("software.amazon.smithy.dafny:conversion:${smithyDafnyJavaConversionVersion}") implementation("software.amazon.cryptography:aws-cryptographic-material-providers:${mplVersion}") implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:${ddbecVersion}") - implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:1.0-SNAPSHOT") + implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:${mplVersion}") implementation(platform("software.amazon.awssdk:bom:2.24.2")) implementation("software.amazon.awssdk:dynamodb") From 3aeef6ff2bd21b0e31c7e770131244735802ceeb Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 16:50:00 -0700 Subject: [PATCH 18/20] enable dotnet in mpl head build --- .github/workflows/ci_examples_net.yml | 14 +++++++++ .github/workflows/ci_test_net.yml | 14 +++++++++ .github/workflows/ci_test_vector_net.yml | 14 +++++++++ .github/workflows/mpl-head.yml | 38 ++++++++++++------------ 4 files changed, 61 insertions(+), 19 deletions(-) diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml index 5c5f47a0f..9d6d7eef6 100644 --- a/.github/workflows/ci_examples_net.yml +++ b/.github/workflows/ci_examples_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: dotNetExamples: @@ -45,6 +50,15 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml index 5e0bf8d39..8ead30d1f 100644 --- a/.github/workflows/ci_test_net.yml +++ b/.github/workflows/ci_test_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testDotNet: @@ -46,6 +51,15 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index c39ab9e96..e2fdff24e 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -13,6 +13,11 @@ on: required: false default: false type: boolean + mpl-head: + description: "Running on MPL HEAD" + required: false + default: false + type: boolean jobs: testDotNet: @@ -51,6 +56,15 @@ jobs: with: dafny-version: ${{ inputs.dafny }} + - name: Update MPL submodule if using MPL HEAD + if: ${{ inputs.mpl-head == true }} + working-directory: submodules/MaterialProviders + run: | + git checkout main + git pull + git submodule update --init --recursive + git rev-parse HEAD + - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.regenerate-code }} uses: ./.github/actions/polymorph_codegen diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 97601f8dc..0dbdd8cae 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -50,28 +50,28 @@ jobs: dafny: ${{needs.getVersion.outputs.version}} mpl-version: ${{needs.getMplHeadVersion.outputs.version}} mpl-head: true - mpl-headci-java-examples: + mpl-head-ci-java-examples: needs: [getVersion, getMplHeadVersion] uses: ./.github/workflows/ci_examples_java.yml with: dafny: ${{needs.getVersion.outputs.version}} mpl-version: ${{needs.getMplHeadVersion.outputs.version}} mpl-head: true - # mpl-head-ci-net: - # needs: getVersion - # uses: ./.github/workflows/ci_test_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true - # mpl-head-ci-net-test-vectors: - # needs: getVersion - # uses: ./.github/workflows/ci_test_vector_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true - # mpl-head-ci-net-examples: - # needs: getVersion - # uses: ./.github/workflows/ci_examples_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # mpl-head: true + mpl-head-ci-net: + needs: getVersion + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true + mpl-head-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true + mpl-head-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + mpl-head: true From 7792af98f5cfc82ce982499ec3af2c4084cdd29f Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 16:57:15 -0700 Subject: [PATCH 19/20] make mpl-head a cron job --- .github/workflows/mpl-head.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/mpl-head.yml b/.github/workflows/mpl-head.yml index 0dbdd8cae..6bb7e1b7c 100644 --- a/.github/workflows/mpl-head.yml +++ b/.github/workflows/mpl-head.yml @@ -2,7 +2,8 @@ name: CI MPL HEAD on: - pull_request: + schedule: + - cron: "00 14 * * 1-5" jobs: getVersion: From 2f3ece37d7459b3a0ef8713bad1bb3d55ac86fc5 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 11 Jul 2024 17:14:51 -0700 Subject: [PATCH 20/20] update --- TestVectors/runtimes/java/build.gradle.kts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/TestVectors/runtimes/java/build.gradle.kts b/TestVectors/runtimes/java/build.gradle.kts index a00006e2d..ae608f1a9 100644 --- a/TestVectors/runtimes/java/build.gradle.kts +++ b/TestVectors/runtimes/java/build.gradle.kts @@ -28,6 +28,7 @@ var dafnyRuntimeJavaVersion = props.getProperty("dafnyRuntimeJavaVersion") var smithyDafnyJavaConversionVersion = props.getProperty("smithyDafnyJavaConversionVersion") group = "software.amazon.cryptography" +// change to ${mplVersion} for next MPL update version = "1.0-SNAPSHOT" description = "TestVectorsDynamoDbEncryption" @@ -90,7 +91,8 @@ dependencies { implementation("software.amazon.smithy.dafny:conversion:${smithyDafnyJavaConversionVersion}") implementation("software.amazon.cryptography:aws-cryptographic-material-providers:${mplVersion}") implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:${ddbecVersion}") - implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:${mplVersion}") + // change to ${mplVersion} for next MPL update + implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:1.0-SNAPSHOT") implementation(platform("software.amazon.awssdk:bom:2.24.2")) implementation("software.amazon.awssdk:dynamodb")