Skip to content

Issues: leanprover/lean4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

512 Open 971 Closed
512 Open 971 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Suggestion on Document: Explicit Declaration for Multiple Universe Level Variable
#4122 opened May 10, 2024 by DKXXXL
@david-christiansen
3
allow using an upstream executable as a lake @[test_runner] feature missing feature Lake Lake related issue
#4121 opened May 10, 2024 by semorrison
Stack overflow on malformed input bug Something isn't working
#4117 opened May 9, 2024 by TwoFX
3 tasks done
lake test --help gives lakefile.lean specific instructions (i.e. not toml) documentation Documentation improvement Lake Lake related issue
#4116 opened May 9, 2024 by semorrison
@tydeu
Pattern alternative binding empty type does not cause redundant alternative warning bug Something isn't working
#4110 opened May 8, 2024 by lovely-error
10
lake translate-config does not give a helpful error message feature missing feature Lake Lake related issue
#4107 opened May 8, 2024 by semorrison
@tydeu
2
lake new should generate a lakefile.toml, not a lakefile.lean Lake Lake related issue new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little RFC Request for comments
#4106 opened May 8, 2024 by semorrison
lake should give a warning when it looks like nothing is imported, by accident Lake Lake related issue new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little RFC Request for comments
#4105 opened May 8, 2024 by semorrison
@tydeu
4
lake update should print a warning, if moving dependencies to a later toolchain than the local toolchain error message Error message produced by Lean is confusing or not informative feature missing feature Lake Lake related issue new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little
#4103 opened May 8, 2024 by semorrison
@tydeu
3
simpa type mismatch error message could be improved bug Something isn't working
#4101 opened May 7, 2024 by kmill
RFC: let unfold tactic zeta reduce local definitions RFC Request for comments
#4090 opened May 7, 2024 by kmill
1
elab_as_elim does not support function application in resulting motive arguments bug Something isn't working
#4086 opened May 7, 2024 by JamesGallicchio
1 task done
Renaming a variable also renames another variable bug Something isn't working
#4081 opened May 6, 2024 by mik-jozef
1 task done
3
Refactoring elab exception handling
#4079 opened May 6, 2024 by Kha
3 tasks
2
Rpc Error when hovering variable bug Something isn't working
#4078 opened May 6, 2024 by hargoniX
1 task done
'Building X' diagnostic for every dependency when processing imports bug Something isn't working Lake Lake related issue server Affects the Lean server code
#4069 opened May 5, 2024 by bustercopley
1 task done
1
rw? regression from v4.7.0 bug Something isn't working
#4062 opened May 4, 2024 by Seasawher
2
Hashes for Expr.lam and Expr.forallE are the same bug Something isn't working
#4060 opened May 3, 2024 by kmill
1
lake puts relative paths in LD_LIBRARY_PATH bug Something isn't working Lake Lake related issue
#4042 opened May 1, 2024 by eric-wieser
1 task done
set_option trace.compiler.ffi_accessors feature missing feature nice to have Cool feature that would be really nice to have
#4041 opened May 1, 2024 by digama0
RFC: simp control over recursive functions (or lemmas) RFC Request for comments
#4027 opened Apr 29, 2024 by nomeata
4
RFC: Lake init/new should create empty README.md (maybe with # $ProjectName) Lake Lake related issue RFC Request for comments
#4017 opened Apr 28, 2024 by alok
Nix builds have empty githash bug Something isn't working
#4015 opened Apr 28, 2024 by enricozb
1 task done
14
error message of register_label_attr bug Something isn't working pr-welcome A PR from an external contributor, implementing the RFC as described, would be welcome.
#4011 opened Apr 28, 2024 by Seasawher
1 task done
1
Redundant =?= in elabTermEnsuringType bug Something isn't working
#3993 opened Apr 26, 2024 by nomeata
ProTip! no:milestone will show everything without a milestone.