[Merged by Bors] - refactor(Order/OmegaCompletePartialOrder): make Chain a structure
#11596
Workflow file for this run
This file contains hidden or 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
| name: Add "closed-pr" emoji in Zulip | |
| # adds a reaction to Zulip messages that refer to a PR that was closed, but not merged | |
| # triggers the action when | |
| on: | |
| pull_request_target: | |
| # the pull request is closed or reopened, to add or remove the emoji | |
| types: [closed, reopened] | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read # minimum permissions for actions/checkout & actions/setup-python | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| add_closed_pr_emoji: | |
| # we set the `TITLE` of the PR as a variable, this shields from possible code injection | |
| env: | |
| TITLE: ${{ github.event.pull_request.title }} | |
| name: Add closed-pr emoji in Zulip | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' || | |
| github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| steps: | |
| - name: Debugging information | |
| run: | | |
| # may be superfluous: GitHub may print the values of the environment variables by default | |
| printf '%s' "${TITLE}" | hexdump -cC | |
| printf 'PR title:"%s"\n' "${TITLE}" | |
| printf 'issue number: "%s"\npull request number: "%s"\n' "${{ github.event.issue.number }}" "${{ github.event.pull_request.number }}" | |
| - name: Checkout local actions | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| ref: ${{ github.workflow_sha }} | |
| fetch-depth: 1 | |
| sparse-checkout: .github/actions | |
| path: workflow-actions | |
| - name: Checkout mathlib-ci | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| uses: ./workflow-actions/.github/actions/get-mathlib-ci | |
| - name: Set up Python | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0 | |
| with: | |
| python-version: '3.x' | |
| - name: Install dependencies | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt" | |
| - name: Update zulip emoji reactions | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| continue-on-error: true | |
| env: | |
| ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} | |
| ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com | |
| ZULIP_SITE: https://leanprover.zulipchat.com | |
| run: | | |
| # ${{ github.event.action }} is either "closed" or "reopened" | |
| # We add the "closed-pr" emoji to the message, if it is "closed" | |
| # and remove the emoji if the action is "reopen". | |
| python "${CI_SCRIPTS_DIR}/zulip/zulip_emoji_reactions.py" "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ github.event.action }}" "none" "${{ github.event.pull_request.number }}" |