|
| 1 | +# |
| 2 | +# This local action serves two purposes: |
| 3 | +# |
| 4 | +# 1. For core workflows like pull.yml and push.yml, |
| 5 | +# it is uses to check that the checked in copy of generated code |
| 6 | +# matches what the current submodule version of smithy-dafny generates. |
| 7 | +# This is important to ensure whenever someone changes the models |
| 8 | +# or needs to regenerate to pick up smithy-dafny improvements, |
| 9 | +# they don't have to deal with unpleasant surprises. |
| 10 | +# |
| 11 | +# 2. For workflows that check compatibility with other Dafny versions, |
| 12 | +# such as nightly_dafny.yml, it is necessary to regenerate the code |
| 13 | +# for that version of Dafny first. |
| 14 | +# This is ultimately because some of the code smithy-dafny generates |
| 15 | +# is tightly coupled to what code Dafny itself generates. |
| 16 | +# A concrete example is that Dafny 4.3 added TypeDescriptors |
| 17 | +# as parameters when constructing datatypes like Option and Result. |
| 18 | +# |
| 19 | +# This is why this is a composite action instead of a reusable workflow: |
| 20 | +# the latter executes in a separate runner environment, |
| 21 | +# but here we need to actually overwrite the generated code in place |
| 22 | +# so that subsequent steps can work correctly. |
| 23 | +# |
| 24 | +# This action assumes that the given version of Dafny and .NET 6.0.x |
| 25 | +# have already been set up, since they are used to format generated code. |
| 26 | +# |
| 27 | +# Note that recursively generating code doesn't currently work in this repo |
| 28 | +# with the version of the mpl pinned by the submodule, |
| 29 | +# because the SharedMakefileV2.mk in it doesn't work with newer versions of smithy-dafny. |
| 30 | +# Therefore by default we don't recursively regenerate code |
| 31 | +# (accomplished by setting the POLYMORPH_DEPENDENCIES environment variable to ""). |
| 32 | +# If `update-and-regenerate-mpl` is true, we first pull the latest mpl, |
| 33 | +# which is necessary both for Makefile compatibility and so we can regenerate mpl code |
| 34 | +# for compatibility with newer versions of Dafny. |
| 35 | +# |
| 36 | + |
| 37 | +name: "Polymorph code generation" |
| 38 | +description: "Regenerates code using smithy-dafny, and optionally checks that the result matches the checked in state" |
| 39 | +inputs: |
| 40 | + dafny: |
| 41 | + description: "The Dafny version to run" |
| 42 | + required: true |
| 43 | + type: string |
| 44 | + library: |
| 45 | + description: "Name of the library to regenerate code for" |
| 46 | + required: true |
| 47 | + type: string |
| 48 | + diff-generated-code: |
| 49 | + description: "Diff regenerated code against committed state" |
| 50 | + required: true |
| 51 | + type: boolean |
| 52 | + update-and-regenerate-mpl: |
| 53 | + description: "Locally update MPL to the tip of master and regenerate its code too" |
| 54 | + required: false |
| 55 | + default: false |
| 56 | + type: boolean |
| 57 | +runs: |
| 58 | + using: "composite" |
| 59 | + steps: |
| 60 | + - name: Update MPL submodule locally if requested |
| 61 | + if: inputs.update-and-regenerate-mpl == 'true' |
| 62 | + working-directory: submodules/MaterialProviders |
| 63 | + shell: bash |
| 64 | + run: | |
| 65 | + git checkout main |
| 66 | + git pull |
| 67 | + git submodule update --init --recursive |
| 68 | +
|
| 69 | + - name: Update top-level project.properties file in MPL |
| 70 | + if: inputs.update-and-regenerate-mpl == 'true' |
| 71 | + shell: bash |
| 72 | + working-directory: submodules/MaterialProviders |
| 73 | + run: | |
| 74 | + make generate_properties_file |
| 75 | +
|
| 76 | + # Update the project.properties file so that we pick up the right runtimes etc., |
| 77 | + # in cases where inputs.dafny is different from the current value in that file. |
| 78 | + - name: Generate smithy-dafny-project.properties file |
| 79 | + if: inputs.update-and-regenerate-mpl == 'true' |
| 80 | + env: |
| 81 | + DAFNY_VERSION: ${{ inputs.dafny }} |
| 82 | + shell: bash |
| 83 | + run: | |
| 84 | + make generate_properties_file |
| 85 | +
|
| 86 | + - name: Update top-level project.properties file |
| 87 | + if: inputs.update-and-regenerate-mpl == 'true' |
| 88 | + shell: bash |
| 89 | + run: | |
| 90 | + awk -F= '!a[$1]++' smithy-dafny-project.properties project.properties > merged.properties |
| 91 | + mv merged.properties project.properties |
| 92 | + cat project.properties |
| 93 | +
|
| 94 | + - name: Don't regenerate dependencies unless requested |
| 95 | + id: dependencies |
| 96 | + shell: bash |
| 97 | + run: | |
| 98 | + echo "PROJECT_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'PROJECT_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT |
| 99 | +
|
| 100 | + - name: Regenerate Dafny code using smithy-dafny |
| 101 | + # Unfortunately Dafny codegen doesn't work on Windows: |
| 102 | + # https://github.com/smithy-lang/smithy-dafny/issues/317 |
| 103 | + if: runner.os != 'Windows' |
| 104 | + working-directory: ./${{ inputs.library }} |
| 105 | + shell: bash |
| 106 | + run: | |
| 107 | + make polymorph_dafny ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} |
| 108 | +
|
| 109 | + - name: Set up prettier in MPL |
| 110 | + if: inputs.update-and-regenerate-mpl == 'true' |
| 111 | + shell: bash |
| 112 | + # Annoyingly, prettier has to be installed in each library individually. |
| 113 | + # And this is only necessary or even possible if we've updated the mpl submodule. |
| 114 | + run: | |
| 115 | + make -C submodules/MaterialProviders/AwsCryptographyPrimitives setup_prettier |
| 116 | + make -C submodules/MaterialProviders/AwsCryptographicMaterialProviders setup_prettier |
| 117 | + make -C submodules/MaterialProviders/ComAmazonawsKms setup_prettier |
| 118 | + make -C submodules/MaterialProviders/ComAmazonawsDynamodb setup_prettier |
| 119 | +
|
| 120 | + - name: Regenerate Java code using smithy-dafny |
| 121 | + # npx seems to be unavailable on Windows GHA runners, |
| 122 | + # so we don't regenerate Java code on them either. |
| 123 | + if: runner.os != 'Windows' |
| 124 | + working-directory: ./${{ inputs.library }} |
| 125 | + shell: bash |
| 126 | + # smithy-dafny also formats generated code itself now, |
| 127 | + # so prettier is a necessary dependency. |
| 128 | + run: | |
| 129 | + make setup_prettier |
| 130 | + make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} |
| 131 | +
|
| 132 | + - name: Regenerate .NET code using smithy-dafny |
| 133 | + working-directory: ./${{ inputs.library }} |
| 134 | + shell: bash |
| 135 | + run: | |
| 136 | + make polymorph_dotnet ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} |
| 137 | +
|
| 138 | + - name: Check regenerated code against commited code |
| 139 | + # Composite action inputs seem to not actually support booleans properly for some reason |
| 140 | + if: inputs.diff-generated-code == 'true' |
| 141 | + working-directory: ./${{ inputs.library }} |
| 142 | + shell: bash |
| 143 | + run: | |
| 144 | + make check_polymorph_diff |
0 commit comments