All pull requests

Pull requests

• chore: dot-notation-respects-open convention for internal error utilities

  changelog-notoolchain-available
  #15719·robsimmons opened Oct 15, 2026Contributor·

  ·

• fix: parameterize ST.RefPointed to prevent unsafe cast

  changelog-notoolchain-available
  #15718·Rob23oba opened Oct 15, 2026Contributor·

  ·
  1

• feat: encode a % k as a in lia when 0 ≤ a < k

  toolchain-available
  #15716·sgraf812 opened Oct 15, 2026Contributor·

  ·

• perf: lake: resolve a module's transitive import closure from one store snapshot

  toolchain-available
  #15714·zeldovich opened Oct 15, 2026·

  ·

• perf: lake: read the build store without taking its ref

  toolchain-available
  #15712·zeldovich opened Oct 15, 2026·

  ·
  2

• fix: prevent order-dependent cache pollution in kernel is_def_eq

  awaiting-reviewchangelog-othertoolchain-available
  #15709·gersh opened Oct 15, 2026·

  ·
  1

  1

• fix: fully typecheck recursor computation rules in check_recursors

  awaiting-reviewchangelog-othertoolchain-available
  #15708·gersh opened Oct 15, 2026·

  ·
  1

  1

• fix: verify type annotations and parameter domains in inductive checking

  awaiting-reviewchangelog-othertoolchain-available
  #15707·gersh opened Oct 15, 2026·

  ·
  1

  1

• perf: alternatives to #15351

  downstreamtoolchain-available
  #15698·arthur-adjedj opened Oct 15, 2026Contributor·

  ·
  9

• fix: lake: fetch plugin and link facets on the fetching thread

  toolchain-available
  #15696·rbeauchamp opened Oct 14, 2026Contributor·

  ·
  1

• perf: make column computations on long lines independent of the line length

  toolchain-available
  #15695·Kha opened Oct 14, 2026Member·

  ·
  1

  4

• perf: shard the interpreter's native symbol cache lock

  toolchain-available
  #15693·marcelolynch opened Oct 14, 2026Contributor·

  ·
  2

• fix: Sym.simp reduces match on literal discriminants

  toolchain-available
  #15690·sgraf812 opened Oct 14, 2026Contributor·

  ·

• fix: make unfold on non-recursive definitions independent of eq_def realization

  downstreamtoolchain-available
  #15687·Kha opened Oct 14, 2026Member·

  ·
  1

• fix: elaborate the do continuation only once when contracting pure ()

  changelog-languagedownstreamtoolchain-available
  #15682·sgraf812 opened Oct 14, 2026Contributor·

  ·
  1

  1

• refactor: implement reference-counting deletion's cascade in Lean

  toolchain-available
  #15676·vincentqb opened Oct 14, 2026Contributor·

  ·

• perf: avoid the task-manager mutex when destroying pure tasks

  toolchain-available
  #15673·marcelolynch opened Oct 14, 2026Contributor·

  ·
  2

• fix: fail libuv calls after the event loop is torn down

  changelog-libraryrelease-citoolchain-available
  #15671·algebraic-dev opened Oct 14, 2026Member·10/10·

  ·

• perf: reduce lock contention when unfolding imported constants

  toolchain-available
  #15670·marcelolynch opened Oct 13, 2026Contributor·

  ·
  4

• feat: cancel queued libuv threadpool requests at exit

  changelog-librarytoolchain-available
  #15669·algebraic-dev opened Oct 13, 2026Member·9/10·

  ·
  

• feat: teardown libuv

  changelog-librarytoolchain-available
  #15668·algebraic-dev opened Oct 13, 2026Member·8/10·

  ·

• fix: stop a repeating signal that nothing waits on

  changelog-librarytoolchain-available
  #15667·algebraic-dev opened Oct 13, 2026Member·7/10·

  ·
  

• perf: defer global queries during local name resolution

  downstreamtoolchain-available
  #15666·ejgallego opened Oct 13, 2026Contributor·

  ·
  3

• feat: bundle lean-beam with release toolchains

  release-citoolchain-available
  #15665·ejgallego opened Oct 13, 2026Contributor·

  ·
  6

• feat: verify all and any for tree maps

  toolchain-available
  #15664·saviorand opened Oct 13, 2026·

  ·
  1