Labels

• awaiting-author

  A reviewer has asked the author a question or requested changes
• awaiting-CI

  The author would like to see what CI has to say before doing more work.
• awaiting-review

  The author would like community review of the PR
• blocked-by-other-PR

  This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
• blocked-by-out-of-sync-queue

  The #outofsync queue must have at most 20 items
• bug
• CI

  This issue or PR is about continuous integration
• delegated

  The PR author may merge after reviewing final suggestions.
• docs

  This PR is about documentation
• duplicate
• easy

  < 20s of review time. See the lifecycle page for guidelines.
• enhancement
• feature-request

  This issue is a feature request, either for mathematics, tactics, or CI
• good-first-project
• hacktoberfest-accepted

  Without this label hacktoberfest is scared off by bors
• hard
• help-wanted

  The author needs attention to resolve issues
• imo

  Formalisation of an IMO problem
• incomplete
• invalid
• lean-gptf

  Co-authored by `lean-gptf`
• linter
• lintfix

  This PR only fixes linting errors
• long term
• mathlib4-synchronization

  This PR *only* adds a message to the module doc about synchronization with mathlib4
• mathport

  For compatibility with Lean 4 changes, to simplify porting
• maybe-later
• medium
• merge-conflict

  Please `git merge origin/master` then a bot will remove this label.
• modifies-synchronized-file

  This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.