Labels

• awaiting-author

  awaiting-author

  Waiting for PR author to address issues

• awaiting-manual

  awaiting-manual

  We should not merge this until there is a successful build of the Lean Language Reference

• awaiting-mathlib

  awaiting-mathlib

  We should not merge this until we have a successful Mathlib build

• awaiting-review

  awaiting-review

  Waiting for someone to review the PR

• backport releases/v4.18.0

  backport releases/v4.18.0

• backport releases/v4.19.0

  backport releases/v4.19.0

• backport releases/v4.20.0

  backport releases/v4.20.0

• backport releases/v4.22.0

  backport releases/v4.22.0

• backport releases/v4.23.0

  backport releases/v4.23.0

• backport releases/v4.24.0

  backport releases/v4.24.0

• backport releases/v4.25.0

  backport releases/v4.25.0

• backport releases/v4.26.0

  backport releases/v4.26.0

• backport releases/v4.27.0

  backport releases/v4.27.0

• backport releases/v4.28.0

  backport releases/v4.28.0

• backport releases/v4.29.0

  backport releases/v4.29.0

• backport releases/v4.30.0

  backport releases/v4.30.0

• backport releases/v4.31.0

  backport releases/v4.31.0

• backport releases/v4.32.0

  backport releases/v4.32.0

• blocks-release-v4.29.0

  blocks-release-v4.29.0

  Blocks the next v4.29.0 release candidate or release from being published.

• blocks-release-v4.30.0

  blocks-release-v4.30.0

  Blocks the next v4.30.0 release candidate or release from being published.

• blocks-release-v4.31.0

  blocks-release-v4.31.0

  Blocks the next v4.31.0 release candidate or release from being published.

• blocks-release-v4.32.0

  blocks-release-v4.32.0

  Blocks the next v4.32.0 release candidate or release from being published.

• blocks-release-v4.33.0

  blocks-release-v4.33.0

  Blocks the next v4.33.0 release candidate or release from being published.

• breaks-manual

  breaks-manual

  This is not necessarily a blocker for merging, but there needs to be a plan.

• breaks-mathlib

  breaks-mathlib

  This is not necessarily a blocker for merging: but there needs to be a plan

• bug

  bug

  Something isn't working

• builds-manual

  builds-manual

  CI has verified that the Lean Language Reference builds against this PR

• builds-mathlib

  builds-mathlib

  CI has verified that Mathlib builds against this PR

• changelog-compiler

  changelog-compiler

  Compiler, runtime, and FFI

• changelog-doc

  changelog-doc

  Documentation