All pull requests

Pull requests

• [#16218] feat: keep haves above a split match in equation lemmas

  adaptationcache-available
  #222·downstream-lean4[bot] opened Nov 3, 2026Bot·

  ·
  1

• fix: record the Nat.extendedGcd_gcd rewrite in MathlibTest.LibraryRewrite (lean4#15160)

  cache-available
  #220·downstream-lean4[bot] opened Nov 3, 2026Bot·

  ·
  1

• fix: adapt mathlib4, reference-manual, lean4export and cslib to nightly-2026-11-03 (lean4#16147, lean4#16113, lean4#16203)

  cache-available
  #219·downstream-lean4[bot] opened Nov 3, 2026Bot·

  ·
  1

• [#16208] feat: keep haves in equation lemmas that do not split a match

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

  ·

• [#16182] feat: use SHA-256 for Lake content hashes

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

  ·
  5

• [spike] strict instance check

  #206·datokrat opened Oct 29, 2026·

  ·

• [#15935] experiment: better caching of isUnitLikeType

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

  ·
  9

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

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

  ·
  5

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

  ·