Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / leanprover/lean4 issues and pull requests
#3291 - chore: upstream Std's linter framework
Pull Request -
State: open - Opened by kim-em 9 months ago
- 2 comments
Labels: WIP
#3287 - doc: mention maxSteps setting in its error message
Pull Request -
State: open - Opened by BoltonBailey 9 months ago
- 2 comments
Labels: awaiting-author, toolchain-available
#3219 - "failed to generate equational theorem" with nested matches
Issue -
State: open - Opened by soulsource 10 months ago
- 2 comments
Labels: bug, P-medium
#3215 - feat: enforce indentation of command contents
Pull Request -
State: open - Opened by Kha 10 months ago
- 5 comments
Labels: breaks-mathlib, toolchain-available
#3213 - Eta-expansion of `Prop`-structures
Issue -
State: open - Opened by arthur-adjedj 10 months ago
Labels: bug, P-low
#3211 - RFC: Support http proxy
Issue -
State: open - Opened by Landau1994 10 months ago
- 1 comment
Labels: RFC, P-low
#3192 - LLVM vs C backend performance
Issue -
State: closed - Opened by hargoniX 10 months ago
- 2 comments
Labels: bug
#3182 - fix: make lean4 build on FreeBSD
Pull Request -
State: open - Opened by yurivict 10 months ago
- 2 comments
Labels: awaiting-author, toolchain-available
#3181 - Please make installing LICENSE and LICENSES files optional based on a cmake option
Issue -
State: closed - Opened by yurivict 10 months ago
- 6 comments
Labels: bug
#3177 - lean4 installs files into a non-standard location src/lean
Issue -
State: open - Opened by yurivict 10 months ago
- 20 comments
Labels: bug, P-low
#3174 - feat: lake: `require` overhaul
Pull Request -
State: open - Opened by tydeu 10 months ago
- 3 comments
Labels: WIP, builds-mathlib, toolchain-available
#3166 - refactor: lake: API cleanup / mark some defs `private`
Pull Request -
State: open - Opened by tydeu 10 months ago
- 3 comments
Labels: builds-mathlib, toolchain-available
#3162 - RFC: Signed Fixed-width Integer Support
Issue -
State: open - Opened by pnwamk 10 months ago
- 8 comments
Labels: RFC, P-high
#3161 - feat: profile instructions on Linux
Pull Request -
State: open - Opened by Kha 10 months ago
- 6 comments
Labels: builds-mathlib, toolchain-available
#3160 - feat: manage nested inductive types in `deriving`
Pull Request -
State: closed - Opened by arthur-adjedj 10 months ago
- 31 comments
Labels: awaiting-review, breaks-mathlib, toolchain-available, P-medium
#3152 - fix: reduce let-bodies correctly in `StructInst`
Pull Request -
State: open - Opened by arthur-adjedj 10 months ago
- 1 comment
Labels: awaiting-review, builds-mathlib, toolchain-available, P-medium
#3150 - Bug leading to stack overflow
Issue -
State: open - Opened by alreadydone 10 months ago
- 5 comments
Labels: bug, P-medium
#3146 - Unification bug
Issue -
State: open - Opened by jthulhu 10 months ago
Labels: bug, P-medium
#3127 - feat: make constructor tactic fail in ambiguous cases
Pull Request -
State: open - Opened by hrmacbeth 11 months ago
- 5 comments
Labels: WIP, builds-mathlib, toolchain-available
#3102 - fix: remove `Option.lt` and related components
Pull Request -
State: open - Opened by linesthatinterlace 11 months ago
- 13 comments
Labels: builds-mathlib, toolchain-available
#2710 - noncomputable structure defaults cannot be marked noncomputable
Issue -
State: closed - Opened by eric-wieser about 1 year ago
Labels: bug
#2695 - fix: universe inference for `Prop`-valued structures/inductives
Pull Request -
State: closed - Opened by arthur-adjedj about 1 year ago
- 2 comments
Labels: WIP, breaks-mathlib, toolchain-available
#2542 - feat: lake: add `lake dump-config` command
Pull Request -
State: open - Opened by digama0 about 1 year ago
- 18 comments
Labels: toolchain-available
#2524 - Delaboration of re-exported names
Issue -
State: open - Opened by hargoniX about 1 year ago
- 3 comments
#2459 - fix: deprecation span should only cover the ident
Pull Request -
State: open - Opened by digama0 about 1 year ago
- 1 comment
Labels: awaiting-author
#2374 - `#eval` on `let rec` causes error in kernel
Issue -
State: closed - Opened by Vierkantor over 1 year ago
#2355 - fix: bug in gen_injective_theorems%
Pull Request -
State: open - Opened by digama0 over 1 year ago
Labels: awaiting-author
#2335 - Sort messages by position when printing
Pull Request -
State: open - Opened by Kha over 1 year ago
- 4 comments
Labels: awaiting-author
#2293 - Make token parser customizable
Pull Request -
State: open - Opened by Kha over 1 year ago
- 10 comments
Labels: awaiting-author, dev meeting
#2276 - fix: respect type reducibility when generating injectivity lemmas
Pull Request -
State: open - Opened by eric-wieser over 1 year ago
- 2 comments
Labels: awaiting-author, awaiting-review, missing RFC
#2267 - feat: `eta_reduce_fun%` in cdot parser, v2
Pull Request -
State: open - Opened by digama0 over 1 year ago
Labels: low priority, awaiting-author
#2263 - feat: `eta_reduce_fun%` in cdot parser
Pull Request -
State: open - Opened by digama0 over 1 year ago
- 1 comment
Labels: low priority, awaiting-author
#2239 - fix: resolve `_root_` in `macro`, `syntax`, `elab`
Pull Request -
State: open - Opened by digama0 over 1 year ago
- 9 comments
Labels: needs-update-stage0, awaiting-author, toolchain-available
#2204 - Issue finding `Inhabited` instances in partial definition
Issue -
State: open - Opened by fgdorais over 1 year ago
- 3 comments
#2112 - fix: prepend underscore on autogenerated 'proof_{n}' constant names
Pull Request -
State: open - Opened by dwrensha over 1 year ago
Labels: low priority
#2105 - chore: use binderIdent consistently in grammar
Pull Request -
State: open - Opened by digama0 almost 2 years ago
Labels: awaiting-author
#2094 - fix: #include <mutex> in mutex.cpp
Pull Request -
State: open - Opened by iacore almost 2 years ago
- 2 comments
Labels: awaiting-author
#2090 - fix: LLVM backend: detect size_t from target triple
Pull Request -
State: open - Opened by iacore almost 2 years ago
- 13 comments
Labels: awaiting-review
#2083 - [cmake] Build Files Generator not pinned to Unix Makefiles
Issue -
State: closed - Opened by iacore almost 2 years ago
- 3 comments
#2060 - Use `Bool.asProp` for coercions
Pull Request -
State: open - Opened by gebner almost 2 years ago
- 4 comments
#2058 - Confusing error message with unassigned metavariables
Issue -
State: closed - Opened by gebner almost 2 years ago
- 2 comments
Labels: P-medium
#2044 - Auto-generated instance names do not inherit macro scopes
Issue -
State: closed - Opened by Vtec234 almost 2 years ago
#2038 - Make `Decidable` a subtype of `Bool`
Pull Request -
State: open - Opened by gebner almost 2 years ago
- 8 comments
Labels: dev meeting
#1967 - feat: support MessageData in #eval
Pull Request -
State: open - Opened by gebner almost 2 years ago
Labels: dev meeting
#1928 - doc: document Lean.Elab.StructInst
Pull Request -
State: open - Opened by thorimur almost 2 years ago
#1913 - chore: CI: enable emulated tests on Linux aarch64
Pull Request -
State: open - Opened by gebner almost 2 years ago
- 1 comment
#1910 - Dot notation and `CoeFun`
Issue -
State: closed - Opened by Vtec234 almost 2 years ago
- 1 comment
Labels: RFC
#1897 - chore: normalize naming convention in theorems
Pull Request -
State: open - Opened by digama0 almost 2 years ago
- 4 comments
#1867 - passing instances to named arguments turns explicit args into implicit
Issue -
State: open - Opened by digama0 almost 2 years ago
- 4 comments
#1774 - compiler produces `(kernel) function expected`
Issue -
State: open - Opened by fpfu about 2 years ago
- 1 comment
Labels: depends on new code generator
#1749 - feat: `show` tactic (full version)
Pull Request -
State: open - Opened by digama0 about 2 years ago
- 2 comments
Labels: awaiting-author
#1665 - [WIP] feat: Suggest tactic
Pull Request -
State: open - Opened by EdAyers about 2 years ago
Labels: awaiting-author
#1651 - Completion for tactics
Issue -
State: closed - Opened by digama0 about 2 years ago
- 1 comment
Labels: server
#738 - Asynchronous printing hangs the server
Issue -
State: open - Opened by tydeu about 3 years ago
- 5 comments
Labels: bug, low priority
#100 - define mutable quotients
Pull Request -
State: closed - Opened by cipher1024 almost 5 years ago
- 1 comment
#99 - Optimize syntax category antiquotations
Issue -
State: closed - Opened by Kha almost 5 years ago
#98 - doc: try naming result type
Pull Request -
State: closed - Opened by dselsam almost 5 years ago
- 1 comment
#97 - fix: lowercase error messages
Pull Request -
State: closed - Opened by cipher1024 almost 5 years ago
- 1 comment
#96 - fix: DiscrTree typos
Pull Request -
State: closed - Opened by dselsam almost 5 years ago
- 1 comment
#95 - Add std streams (depends on #84)
Pull Request -
State: closed - Opened by cipher1024 almost 5 years ago
- 1 comment
#94 - parser/macro macros
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#93 - Add command quotations
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#92 - feat: track macro scopes in CommandElab and synchronize them with TermElab
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 2 comments
#91 - fix: typo in SynthInstance.lean
Pull Request -
State: closed - Opened by dselsam almost 5 years ago
- 1 comment
#90 - fix: dead link in doc
Pull Request -
State: closed - Opened by dselsam almost 5 years ago
- 1 comment
#89 - refactor: use more quotations in the elaborator
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#88 - Antiquotation kinds
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 5 comments
#87 - CI: check for memory leaks in tests & stdlib
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#86 - Fix memory leaks
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#85 - Support (almost) proper name resolution in quotations in the old frontend
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#84 - Io api
Pull Request -
State: closed - Opened by cipher1024 almost 5 years ago
- 7 comments
#83 - Flesh out quotations and macro scope handling
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#82 - fixed stage2 fix
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#81 - fix: truly separate stage2/3 builds by copying all sources
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#80 - Syntax quotations
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#79 - Extended CI checks
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#78 - implement HasEval for MetaM
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#77 - stage 2 and 3 builds, second edition
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 1 comment
#76 - feat: stage 2 and 3 builds
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 5 comments
#75 - Github Actions & CCache
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 2 comments
#74 - feat: `import runtime`
Pull Request -
State: closed - Opened by Kha almost 5 years ago
#73 - LEAN_PATH as a mapping from package names to root dirs
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 5 comments
#72 - chore: use paths instead of indices for stdlib tests
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 2 comments
#71 - chore: use proper nested make calls by hard-coding make as the build system
Pull Request -
State: closed - Opened by Kha almost 5 years ago
- 4 comments
#70 - chore: remove cygwin support
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 2 comments
#69 - fix: Windows build
Pull Request -
State: closed - Opened by Kha about 5 years ago
#68 - Improve bootstrapping process
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 2 comments
#67 - `panic`ing in the interpreter
Issue -
State: open - Opened by leodemoura about 5 years ago
- 12 comments
Labels: enhancement
#66 - Improve error handling
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 3 comments
#65 - feat: solves mvars in reverse order during tabled tc
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#64 - feat: solve typeclass subgoals in reverse order
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#63 - feat: allow metas in intermediate tc answers
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#62 - feat: allow metas in intermediate tc answers
Pull Request -
State: closed - Opened by dselsam about 5 years ago
#61 - doc(elabissues): typeclass loop issue and suggestions
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 2 comments
#60 - fix: (throwaway) context was ignoring const levels
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#59 - Plugin Support
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 5 comments
#58 - chore: update-stage0: stage all files
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 1 comment
#57 - doc(elabissues): namespace A.B vs namespace A namespace B
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#56 - doc(elabissues): tc triggers nested tc, potentially with tmp-mvar leak
Pull Request -
State: closed - Opened by dselsam about 5 years ago
- 1 comment
#55 - Revert debug commits
Pull Request -
State: closed - Opened by Kha about 5 years ago
- 1 comment