Skip to content

No labels!

There aren’t any labels for this repository quite yet.

79 labels

Sort
Sort
Alphabetically
Reverse alphabetically
Most issues
Fewest issues
dependencies
dependencies
Pull requests that update a dependency file
depends on new code generator
depends on new code generator
We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it
52
dev meeting
dev meeting
It will be discussed at the (next) dev meeting
4
documentation
documentation
Documentation improvement
3
duplicate
duplicate
This issue or pull request already exists
elaboration
elaboration
Affects the elaborator
1
enhancement
enhancement
New feature or request
70
error message
error message
Error message produced by Lean is confusing or not informative
3
feature
feature
missing feature
20
good first issue
good first issue
Good for newcomers
help wanted
help wanted
Extra attention is needed
11
invalid
invalid
This doesn't seem right
Lake
Lake
Lake related issue
47
language
language
Lean language issue or PR
1
lean4_release
lean4_release
Must be addressed before first official release
3
low priority
low priority
33
Mathlib4 high prio
Mathlib4 high prio
Mathlib4 high priority issue
2
merge-ci
merge-ci
Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms.
1
missing documentation
missing documentation
PR is missing documentation
1
missing mwe
missing mwe
Issue is missing an example to reproduce the problem, or the example is not reproducible
missing release notes
missing release notes
Please add a short bullet point to RELEASES.md
missing RFC
missing RFC
Non trivial PR was submitted before RFC has been created
1
missing tests
missing tests
This PR requires the addition of tests before it can be merged.
1
needs-update-stage0
needs-update-stage0
stage 0 should be updated after merging this PR
2
new-user-papercuts
new-user-papercuts
Issue likely to confuse or otherwise negatively affect new users, even if only a little
8
nice to have
nice to have
Cool feature that would be really nice to have
4
no plans to address
no plans to address
The core developers are not planning to address this issue any time soon. It is super low priority.
P-high
P-high
We will work on this issue
33
P-low
P-low
We are not planning to work on this issue
142
P-medium
P-medium
We may work on this issue if we find the time
200