feat(RingTheory/TensorProduct/Pi): add piScalarRight_symm_apply_algebraMap
#4877
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' | |
| 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: Set up Python | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.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 zulip | |
| - name: checkout the zulip_emoji_reactions script | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| ref: master | |
| sparse-checkout: | | |
| scripts/zulip_emoji_reactions.py | |
| - name: Update zulip emoji reactions | |
| if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') || | |
| github.event_name == 'reopened' }} | |
| 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 scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ github.event.action }}" "none" "${{ github.event.pull_request.number }}" |