Code

feat: asynchronous kernel checking#6368

Code

Draft

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

+136,348-117,523

Commits

Commits on Jan 15, 2025

• feat: verify insertMany method for adding lists to HashMaps (leanprover#6211)

  Show description for 6665837
  

  monsterkrampe

  and

  jt0202

  authored
  6665837

  Copy full SHA for 6665837

• fix: improve E-matching pattern selection heuristics (leanprover#6653)

  Show description for b3f8fef
  leodemoura

  authored
  b3f8fef

  Copy full SHA for b3f8fef

• feat: better support for partial applications in the E-matching procedure (leanprover#6654)

  Show description for 54f06cc
  leodemoura

  authored
  54f06cc

  Copy full SHA for 54f06cc

• feat: improvegrind diagnostic information (leanprover#6656)

  Show description for 65175dc
  leodemoura

  authored
  65175dc

  Copy full SHA for 65175dc

• feat: more grind tests (leanprover#6650)

  Show description for 127b3f9
  kim-em

  authored
  127b3f9

  Copy full SHA for 127b3f9

• feat: improve grind search procedure (leanprover#6657)

  Show description for 64cf5e5
  leodemoura

  authored
  64cf5e5

  Copy full SHA for 64cf5e5

• refactor: lake: use StateRefT for BuildStore (leanprover#6290)

  Show description for 0050e93
  tydeu

  authored
  0050e93

  Copy full SHA for 0050e93

Commits on Jan 16, 2025

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

  Show description for 6259b47
  leodemoura

  authored
  6259b47

  Copy full SHA for 6259b47

• fix: grind term preprocessor (leanprover#6659)

  Show description for af4a7d7
  

  leodemoura

  and

  kim-em

  authored
  af4a7d7

  Copy full SHA for af4a7d7

• feat: canonicalizer diagnostics (leanprover#6662)

  Show description for 3a6c5cf
  leodemoura

  authored
  3a6c5cf

  Copy full SHA for 3a6c5cf

• feat: align List/Array/Vector.flatMap (leanprover#6660)

  Show description for 80ddbf4
  kim-em

  authored
  80ddbf4

  Copy full SHA for 80ddbf4

• feat: Vector.getElem_flatMap (leanprover#6661)

  Show description for f4c9934
  kim-em

  authored
  f4c9934

  Copy full SHA for f4c9934

• feat: align List.replicate/Array.mkArray/Vector.mkVector lemmas (leanprover#6667)

  Show description for f015271
  kim-em

  authored
  f015271

  Copy full SHA for f015271

• feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib, shiftLeft_and_distrib, testBit_mul_two_pow, bitwise_mul_two_pow, shiftLeft_bitwise_distrib] (leanprover#6630)

  Show description for 906aa1b
  

  luisacicolini

  and

  alexkeizer

  authored
  906aa1b

  Copy full SHA for 906aa1b

• feat: equality resolution for grind (leanprover#6663)

  Show description for e42f7d9
  leodemoura

  authored
  e42f7d9

  Copy full SHA for e42f7d9

• fix: add workaround for MessageData limitations (leanprover#6669)

  Show description for 17c0187
  leodemoura

  authored
  17c0187

  Copy full SHA for 17c0187

• chore: remove unneeded instance (leanprover#6671)

  Show description for 60142c9
  hargoniX

  authored
  60142c9

  Copy full SHA for 60142c9

Commits on Jan 17, 2025

• feat: add simp-like parameters to grind (leanprover#6675)

  Show description for 35a4da2
  leodemoura

  authored
  35a4da2

  Copy full SHA for 35a4da2

• fix: don't filter out local instances in LCNF toMono pass (leanprover#6664)

  Show description for 7f0ae22
  zwarich

  authored
  7f0ae22

  Copy full SHA for 7f0ae22

• feat: add lcAny constant to Prelude (leanprover#6665)

  Show description for b7815b5
  zwarich

  authored
  b7815b5

  Copy full SHA for b7815b5

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  e3fd954

  Copy full SHA for e3fd954

• refactor: move ext environment extension to Lean.Meta.Tactic

  leodemoura

  committed
  f374ef1

  Copy full SHA for f374ef1

• chore: update stage0

  Show description for 9b629cc
  leodemoura

  committed
  9b629cc

  Copy full SHA for 9b629cc

• feat: extensionality theorems in grind (leanprover#6682)

  Show description for 4d4c094
  leodemoura

  authored
  4d4c094

  Copy full SHA for 4d4c094

Commits on Jan 18, 2025

• fix: grind parameter issues and configuration (leanprover#6686)

  Show description for d4070d4
  leodemoura

  authored
  d4070d4

  Copy full SHA for d4070d4

• fix: make #check_failure's output be info (leanprover#6685)

  Show description for 98e3d6f
  Seasawher

  authored
  98e3d6f

  Copy full SHA for 98e3d6f

• chore: fix typo in docstring of mkMVar (leanprover#6687)

  Show description for 5e63dd2
  goens

  authored
  5e63dd2

  Copy full SHA for 5e63dd2

• feat: split Lean.Kernel.Environment from Lean.Environment (leanprover#5145)

  Show description for 3770808
  Kha

  authored
  3770808

  Copy full SHA for 3770808

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  5fb2e89

  Copy full SHA for 5fb2e89

• refactor: move registration of namespaces on kernel add into elaborator (leanprover#6214)

  Show description for 50a0a97
  Kha

  authored
  50a0a97

  Copy full SHA for 50a0a97

• chore: init_grind_norm command parser (leanprover#6689)

  leodemoura

  authored
  70050c3

  Copy full SHA for 70050c3

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  2694179

  Copy full SHA for 2694179

• refactor: getUnfoldableConst*? (leanprover#5997)

  Show description for 8a8417f
  Kha

  authored
  8a8417f

  Copy full SHA for 8a8417f

• feat: regression tests for grind adapted from lean-egg (leanprover#6688)

  Show description for 5998ba5
  kim-em

  authored
  5998ba5

  Copy full SHA for 5998ba5

Commits on Jan 19, 2025

• feat: init_grind_norm elaborator (leanprover#6690)

  Show description for 478d421
  leodemoura

  authored
  478d421

  Copy full SHA for 478d421

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  7ee9382

  Copy full SHA for 7ee9382

• feat: Environment.addConstAsync

  Kha

  committed
  eca38b0

  Copy full SHA for eca38b0

• fix: do not double-report snapshotTasks after wrapAsyncAsSnapshot

  Kha

  committed
  cc8c5eb

  Copy full SHA for cc8c5eb

• feat: asynchronous kernel checking

  Kha

  committed
  d519e08

  Copy full SHA for d519e08

• perf: optimize setImportedEntries

  Kha

  committed
  2524cce

  Copy full SHA for 2524cce