All pull requests

Pull requests

• feat: lake: package-specified cache services

  changelog-lake
  #16302·tydeu opened Nov 6, 2026Member·

  ·

• fix: make local artifact sharing safe across workspaces

  changelog-laketoolchain-available
  #16301·kim-em opened Nov 6, 2026Collaborator·

  ·

• feat: vcgen destructures binders by @[vcgen_rintro] rules

  toolchain-available
  #16291·sgraf812 opened Nov 5, 2026Member·

  ·
  2

• perf: share type class resolution results with output parameters across local contexts

  downstreamtoolchain-available
  #16288·Kha opened Nov 5, 2026Member·2/2·

  ·
  1

• fix: correct HTTP/1.1 parsing, framing and connection handling

  changelog-librarytoolchain-available
  #16282·algebraic-dev opened Nov 5, 2026Member·

  ·

• fix: rethrow kernel resource-limit errors in decide +kernel

  toolchain-available
  #16277·BorisTheBrave opened Nov 5, 2026·

  ·
  1

  1

• chore: use fast overflow circuit by default

  toolchain-available
  #16274·luisacicolini opened Nov 5, 2026Contributor·

  ·
  2

• feat: introduce a supremum or a guard under the frame operator in vcgen preconditions

  changelog-tacticstoolchain-available
  #16254·sgraf812 opened Nov 4, 2026Member·

  ·

• fix: let grind case-split on a check guard of the form ¬p

  changelog-tacticstoolchain-available
  #16250·sgraf812 opened Nov 4, 2026Member·

  ·

• fix: give List.take_add the guarded grind pattern (l.drop i).take j

  changelog-librarytoolchain-available
  #16245·sgraf812 opened Nov 4, 2026Member·

  ·
  1

  2

• fix: respect debug.skipKernelTC when replaying realized constants

  changelog-languagetoolchain-available
  #16243·kim-em opened Nov 4, 2026Collaborator·

  ·
  1

• feat: implement big number arithmetic in Lean and drop GMP

  downstreamtoolchain-available
  #16240·Kha opened Nov 3, 2026Member·

  ·
  5

• fix: include non-optional version in VersionedTextDocumentIdentifier json

  changelog-serverdownstreamtoolchain-available
  #16237·thorimur opened Nov 3, 2026Contributor·

  ·
  1

  5

• perf: faster isProof major in reduceRec

  downstreamtoolchain-available
  #16232·arthur-adjedj opened Nov 3, 2026Contributor·

  ·
  4

• chore: bump olean header version and merge olean formats

  changelog-notoolchain-available
  #16214·nomeata opened Nov 3, 2026Collaborator·

  ·

• perf: constant fold signed fixed-width integer literals

  code-generatortoolchain-available
  #16196·vincentqb 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

• 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

• 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