All pull requests

Pull requests

• fix: verso breakage from lean4#15845

  #213·downstream-lean4[bot] opened Oct 30, 2026Bot·

  ·

• [#16099] fix: remove redundant instances for arrows

  adaptationcache-availabletoolchain-available
  #211·downstream-lean4[bot] opened Oct 29, 2026Bot·

  ·
  1

• [spike] strict instance check

  #206·datokrat opened Oct 29, 2026·

  ·

• [#13674] feat: more semantic tokens for Markdown/Verso

  adaptationcache-availabletoolchain-available
  #203·downstream-lean4[bot] opened Oct 28, 2026Bot·

  ·

• [#15935] experiment: better caching of isUnitLikeType

  adaptationcache-availabletoolchain-available
  #197·downstream-lean4[bot] opened Oct 25, 2026Bot·

  ·
  5

• [#15923] perf: import simp sets and instances from per-module olean data

  adaptationcache-availabletoolchain-available
  #196·downstream-lean4[bot] opened Oct 24, 2026Bot·

  ·
  5

• [#15903] perf: invalidate type class resolution results only on instance changes of consulted classes

  adaptationcache-availabletoolchain-available
  #194·downstream-lean4[bot] opened Oct 23, 2026Bot·

  ·
  3

• [#15889] perf: share type class resolution results across local contexts and instance changes

  adaptationcache-availabletoolchain-available
  #193·downstream-lean4[bot] opened Oct 23, 2026Bot·

  ·
  3

• [#15844] fix: lake: await export metadata through job dependencies

  adaptationcache-availabletoolchain-available
  #188·downstream-lean4[bot] opened Oct 21, 2026Bot·

  ·
  3

• [#15845] perf: avoid rebuilding the FileMap of parser inputs

  adaptationcache-availabletoolchain-available
  #187·downstream-lean4[bot] opened Oct 21, 2026Bot·

  ·
  3

• [#15550] feat: add #html display command

  adaptationcache-availabletoolchain-available
  #184·downstream-lean4[bot] opened Oct 19, 2026Bot·

  ·
  1

• [#15528] perf: flatten IR data structure

  adaptationcache-availabletoolchain-available
  #178·downstream-lean4[bot] opened Oct 17, 2026Bot·

  ·
  3

• [#15724] temp: claudified import profiling for testing

  adaptationcache-availabletoolchain-available
  #173·downstream-lean4[bot] opened Oct 16, 2026Bot·

  ·
  1

• [#15023] feat: make Quot live in Sort (max 1 u) rather than Sort u

  adaptationcache-availabletoolchain-available
  #171·downstream-lean4[bot] opened Oct 15, 2026Bot·

  ·
  1

• [#13851] feat: no large elim of recursive Prop inductives in the kernel

  adaptationcache-available
  #163·downstream-lean4[bot] opened Oct 13, 2026Bot·

  ·
  1

• [#15650] perf: retry stuck instance problems only when a blocker is assigned

  adaptationcache-availabletoolchain-available
  #160·downstream-lean4[bot] opened Oct 13, 2026Bot·

  ·
  1

• [#15557] perf: bytecode interpreter

  adaptationcache-availabletoolchain-available
  #152·downstream-lean4[bot] opened Oct 9, 2026Bot·

  ·
  9

• [#15578] perf: do not export data that depends on how a theorem is proved

  adaptationcache-availabletoolchain-available
  #150·downstream-lean4[bot] opened Oct 9, 2026Bot·

  ·
  1

• [#15556] feat: collect axioms of imported declarations on demand

  adaptationcache-availabletoolchain-available
  #146·downstream-lean4[bot] opened Oct 8, 2026Bot·

  ·
  1

• [#15540] feat: track visibility of section variables

  adaptationcache-availabletoolchain-available
  #144·downstream-lean4[bot] opened Oct 7, 2026Bot·

  ·
  1

• ci: use a matrix for post-build export jobs

  #143·jessealama opened Oct 7, 2026Contributor·

  ·

• ci: add Dependabot for GitHub Actions

  #141·jessealama opened Oct 6, 2026Contributor·

  ·

• ci: lint workflow files with actionlint

  #138·jessealama opened Oct 6, 2026Contributor·

  ·

• ci: report builds that crash before producing a report

  #136·jessealama opened Oct 6, 2026Contributor·

  ·

• Register HexBasic and HexPermGroup for toolchain adaptation

  cache-available
  #135·kim-em opened Oct 6, 2026·

  ·
  1