Skip to content

Issues: leanprover-community/lean

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

107 Open 98 Closed
107 Open 98 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
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

leanittest_complete_trailing_period.lean test fails (99% tests passed, 1 tests failed out of 1441)
#816 opened Sep 3, 2024 by barracuda156
Segmentation fault when using get_env with run_tactic
#803 opened Mar 15, 2023 by lenianiva
1 task done
1
"Invalid return type" error when definining inductive propositions can be attached to more suitable text range
#802 opened Feb 25, 2023 by ddrone
1 task done
1
pp.links handles unit.star badly
#789 opened Dec 2, 2022 by eric-wieser
1 task done
opening a namespace can affect elaboration
#776 opened Oct 26, 2022 by alexjbest
local notation can change explicitness of arguments bug Something isn't working
#772 opened Sep 26, 2022 by fpvandoorn
clang prints warnings: use reference type ... to prevent copying
#767 opened Sep 5, 2022 by yurivict
Simple programs run for many seconds
#765 opened Sep 1, 2022 by yurivict
1 task done
8
Failures in get_peak_rss() should fail the application instead of silently returning 0
#763 opened Aug 31, 2022 by yurivict
1 task done
Kernel failed to type-check due to name collision involving include bug Something isn't working
#751 opened Jul 29, 2022 by Vierkantor
1 task done
exceptions when saving oleans are not user-visible
#750 opened Jul 29, 2022 by collares
1 task done
is_bi_equal use of BinderInfo-unaware hashes causes many collisions (a.k.a. timeout when saving oleans)
#749 opened Jul 29, 2022 by collares
1 task done
Assertion failure in local_context_adapter.cpp
#748 opened Jul 29, 2022 by eric-wieser
1 task done
1
native.rb_map.insert not working as expected
#738 opened Jul 10, 2022 by isadofschi
1 task done
2
invalid synthesis of reflected instances
#731 opened Jun 16, 2022 by eric-wieser
1 task done
Cannot build .olean file on NFS
#718 opened May 21, 2022 by Longhao-Chen
1 task done
6
Test failure on i686 (32 bit)
#685 opened Feb 19, 2022 by tornaria
1 task done
"kernel failed to type check declaration" in presence of implicit coercion to Sort
#672 opened Jan 25, 2022 by kmill
1 task done
universe error in definition generated by the equation compiler
#655 opened Dec 10, 2021 by robertylewis
1 task
apply tactic produces incorrect proof
#644 opened Nov 1, 2021 by gebner
1
segfault in badly typed pattern match
#625 opened Sep 22, 2021 by robertylewis
1 task
CI: Flaky test on macos debug runs
#624 opened Sep 22, 2021 by bryangingechen
simp ignores direction of equation lemmas
#623 opened Sep 21, 2021 by eric-wieser
1 task done
(No equational lemmas)/(Mistaken as field notation) when using a namespace inside a section with universe polymorphism
#613 opened Sep 6, 2021 by winestone
1 task done
Repeat tactic does not terminate instead of giving an error or functioning as it should.
#584 opened Jun 20, 2021 by Karthik-Dulam
1 task done
1
ProTip! no:milestone will show everything without a milestone.