Code

feat: asynchronous kernel checking#6368

Code

Draft

Kha wants to merge 42 commits intoleanprover:kernel-env-baseleanprover/lean4:kernel-env-basefrom Kha:async-tcKha/lean4:async-tcCopy head branch name to clipboard

+195,734-98,647

Commits

Commits on Jan 8, 2025

• fix: set LLVM sysroot consistently (leanprover#6574)

  Show description for 680ede7
  Kha

  authored
  680ede7

  Copy full SHA for 680ede7

• feat: make classical tactic incremental (leanprover#6575)

  Show description for 034bc26
  Kha

  authored
  034bc26

  Copy full SHA for 034bc26

• fix: forall propagation in grind (leanprover#6578)

  Show description for 5be241c
  

  leodemoura

  and

  kim-em

  authored
  5be241c

  Copy full SHA for 5be241c

• feat: add grind configuration options to control case-splitting (leanprover#6581)

  Show description for ddd454c
  leodemoura

  authored
  ddd454c

  Copy full SHA for ddd454c

• feat: apply E-matching for local lemmas in grind (leanprover#6582)

  Show description for 0afa1d1
  leodemoura

  authored
  0afa1d1

  Copy full SHA for 0afa1d1

Commits on Jan 9, 2025

• feat: add helper theorems for handling offsets in grind (leanprover#6584)

  Show description for c5314da
  leodemoura

  authored
  c5314da

  Copy full SHA for c5314da

• fix: grind canonicalizer (leanprover#6585)

  Show description for cb9f198
  leodemoura

  authored
  cb9f198

  Copy full SHA for cb9f198

• feat: aligning List/Array/Vector lemmas for map (leanprover#6586)

  Show description for 623dec1
  kim-em

  authored
  623dec1

  Copy full SHA for 623dec1

• feat: align List/Array lemmas for filter/filterMap (leanprover#6589)

  Show description for 827c667
  kim-em

  authored
  827c667

  Copy full SHA for 827c667

• feat: improve grind canonicalizer diagnostics (leanprover#6588)

  Show description for dd64455
  

  leodemoura

  and

  kim-em

  authored
  dd64455

  Copy full SHA for dd64455

• feat: add UInt32.{lt, le} (leanprover#6591)

  Show description for 1b42728
  david-christiansen

  authored
  1b42728

  Copy full SHA for 1b42728

• feat: Std.Net.Addr (leanprover#6563)

  Show description for a6789a7
  hargoniX

  authored
  a6789a7

  Copy full SHA for a6789a7

• feat: improve inequality offset support theorems for grind (leanprover#6595)

  Show description for d369976
  leodemoura

  authored
  d369976

  Copy full SHA for d369976

Commits on Jan 10, 2025

• feat: add simp? and dsimp? in conversion mode (leanprover#6593)

  Show description for c07948a
  jrr6

  authored
  c07948a

  Copy full SHA for c07948a

• feat: BitVec.{toInt, toFin, msb}_udiv (leanprover#6402)

  Show description for d2c4471
  

  alexkeizer

  and

  kim-em

  authored
  d2c4471

  Copy full SHA for d2c4471

• feat: add decidable instances for comparison operation of time offset types (leanprover#6587)

  Show description for ed309dc
  algebraic-dev

  authored
  ed309dc

  Copy full SHA for ed309dc

• feat: BitVec.toNat theorems for rotateLeft and rotateRight (leanprover#6347)

  Show description for 0b5d977
  

  mhk119

  and

  kim-em

  authored
  0b5d977

  Copy full SHA for 0b5d977

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  58cd011

  Copy full SHA for 58cd011

• feat: BitVec.{toFin, toInt, msb}_umod (leanprover#6404)

  Show description for 918924c
  

  alexkeizer

  and

  kim-em

  authored
  918924c

  Copy full SHA for 918924c

Commits on Jan 11, 2025

• doc: update FFI description for Int and signed fixed-width ints (leanprover#6599)

  Show description for 03081a5
  david-christiansen

  authored
  03081a5

  Copy full SHA for 03081a5

• chore: add lean4-cli to release checklist (leanprover#6596)

  Show description for 8791a9c
  

  kim-em

  and

  TwoFX

  authored
  8791a9c

  Copy full SHA for 8791a9c

Commits on Jan 12, 2025

• fix: pattern selection for local lemmas (leanprover#6606)

  Show description for acad587
  leodemoura

  authored
  acad587

  Copy full SHA for acad587

• feat: add support for splitting on <-> to grind (leanprover#6607)

  Show description for 7ea5504
  leodemoura

  authored
  7ea5504

  Copy full SHA for 7ea5504

• fix: simp_arith (leanprover#6608)

  Show description for 4636091
  leodemoura

  authored
  4636091

  Copy full SHA for 4636091

• feat: improve case-split heuristic used in grind (leanprover#6609)

  Show description for 5119528
  leodemoura

  authored
  5119528

  Copy full SHA for 5119528

• fix: bug in the grind propagator (leanprover#6610)

  Show description for c5c1278
  leodemoura

  authored
  c5c1278

  Copy full SHA for c5c1278

• fix: checkParents in grind (leanprover#6611)

  Show description for ce1ff03
  leodemoura

  authored
  ce1ff03

  Copy full SHA for ce1ff03

• feat: lemmas about Array.append (leanprover#6612)

  Show description for 8b1aabb
  kim-em

  authored
  8b1aabb

  Copy full SHA for 8b1aabb

• feat: improve case split heuristic used in grind (leanprover#6613)

  Show description for 5419025
  leodemoura

  authored
  5419025

  Copy full SHA for 5419025

• feat: improve [grind =] attribute (leanprover#6614)

  Show description for 349da6c
  leodemoura

  authored
  349da6c

  Copy full SHA for 349da6c

• fix: allow dot idents to resolve to local names (leanprover#6602)

  Show description for 0da3624
  cppio

  authored
  0da3624

  Copy full SHA for 0da3624

• feat: offset constraints support for the grind tactic (leanprover#6603)

  Show description for c7939cf
  

  leodemoura

  and

  kim-em

  authored
  c7939cf

  Copy full SHA for c7939cf

• feat: split Lean.Kernel.Environment from Lean.Environment

  Kha

  committed
  7818f9b

  Copy full SHA for 7818f9b

• chore: update stage0

  Kha

  committed
  136e93a

  Copy full SHA for 136e93a

• chore: clean up after update-stage0

  Kha

  committed
  a46ba58

  Copy full SHA for a46ba58

• refactor: move registration of namespaces on kernel add into elaborator

  Kha

  committed
  ffee8e5

  Copy full SHA for ffee8e5

Commits on Jan 13, 2025

• feat: Environment.addConstAsync

  Kha

  committed
  6e86d0a

  Copy full SHA for 6e86d0a

• fix: do not double-report snapshotTasks after wrapAsyncAsSnapshot

  Kha

  committed
  1f723b5

  Copy full SHA for 1f723b5

• feat: asynchronous kernel checking

  Kha

  committed
  e91ab17

  Copy full SHA for e91ab17

• also disable async TC in bv_decide et al

  Kha

  committed
  977fe8b

  Copy full SHA for 977fe8b

• fix compilation skip on kernel error

  Kha

  committed
  9588514

  Copy full SHA for 9588514

• disable Lake benchmarks

  Kha

  committed
  57d45ce

  Copy full SHA for 57d45ce