chore: sync public with staging #2
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This workflow performs static analysis checks. | |
| name: Library Dafny verification | |
| on: | |
| pull_request: | |
| push: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| # Manual trigger for this workflow, either the normal version | |
| # or the nightly build that uses the latest Dafny prerelease | |
| # (accordingly to the "nightly" parameter). | |
| inputs: | |
| nightly: | |
| description: 'Run the nightly build' | |
| required: false | |
| type: boolean | |
| schedule: | |
| # Nightly build against Dafny's nightly prereleases, | |
| # for early warning of verification issues or regressions. | |
| # Timing chosen to be adequately after Dafny's own nightly build, | |
| # but this might need to be tweaked: | |
| # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 | |
| - cron: "30 16 * * *" | |
| jobs: | |
| verification: | |
| # Don't run the nightly build on forks | |
| if: github.event_name != 'schedule' || github.repository_owner == 'aws' | |
| strategy: | |
| matrix: | |
| library: [ | |
| AwsEncryptionSDK | |
| ] | |
| os: [ macos-latest ] | |
| runs-on: ${{ matrix.os }} | |
| environment: "MPL_DAFNY" | |
| env: | |
| DOTNET_CLI_TELEMETRY_OPTOUT: 1 | |
| DOTNET_NOLOGO: 1 | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Init Submodules | |
| env: | |
| # This secret is in the configured environment | |
| # Token created on # 09/26/2023 | |
| # expires in ~30 days 10/26/2023 | |
| MPL_PAT: ${{ secrets.MPL_DAFNY }} | |
| run: | | |
| AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')" | |
| git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH" | |
| git config --global --add url.https://github.com/.insteadOf [email protected]: | |
| git submodule update --init libraries | |
| git submodule update --init --recursive mpl | |
| - name: Support longpaths | |
| run: | | |
| git config --global core.longpaths true | |
| - name: Setup Dafny | |
| uses: dafny-lang/[email protected] | |
| with: | |
| # 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: Verify ${{ matrix.library }} Dafny code | |
| shell: bash | |
| working-directory: ./${{ matrix.library }} | |
| run: | | |
| # This works because `node` is installed by default on GHA runners | |
| CORES=$(node -e 'console.log(os.cpus().length)') | |
| make verify CORES=$CORES | |
| - name: Check solver resource use | |
| shell: bash | |
| working-directory: ./${{ matrix.library }} | |
| run: | | |
| make dafny-reportgenerator |