Search results

Dead lean-manual:// cross-references in core docstrings 404 in the manual

bugSomething isn't workingSomething isn't working

Status: Open.

#14163 In leanprover/lean4;

· lydia-schiff opened on Jun 23, 2026

RFC: Configurable / default lake cache scopes

LakeLake related issueLake related issue

RFCRequest for commentsRequest for comments

Status: Open.

#14154 In leanprover/lean4;

· marcelolynch opened on Jun 22, 2026

RFC: lake cache get read chain from multiple services

LakeLake related issueLake related issue

RFCRequest for commentsRequest for comments

Status: Open.

#14152 In leanprover/lean4;

· marcelolynch opened on Jun 22, 2026

RFC: SHA-isolated lake cache get via configurable revision discovery

LakeLake related issueLake related issue

RFCRequest for commentsRequest for comments

RFC 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;

· marcelolynch opened on Jun 22, 2026

lean_alloc_ctor crashes under mimalloc for constructors larger than MI_SMALL_SIZE_MAX

bugSomething isn't workingSomething isn't working

Status: Open.

#14148 In leanprover/lean4;

· cpehle opened on Jun 22, 2026

Using inferInstanceAs with non-exposed definition generates publicly ill-typed declaration

bugSomething isn't workingSomething isn't working

Status: Open.

#14147 In leanprover/lean4;

· gasparattila opened on Jun 22, 2026

Incorrect transparency used to expose differences

bugSomething isn't workingSomething isn't working

Status: Open.

#14143 In leanprover/lean4;

· Rob23oba opened on Jun 22, 2026

Compilation on FreeBSD fails: error: 'free_sized' is missing exception specification 'throw()'

Status: Open.

#14136 In leanprover/lean4;

· yurivict opened on Jun 22, 2026

Inconsistent spelling for cancellation

bugSomething isn't workingSomething isn't working

Status: Open.

#14117 In leanprover/lean4;

· david-christiansen opened on Jun 19, 2026

Selectable.combine can hang and panic

bugSomething isn't workingSomething isn't working

Status: Open.

#14090 In leanprover/lean4;

· david-christiansen opened on Jun 17, 2026

noncomputable error on definitions without data

bugSomething isn't workingSomething isn't working

Status: Open.

#14084 In leanprover/lean4;

· plp127 opened on Jun 16, 2026

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 working

Status: Open.

#14075 In leanprover/lean4;

· yonatan-reicher opened on Jun 16, 2026