Labels

• awaiting-author

  awaiting-author

  A reviewer has asked the author a question or requested changes

• awaiting-CI

  awaiting-CI

  The author would like to see what CI has to say before doing more work.

• awaiting-review

  awaiting-review

  The author would like community review of the PR

• blocked-by-other-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

  blocked-by-out-of-sync-queue

  The #outofsync queue must have at most 20 items

• bug

  bug

• CI

  CI

  This issue or PR is about continuous integration

• delegated

  delegated

  The PR author may merge after reviewing final suggestions.

• docs

  docs

  This PR is about documentation

• duplicate

  duplicate

• easy

  easy

  < 20s of review time. See the lifecycle page for guidelines.

• enhancement

  enhancement

• feature-request

  feature-request

  This issue is a feature request, either for mathematics, tactics, or CI

• good-first-project

  good-first-project

• hacktoberfest-accepted

  hacktoberfest-accepted

  Without this label hacktoberfest is scared off by bors

• hard

  hard

• help-wanted

  help-wanted

  The author needs attention to resolve issues

• imo

  imo

  Formalisation of an IMO problem

• incomplete

  incomplete

• invalid

  invalid

• lean-gptf

  lean-gptf

  Co-authored by `lean-gptf`

• linter

  linter

• lintfix

  lintfix

  This PR only fixes linting errors

• long term

  long term

• mathlib4-synchronization

  mathlib4-synchronization

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

• mathport

  mathport

  For compatibility with Lean 4 changes, to simplify porting

• maybe-later

  maybe-later

• medium

  medium

• merge-conflict

  merge-conflict

  Please `git merge origin/master` then a bot will remove this label.

• modifies-synchronized-file

  modifies-synchronized-file

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