All pull requests

Pull requests

• test hacky project-specific fix for verso failure

  cache-available
  #154·robsimmons opened Oct 9, 2026Contributor·

  ·
  1

• fix verso HTML issues in 10-08 nightly

  cache-available
  #153·robsimmons opened Oct 9, 2026Contributor·

  ·
  3

• [#15557] perf: bytecode interpreter

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

  ·
  9

• [#15581] feat: proper UTF-8 string comparison

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

  ·
  1

• [#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

• fix: mathlib4 breakage from the import-graph main merge

  cache-available
  #149·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

• fix: verso breakage from the verso main merge (supersedes #142)

  cache-available
  #145·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

• [#14327] perf: memoize stuck type class resolution queries

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

  ·
  3

• [#15444] perf: faster interpreter

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

  ·
  3

• [#15438] feat: allow reporting positions above #guard_msgs

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

  ·
  1

• [#14421] feat: look for .ilean.mmap files on watchdog load

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

  ·
  1

• [#15373] feat: eta-expand partial constructors

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

  ·
  1

• [#15374] feat: eta-expand partial recursor apps for structures/K-like types

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

  ·
  1

• [#15372] feat: extend unit-like criteria for eta

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

  ·
  1

• [#15371] feat: eta-expand recursor major for subsingleton structures

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

  ·
  1

• [#15351] fix: eta-expand recursor majors before running whnf

  adaptationcache-availabletoolchain-available
  #110·downstream-lean4[bot] opened Sep 27, 2026Bot·

  ·
  3

• [#15339] chore: don't use max precedence for term following private_decl%

  adaptationcache-availabletoolchain-available
  #109·downstream-lean4[bot] opened Sep 26, 2026Bot·

  ·
  1

• subverso maybe?

  cache-available
  #102·Garmelon opened Sep 22, 2026Collaborator·

  ·
  1