Search results

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

section variables are ignored during type-checking of recursive function

bugSomething isn't workingSomething isn't working

Status: Open.

#14061 In leanprover/lean4;

· tribbloid opened on Jun 15, 2026

RFC: MePo premise selection — candidate-side symbol sets should match the goal side (instance/proof asymmetry)

RFCRequest for commentsRequest for comments

Status: Open.

#14057 In leanprover/lean4;

· xgenereux opened on Jun 15, 2026

Panic when using intro followed by pattern in conv mode

bugSomething isn't workingSomething isn't working

Status: Open.

#14055 In leanprover/lean4;

· hylophile opened on Jun 15, 2026

feat: fast fixed-width integer load/store on ByteArray (native UInt16/UInt32/UInt64 accessors)

featuremissing featuremissing feature

Status: Open.

#14050 In leanprover/lean4;

· kim-em opened on Jun 15, 2026

solve_by_elim failure

bugSomething isn't workingSomething isn't working

Status: Open.

#14014 In leanprover/lean4;

· BrunoDutertre opened on Jun 11, 2026

lake: specify conflict semantics for require X with <opts> when X is required twice

LakeLake related issueLake related issue

questionFurther information is requestedFurther information is requested

Status: Open.

#14005 In leanprover/lean4;

· kim-em opened on Jun 11, 2026

lake: dump link-args response file on link failure

Status: Open.

#14004 In leanprover/lean4;

· kim-em opened on Jun 11, 2026

IO.Process.run throws an error on non-UTF8 stdout or stderr.

bugSomething isn't workingSomething isn't working

Status: Open.

#14003 In leanprover/lean4;

· mzinkevi opened on Jun 11, 2026

IO.Process.output can throw an error while the underlying spawned process is still running

bugSomething isn't workingSomething isn't working

Status: Open.

#14001 In leanprover/lean4;

· mzinkevi opened on Jun 11, 2026