All pull requests

Pull requests

• feat: configure the step limit of the vcgen simp step

  toolchain-available
  #16346·sgraf812 opened Nov 8, 2026Member·

  ·

• perf: check declarations in the kernel in parallel

  downstreamtoolchain-available
  #16343·Kha opened Nov 8, 2026Member·

  ·
  3

• feat: make Std.WP.Assertion an opt-in class

  toolchain-available
  #16342·sgraf812 opened Nov 7, 2026Member·

  ·

• fix: language server hardening

  changelog-servertoolchain-available
  #16337·mhuisi opened Nov 7, 2026Contributor·

  ·
  1

• perf: make Except.bind and OptionT.bind abbreviations for lazy-delta reduction

  toolchain-available
  #16336·arthur-adjedj opened Nov 7, 2026Contributor·

  ·
  1

  2

• fix: correct URI parsing and redirect decisions

  changelog-librarytoolchain-available
  #16328·algebraic-dev opened Nov 6, 2026Member·

  ·
  

• perf: stop awaiting each socket write in the HTTP server

  changelog-librarytoolchain-available
  #16322·algebraic-dev opened Nov 6, 2026Member·

  ·
  

• fix: cbv discharges overlap hypotheses of match equations

  changelog-tacticstoolchain-available
  #16316·wkrozowski opened Nov 6, 2026Contributor·

  ·

• feat: use the documentation modifier for docstring semantic tokens

  changelog-servertoolchain-available
  #16314·david-christiansen opened Nov 6, 2026Contributor·

  ·

• perf: vcgen eliminates binders over unit types

  changelog-tacticstoolchain-available
  #16304·sgraf812 opened Nov 6, 2026Member·

  ·
  6

• fix: publish on-demand Lake cache downloads atomically

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

  ·

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

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

  ·
  1

• 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·

  ·
  6

• 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·

  ·