feat(Topology/Connected): local (path-)connectedness of products and pi types #256594
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: bot fix style | |
| # triggers the action when | |
| on: | |
| issue_comment: | |
| # the PR receives a comment, or a comment is edited | |
| types: [created, edited] | |
| pull_request_review: | |
| # triggers on a review, whether or not it is accompanied by a comment | |
| types: [submitted] | |
| pull_request_review_comment: | |
| # triggers on a review comment | |
| types: [created, edited] | |
| # `lint-style-action` in `fix` mode pushes a style-fix commit and reacts/comments | |
| # on the PR. Grant exactly those scopes rather than inheriting the default token | |
| # permissions; all other scopes are implicitly 'none'. | |
| permissions: | |
| contents: write # push the style-fix commit to the PR branch | |
| pull-requests: write # add the bot's reaction/comment | |
| issues: write # PR comment reactions go through the issues API | |
| jobs: | |
| fix_style: | |
| # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not | |
| # both set simultaneously: depending on the event that triggers the PR, usually only one is set | |
| env: | |
| AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }} | |
| COMMENT_EVENT: ${{ github.event.comment.body }} | |
| COMMENT_REVIEW: ${{ github.event.review.body }} | |
| COMMENT_REVIEW_COMMENT: ${{ github.event.pull_request_review_comment.body }} | |
| name: Fix style issues from lint | |
| # the `if` works with `comment`s, but not with `review`s or `review_comment`s | |
| # if: github.event.issue.pull_request | |
| # && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style')) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18 | |
| with: | |
| mode: fix | |
| lint-bib-file: true | |
| BOT_FIX_STYLE_TOKEN: ${{ secrets.GITHUB_TOKEN }} |