Issues

Universe approximation creates a cyclic level metavariable assignment and stack overflow

leanprover/lean4#16125 · opened

on Oct 31, 2026

Lake reuses an externally replaced .olean despite a current trace, including with --rehash

leanprover/lean4#16123 · opened

on Oct 30, 2026

vcgen +jp: join points not shared after unfolding a definition; shared join hypotheses make discharge exponential

leanprover/lean4#16122 · opened

on Oct 30, 2026

`Std.Http`: a valid `UPDATEREDIRECTREF` request gets 400 when a read ends inside the method name

leanprover/lean4#16111 · opened

on Oct 30, 2026

1

module system: `by exact h` in an exposed definition leaves `h` in the exported body, and importers get a kernel error

leanprover/lean4#16110 · opened

on Oct 30, 2026

`Task.bind` leaks the inner task when the bind task is dropped while its function runs

leanprover/lean4#16109 · opened

on Oct 30, 2026

1

`decide` on bounded quantifiers reaches `maxRecDepth` sooner since #15371

leanprover/lean4#16108 · opened

on Oct 30, 2026

Server: the reference index stores the parent declaration name once per usage location

leanprover/lean4#16100 · opened

on Oct 29, 2026

Eight FFI definitions have the wrong number of parameters, so calls to them can trap on WebAssembly

leanprover/lean4#16089 · opened

on Oct 29, 2026

Kernel performance regression checking computed projection applications (4.32.1 → 4.33.1, persists on nightly)

leanprover/lean4#16088 · opened

on Oct 29, 2026

Lean reports a type error at a wrong source position

leanprover/lean4#16084 · opened

on Oct 29, 2026

import link cost is decided by module-local codegen state

leanprover/lean4#16082 · opened

on Oct 29, 2026

`Sym.Pattern.match?` fails when a universe variable first appear in a `max`

leanprover/lean4#16070 · opened

on Oct 28, 2026

`IO.FS.removeDir` on a non-empty directory aborts builds with assertions

leanprover/lean4#16062 · opened

on Oct 28, 2026

Std.Http: a host name that begins with an IPv4 address (`1.2.3.4-x.example`) is rejected

leanprover/lean4#16058 · opened

on Oct 28, 2026

Field projections may fail due to open namespaces in special circumstances

leanprover/lean4#16044 · opened

on Oct 27, 2026

Std.Time: `O`/`OOOO` (at UTC), `xxxxx` and `Z`-`ZZZ` (with seconds) cannot parse their own formatted output

leanprover/lean4#16043 · opened

on Oct 27, 2026

Std.Time: parsing with `k`, `K` or `y`+`G` (BC) returns the wrong hour or year

leanprover/lean4#16038 · opened

on Oct 27, 2026

Std.Http: `decideRedirect` resolves `Location: /` to the current request path instead of `/`

leanprover/lean4#16036 · opened

on Oct 27, 2026

Std.Http: a request with an overlong request-target gets 400 or 414 depending on where a read ends

leanprover/lean4#16035 · opened

on Oct 27, 2026

Std.Http: query values containing `=` are rejected (`?a=b=c`, base64 padding)

leanprover/lean4#16021 · opened

on Oct 27, 2026

2

RFC: fault injection for error paths of the runtime in the test suite

leanprover/lean4#16020 · opened

on Oct 27, 2026

JSON round trip loses the sign of negative zero: `Json.parse` and `JsonNumber.fromFloat?` turn `-0.0` into `0`

leanprover/lean4#16016 · opened

on Oct 27, 2026

`IO.FS.Handle.mk` and `IO.FS.createTempFile` mishandle a failing `fdopen`

leanprover/lean4#16009 · opened

on Oct 27, 2026

`Json.parse` takes time quadratic in the number of digits of a number

leanprover/lean4#16008 · opened

on Oct 27, 2026

Navigation Menu

Repository navigation

Issues

Universe approximation creates a cyclic level metavariable assignment and stack overflow

Lake reuses an externally replaced .olean despite a current trace, including with --rehash

vcgen +jp: join points not shared after unfolding a definition; shared join hypotheses make discharge exponential

`Std.Http`: a valid `UPDATEREDIRECTREF` request gets 400 when a read ends inside the method name

module system: `by exact h` in an exposed definition leaves `h` in the exported body, and importers get a kernel error

`Task.bind` leaks the inner task when the bind task is dropped while its function runs

`decide` on bounded quantifiers reaches `maxRecDepth` sooner since #15371

Server: the reference index stores the parent declaration name once per usage location

Eight FFI definitions have the wrong number of parameters, so calls to them can trap on WebAssembly

Kernel performance regression checking computed projection applications (4.32.1 → 4.33.1, persists on nightly)

Lean reports a type error at a wrong source position

import link cost is decided by module-local codegen state

`Sym.Pattern.match?` fails when a universe variable first appear in a `max`

`IO.FS.removeDir` on a non-empty directory aborts builds with assertions

Std.Http: a host name that begins with an IPv4 address (`1.2.3.4-x.example`) is rejected

Field projections may fail due to open namespaces in special circumstances

Std.Time: `O`/`OOOO` (at UTC), `xxxxx` and `Z`-`ZZZ` (with seconds) cannot parse their own formatted output

Std.Time: parsing with `k`, `K` or `y`+`G` (BC) returns the wrong hour or year

Std.Http: `decideRedirect` resolves `Location: /` to the current request path instead of `/`

Std.Http: a request with an overlong request-target gets 400 or 414 depending on where a read ends

Std.Http: query values containing `=` are rejected (`?a=b=c`, base64 padding)

RFC: fault injection for error paths of the runtime in the test suite

JSON round trip loses the sign of negative zero: `Json.parse` and `JsonNumber.fromFloat?` turn `-0.0` into `0`

`IO.FS.Handle.mk` and `IO.FS.createTempFile` mishandle a failing `fdopen`

`Json.parse` takes time quadratic in the number of digits of a number