All pull requests

Pull requests

• feat: keep haves in equation lemmas that do not split a match

  changelog-languagedownstreamtoolchain-available
  #16208·leodemoura opened Nov 3, 2026Member·

  ·
  1

• perf: constant fold signed fixed-width integer literals

  toolchain-available
  #16196·vincentqb opened Nov 2, 2026Contributor·

  ·

• fix: default to 8MB thread stacks on all 32-bit targets

  toolchain-available
  #16195·vincentqb opened Nov 2, 2026Contributor·

  ·

• fix: share join points in vcgen +jp [f]

  changelog-tacticstoolchain-available
  #16194·sgraf812 opened Nov 2, 2026Contributor·

  ·
  2

• fix: read the assigned type of a binder domain in vcgen

  toolchain-available
  #16192·sgraf812 opened Nov 2, 2026Contributor·

  ·

• chore: run more of the test suite on the Web Assembly job

  changelog-notoolchain-available
  #16191·basvandijk opened Nov 2, 2026Contributor·

  ·
  2

• fix: check compactor buffer allocation failures

  changelog-notoolchain-available
  #16190·Timeroot opened Nov 2, 2026Contributor·

  ·
  1

• feat: error when privateInPublic exports a reference to an unexported declaration

  changelog-languagetoolchain-available
  #16183·nomeata opened Nov 2, 2026Collaborator·

  ·

• feat: use SHA-256 for Lake content hashes

  changelog-lakedownstreamtoolchain-available
  #16182·Kha opened Nov 2, 2026Member·

  ·
  3

• perf: instantiate only the head in Sym.instantiateMVarsIfMVarAppS

  toolchain-available
  #16181·sgraf812 opened Nov 2, 2026Contributor·

  ·

• fix: decode Win32 errors in the runtime's Windows IO paths

  changelog-librarytoolchain-available
  #16180·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

• fix: check whether a recursor's major premise is a proof without inferring its type

  changelog-languagetoolchain-available
  #16177·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  4

• fix: assign the original goal when a tactic block in an exposed definition fails

  changelog-languagetoolchain-available
  #16176·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  1

• fix: abstract hypotheses used as proofs in exposed definitions

  changelog-languagetoolchain-available
  #16175·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  1

• fix: release Task.bind continuation when the bind task is dropped while its function runs

  changelog-compilertoolchain-available
  #16174·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  1

• fix: wait for more input when a read ends inside an HTTP method name

  changelog-librarytoolchain-available
  #16173·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  1

• fix: make IO.sleep finish while signals interrupt it

  changelog-compilertoolchain-available
  #16172·matthiasgoergens opened Nov 2, 2026Contributor·

  ·
  1

  1

• feat: improve semantic highlighting

  changelog-servertoolchain-available
  #16151·RIvance opened Nov 1, 2026·

  ·
  1

  1

• perf: resolve native symbols inside lean.wasm instead of exporting all of Lean

  changelog-notoolchain-available
  #16149·basvandijk opened Nov 1, 2026Contributor·

  ·
  3

• perf: hash all bits of large Nat literals in Expr

  toolchain-available
  #16146·JasonGross opened Nov 1, 2026·

  ·
  1

• chore: update the Web Assembly CI job to Emscripten 6.0.13

  changelog-notoolchain-available
  #16142·basvandijk opened Oct 31, 2026Contributor·

  ·
  2

• fix: add expected type hints to Sym rules modified by preprocessing

  toolchain-available
  #16140·kmehltretter82 opened Oct 31, 2026·

  ·
  1

• chore: re-enable the Web Assembly CI job

  toolchain-available
  #16135·basvandijk opened Oct 31, 2026Contributor·

  ·
  1

  1

• feat: add hash map merging with collision functions

  changelog-librarytoolchain-available
  #16128·kim-em opened Oct 31, 2026Collaborator·

  ·

• feat: add joint ordered tree map folds

  changelog-librarytoolchain-available
  #16127·kim-em opened Oct 31, 2026Collaborator·

  ·