Skip to content

Commit b2f70ca

Browse files
josecorellajosecorella
authored
chore(GHA): add action for testing against MPL HEAD (#1187)
1 parent a1427e0 commit b2f70ca

12 files changed

+280
-2
lines changed

Diff for: ‎.github/workflows/ci_examples_java.yml

+23
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,15 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-version:
17+
description: "MPL version to use"
18+
required: false
19+
type: string
20+
mpl-head:
21+
description: "Running on MPL HEAD"
22+
required: false
23+
default: false
24+
type: boolean
1625

1726
jobs:
1827
testJava:
@@ -48,6 +57,20 @@ jobs:
4857
with:
4958
dafny-version: ${{ inputs.dafny }}
5059

60+
- name: Update MPL submodule if using MPL HEAD
61+
if: ${{ inputs.mpl-head == true }}
62+
working-directory: submodules/MaterialProviders
63+
run: |
64+
git checkout main
65+
git pull
66+
git submodule update --init --recursive
67+
git rev-parse HEAD
68+
69+
- name: Update project.properties if using MPL HEAD
70+
if: ${{ inputs.mpl-head == true }}
71+
run: |
72+
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
73+
5174
- name: Regenerate code using smithy-dafny if necessary
5275
if: ${{ inputs.regenerate-code }}
5376
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/ci_examples_net.yml

+14
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,11 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-head:
17+
description: "Running on MPL HEAD"
18+
required: false
19+
default: false
20+
type: boolean
1621

1722
jobs:
1823
dotNetExamples:
@@ -45,6 +50,15 @@ jobs:
4550
with:
4651
dafny-version: ${{ inputs.dafny }}
4752

53+
- name: Update MPL submodule if using MPL HEAD
54+
if: ${{ inputs.mpl-head == true }}
55+
working-directory: submodules/MaterialProviders
56+
run: |
57+
git checkout main
58+
git pull
59+
git submodule update --init --recursive
60+
git rev-parse HEAD
61+
4862
- name: Regenerate code using smithy-dafny if necessary
4963
if: ${{ inputs.regenerate-code }}
5064
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/ci_test_java.yml

+23
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,15 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-version:
17+
description: "MPL version to use"
18+
required: false
19+
type: string
20+
mpl-head:
21+
description: "Running on MPL HEAD"
22+
required: false
23+
default: false
24+
type: boolean
1625

1726
jobs:
1827
testJava:
@@ -42,6 +51,20 @@ jobs:
4251
with:
4352
dafny-version: ${{ inputs.dafny }}
4453

54+
- name: Update MPL submodule if using MPL HEAD
55+
if: ${{ inputs.mpl-head == true }}
56+
working-directory: submodules/MaterialProviders
57+
run: |
58+
git checkout main
59+
git pull
60+
git submodule update --init --recursive
61+
git rev-parse HEAD
62+
63+
- name: Update project.properties if using MPL HEAD
64+
if: ${{ inputs.mpl-head == true }}
65+
run: |
66+
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
67+
4568
- name: Regenerate code using smithy-dafny if necessary
4669
if: ${{ inputs.regenerate-code }}
4770
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/ci_test_net.yml

+14
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,11 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-head:
17+
description: "Running on MPL HEAD"
18+
required: false
19+
default: false
20+
type: boolean
1621

1722
jobs:
1823
testDotNet:
@@ -46,6 +51,15 @@ jobs:
4651
with:
4752
dafny-version: ${{ inputs.dafny }}
4853

54+
- name: Update MPL submodule if using MPL HEAD
55+
if: ${{ inputs.mpl-head == true }}
56+
working-directory: submodules/MaterialProviders
57+
run: |
58+
git checkout main
59+
git pull
60+
git submodule update --init --recursive
61+
git rev-parse HEAD
62+
4963
- name: Regenerate code using smithy-dafny if necessary
5064
if: ${{ inputs.regenerate-code }}
5165
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/ci_test_vector_java.yml

+23
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,15 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-version:
17+
description: "MPL version to use"
18+
required: false
19+
type: string
20+
mpl-head:
21+
description: "Running on MPL HEAD"
22+
required: false
23+
default: false
24+
type: boolean
1625

1726
jobs:
1827
testJava:
@@ -51,6 +60,20 @@ jobs:
5160
with:
5261
dafny-version: ${{ inputs.dafny }}
5362

63+
- name: Update MPL submodule if using MPL HEAD
64+
if: ${{ inputs.mpl-head == true }}
65+
working-directory: submodules/MaterialProviders
66+
run: |
67+
git checkout main
68+
git pull
69+
git submodule update --init --recursive
70+
git rev-parse HEAD
71+
72+
- name: Update project.properties if using MPL HEAD
73+
if: ${{ inputs.mpl-head == true }}
74+
run: |
75+
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
76+
5477
- name: Regenerate code using smithy-dafny if necessary
5578
if: ${{ inputs.regenerate-code }}
5679
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/ci_test_vector_net.yml

+14
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,11 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-head:
17+
description: "Running on MPL HEAD"
18+
required: false
19+
default: false
20+
type: boolean
1621

1722
jobs:
1823
testDotNet:
@@ -51,6 +56,15 @@ jobs:
5156
with:
5257
dafny-version: ${{ inputs.dafny }}
5358

59+
- name: Update MPL submodule if using MPL HEAD
60+
if: ${{ inputs.mpl-head == true }}
61+
working-directory: submodules/MaterialProviders
62+
run: |
63+
git checkout main
64+
git pull
65+
git submodule update --init --recursive
66+
git rev-parse HEAD
67+
5468
- name: Regenerate code using smithy-dafny if necessary
5569
if: ${{ inputs.regenerate-code }}
5670
uses: ./.github/actions/polymorph_codegen

Diff for: ‎.github/workflows/daily_ci.yml

+5
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,11 @@ jobs:
3636
uses: ./.github/workflows/test_vector_verification.yml
3737
with:
3838
dafny: ${{needs.getVerifyVersion.outputs.version}}
39+
daily-ci-java:
40+
needs: getVersion
41+
uses: ./.github/workflows/ci_test_java.yml
42+
with:
43+
dafny: ${{needs.getVersion.outputs.version}}
3944
daily-ci-java-test-vectors:
4045
needs: getVersion
4146
uses: ./.github/workflows/ci_test_vector_java.yml

Diff for: ‎.github/workflows/library_dafny_verification.yml

+25-2
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,15 @@ on:
1313
required: false
1414
default: false
1515
type: boolean
16+
mpl-version:
17+
description: "MPL version to use"
18+
required: false
19+
type: string
20+
mpl-head:
21+
description: "Running on MPL HEAD"
22+
required: false
23+
default: false
24+
type: boolean
1625

1726
jobs:
1827
verification:
@@ -47,6 +56,20 @@ jobs:
4756
with:
4857
dafny-version: ${{ inputs.dafny }}
4958

59+
- name: Update MPL submodule if using MPL HEAD
60+
if: ${{ inputs.mpl-head == true }}
61+
working-directory: submodules/MaterialProviders
62+
run: |
63+
git checkout main
64+
git pull
65+
git submodule update --init --recursive
66+
git rev-parse HEAD
67+
68+
- name: Update project.properties if using MPL HEAD
69+
if: ${{ inputs.mpl-head == true }}
70+
run: |
71+
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
72+
5073
# dafny-reportgenerator requires next6
5174
# but only 7.0 is installed on macos-12-large
5275
- name: Setup .NET Core SDK '6.0.x'
@@ -63,14 +86,14 @@ jobs:
6386
diff-generated-code: false
6487

6588
- name: Verify ${{ matrix.library }} Dafny code
66-
working-directory: ./DynamoDbEncryption
89+
working-directory: DynamoDbEncryption
6790
run: |
6891
# This works because `node` is installed by default on GHA runners
6992
CORES=$(node -e 'console.log(os.cpus().length)')
7093
make verify_service CORES=$CORES SERVICE=${{ matrix.library }}
7194
7295
- name: Check solver resource use
7396
if: success() || failure()
74-
working-directory: ./DynamoDbEncryption
97+
working-directory: DynamoDbEncryption
7598
run: |
7699
make dafny-reportgenerator

Diff for: ‎.github/workflows/mpl-head.yml

+78
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
# This workflow invokes other workflows with the latest MPL head at 14:00 UTC (7am PDT)
2+
name: CI MPL HEAD
3+
4+
on:
5+
schedule:
6+
- cron: "00 14 * * 1-5"
7+
8+
jobs:
9+
getVersion:
10+
# Don't run the cron builds on forks
11+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
12+
uses: ./.github/workflows/dafny_version.yml
13+
getVerifyVersion:
14+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
15+
uses: ./.github/workflows/dafny_verify_version.yml
16+
getMplHeadVersion:
17+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
18+
uses: ./.github/workflows/mpl_head_version.yml
19+
mpl-head-ci-format:
20+
needs: getVersion
21+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
22+
uses: ./.github/workflows/library_format.yml
23+
with:
24+
dafny: ${{needs.getVersion.outputs.version}}
25+
mpl-head-ci-verification:
26+
needs: [getVerifyVersion, getMplHeadVersion]
27+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
28+
uses: ./.github/workflows/library_dafny_verification.yml
29+
with:
30+
dafny: ${{needs.getVerifyVersion.outputs.version}}
31+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
32+
mpl-head: true
33+
mpl-head-ci-test-vector-verification:
34+
needs: [getVerifyVersion, getMplHeadVersion]
35+
uses: ./.github/workflows/test_vector_verification.yml
36+
with:
37+
dafny: ${{needs.getVerifyVersion.outputs.version}}
38+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
39+
mpl-head: true
40+
mpl-head-ci-java:
41+
needs: [getVersion, getMplHeadVersion]
42+
uses: ./.github/workflows/ci_test_java.yml
43+
with:
44+
dafny: ${{needs.getVersion.outputs.version}}
45+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
46+
mpl-head: true
47+
mpl-head-ci-java-test-vectors:
48+
needs: [getVersion, getMplHeadVersion]
49+
uses: ./.github/workflows/ci_test_vector_java.yml
50+
with:
51+
dafny: ${{needs.getVersion.outputs.version}}
52+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
53+
mpl-head: true
54+
mpl-head-ci-java-examples:
55+
needs: [getVersion, getMplHeadVersion]
56+
uses: ./.github/workflows/ci_examples_java.yml
57+
with:
58+
dafny: ${{needs.getVersion.outputs.version}}
59+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
60+
mpl-head: true
61+
mpl-head-ci-net:
62+
needs: getVersion
63+
uses: ./.github/workflows/ci_test_net.yml
64+
with:
65+
dafny: ${{needs.getVersion.outputs.version}}
66+
mpl-head: true
67+
mpl-head-ci-net-test-vectors:
68+
needs: getVersion
69+
uses: ./.github/workflows/ci_test_vector_net.yml
70+
with:
71+
dafny: ${{needs.getVersion.outputs.version}}
72+
mpl-head: true
73+
mpl-head-ci-net-examples:
74+
needs: getVersion
75+
uses: ./.github/workflows/ci_examples_net.yml
76+
with:
77+
dafny: ${{needs.getVersion.outputs.version}}
78+
mpl-head: true

Diff for: ‎.github/workflows/mpl_head_version.yml

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# This workflow reads the project.properties
2+
# into the environment variables
3+
# and then creates an output variable for `dafnyVerifyVersion `
4+
name: MPL HEAD Version
5+
6+
on:
7+
workflow_call:
8+
outputs:
9+
version:
10+
description: "The dafny version for verify"
11+
value: ${{ jobs.getMplHeadVersion.outputs.version }}
12+
13+
jobs:
14+
getMplHeadVersion:
15+
runs-on: ubuntu-latest
16+
outputs:
17+
version: ${{ steps.read_property.outputs.mplVersion }}
18+
steps:
19+
- uses: actions/checkout@v4
20+
with:
21+
submodules: recursive
22+
- name: Update MPL submodule locally if requested
23+
working-directory: submodules/MaterialProviders
24+
shell: bash
25+
run: |
26+
git checkout main
27+
git pull
28+
git submodule update --init --recursive
29+
git rev-parse HEAD
30+
31+
- name: Get the MPL version from the MPL submodule
32+
id: read_property
33+
uses: christian-draeger/[email protected]
34+
with:
35+
path: "submodules/MaterialProviders/project.properties"
36+
properties: "mplVersion"

0 commit comments

Comments
 (0)