-
Notifications
You must be signed in to change notification settings - Fork 883
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Dead lean-manual:// cross-references in core docstrings 404 in the manual
bugSomething isn't workingSomething isn't workingStatus: Open.#14163 In leanprover/lean4;RFC: Configurable / default
lake cachescopesLakeLake related issueLake related issueP-highWe will work on this issueWe will work on this issueRFCRequest for commentsRequest for commentsStatus: Open.#14154 In leanprover/lean4;RFC:
lake cache getread chain from multiple servicesLakeLake related issueLake related issueP-highWe will work on this issueWe will work on this issueRFCRequest for commentsRequest for commentsStatus: Open.#14152 In leanprover/lean4;RFC: SHA-isolated
lake cache getvia configurable revision discoveryLakeLake related issueLake related issueP-highWe will work on this issueWe will work on this issueRFCRequest for commentsRequest for commentsRFC acceptedRFC is waiting for a corresponding PR (external or internal)RFC is waiting for a corresponding PR (external or internal)Status: Open.#14151 In leanprover/lean4;lean_alloc_ctorcrashes under mimalloc for constructors larger thanMI_SMALL_SIZE_MAXbugSomething isn't workingSomething isn't workingStatus: Open.#14148 In leanprover/lean4;Using
inferInstanceAswith non-exposed definition generates publicly ill-typed declarationbugSomething isn't workingSomething isn't workingP-highWe will work on this issueWe will work on this issueStatus: Open.#14147 In leanprover/lean4;Incorrect transparency used to expose differences
bugSomething isn't workingSomething isn't workingP-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeStatus: Open.#14143 In leanprover/lean4;Compilation on FreeBSD fails: error: 'free_sized' is missing exception specification 'throw()'
P-lowWe are not planning to work on this issueWe are not planning to work on this issueStatus: Open.#14136 In leanprover/lean4;Inconsistent spelling for cancellation
bugSomething isn't workingSomething isn't workingStatus: Open.#14117 In leanprover/lean4;noncomputableerror on definitions without databugSomething isn't workingSomething isn't workingP-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeStatus: Open.#14084 In leanprover/lean4;Bad error message "unknown parser declaration/category/alias
..." when using a non-public syntax declaration from a public one.bugSomething isn't workingSomething isn't workingP-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeStatus: Open.#14075 In leanprover/lean4;section variables are ignored during type-checking of recursive function
bugSomething isn't workingSomething isn't workingP-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the timeStatus: Open.#14061 In leanprover/lean4;