Commit graph

Select branches

Hide pull requests

master

Mono Color

• fda4793215
  test: copy ver_clash test data to temp dir before modifying (#13134) Sebastian Ullrich 2026-03-27 11:25:58 +01:00
• 215aa4010b chore: update stage0 Lean stage0 autoupdater 2026-03-27 11:03:27 +00:00
• 142ca24192
  feat: support #print axioms under the module system (#13117) Joachim Breitner 2026-03-27 11:15:49 +01:00
• c71a0ea9a5
  perf: coalescing of RC ops within one basic block (#13136) Henrik Böving 2026-03-27 11:13:04 +01:00
• 439c3c5544
  refactor: make exportEntriesFnEx return all olean levels at once (#13142) Joachim Breitner 2026-03-27 09:57:45 +01:00
• 2bc7a77806
  fix: lake: lake cache help put-staged (#13150) Mac Malone 2026-03-27 01:11:43 -04:00
• e55f69acd0
  refactor: simplify grind canonicalizer and fix preprocessing issues (#13149) Leonardo de Moura 2026-03-26 22:00:01 -07:00
• 50785098d8
  feat: lake: cache staging (#13144) Mac Malone 2026-03-26 23:16:09 -04:00
• fee2d7a6e8
  fix: potential Array.get!Internal leaks part 2 (#13148) Henrik Böving 2026-03-27 03:51:39 +01:00
• bc5210d52a chore: update stage0 Lean stage0 autoupdater 2026-03-27 01:15:51 +00:00
• 12c547122f chore: update stage0 Lean stage0 autoupdater 2026-03-27 01:04:33 +00:00
• f9c8b5e93d
  fix: potential Array.get!Internal leaks part 1 (#13147) Henrik Böving 2026-03-27 01:13:17 +01:00
• f8f12fdbc8
  fix: lake: run git clean -xf when updating packages (#13141) Mac Malone 2026-03-26 18:12:54 -04:00
• 7f424b371e chore: update stage0 Lean stage0 autoupdater 2026-03-26 22:47:08 +00:00
• d56424b587
  feat: weak_specialize annotations (#13138) Henrik Böving 2026-03-26 22:58:52 +01:00
• 144db355ea
  fix: rebootstrap cache in github CI (#13143) Henrik Böving 2026-03-26 21:50:03 +01:00
• 0975b7136a chore: update stage0 Lean stage0 autoupdater 2026-03-26 16:38:25 +00:00
• ccef9588ae
  feat: add further cbv annotations (#13135) Wojciech Różowski 2026-03-26 14:55:40 +00:00
• a8bbc95d9f
  chore: remove lean4checker from release repos (#13121) Garmelon 2026-03-26 13:15:37 +01:00
• a54eafb84f
  refactor: decouple solve from grind in sym-based mvcgen (#13133) Sebastian Graf 2026-03-26 12:19:08 +01:00
• 6f2745d88b
  feat: verification of backwards string patterns (#13129) Markus Himmel 2026-03-26 09:44:47 +01:00
• 25c71d91aa
  feat: add rfl lemmas about ExceptCpsT.runK (#12912) Eric Wieser 2026-03-26 01:13:20 -07:00
• db491ddd35
  refactor: move issue tracker from grind to SymM (#13125) Leonardo de Moura 2026-03-25 19:27:27 -07:00
• e8c3485e08
  fix: cbv getting stuck after a rewrite of cbv_opaque function (#13122) Wojciech Różowski 2026-03-25 18:13:13 +00:00
• dee571e13b
  chore: revert mvcgen witnesses syntax (#12882) (#13120) Sebastian Graf 2026-03-25 18:56:04 +01:00
• 51f67be2bd
  chore: remove unnecessary level normalization from Sym-based mvcgen (#13119) Sebastian Graf 2026-03-25 17:06:57 +01:00
• c77f2124fb
  fix: include modPkgExt in .ir file exports (#13118) Sebastian Ullrich 2026-03-25 16:49:42 +01:00
• d634f80149 chore: update stage0 Lean stage0 autoupdater 2026-03-25 15:45:01 +00:00
• 40cdec76c5
  chore: revert @[mvcgen_witness_type] attribute (#12882) (#13111) Sebastian Graf 2026-03-25 15:38:59 +01:00
• 4227765e2b chore: update stage0 Lean stage0 autoupdater 2026-03-25 14:58:54 +00:00
• 438d1f1fe1
  perf: reading from persistent values should count as borrowing (#13116) Henrik Böving 2026-03-25 13:22:00 +01:00
• 4786e082dc
  doc: update inferInstanceAs docstring and rename normalizeInstance to wrapInstance (#13115) Kim Morrison 2026-03-25 13:20:49 +11:00
• bd5fb4e90c
  fix: handle duplicate nightly tag in scheduled CI runs (#13114) Kim Morrison 2026-03-25 12:10:54 +11:00
• e60078db3b
  test: harden sym mvcgen bench script and tune benchmark sizes (#13107) Sebastian Graf 2026-03-24 22:14:36 +01:00
• f7102363de
  fix: lake: race condition in Cache.saveArtifact (#13110) Mac Malone 2026-03-24 15:05:56 -04:00
• ce073771b1
  feat: String.drop lemmas (#13109) Markus Himmel 2026-03-24 18:51:06 +01:00
• dec394d3a4
  feat: lemmas about String.Pos.nextn (#13106) Markus Himmel 2026-03-24 17:12:57 +01:00
• 6457e3686f
  feat: lemmas for String.front? (#13105) Markus Himmel 2026-03-24 15:38:27 +01:00
• c14fa66068 chore: update stage0 Lean stage0 autoupdater 2026-03-24 14:42:18 +00:00
• d0aa7d2faa
  perf: mark inhabited arguments to extern as borrowed (#13094) Henrik Böving 2026-03-24 14:54:06 +01:00
• 4117ceaf84
  doc: typo fix for strict implicit binder (#13099) JadAbouHawili 2026-03-24 15:15:23 +02:00
• a824e5b85e
  test: add iota reduction via reduceRecMatcher? to sym-based mvcgen' (#13100) Sebastian Graf 2026-03-24 13:52:01 +01:00
• 83c6f6e5ac
  test: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen (#12893) Sebastian Graf 2026-03-24 12:27:13 +01:00
• 9ffd748104
  chore: generalize theorems about Nat.ofDigitChars (#13098) Markus Himmel 2026-03-24 12:01:20 +01:00
• fd8d89853b
  feat: print more information for LCNF RC ops (#13097) Henrik Böving 2026-03-24 11:54:08 +01:00
• 0260c91d03
  feat: lemmas comparing List.Cursor.pos to List.length (#13096) Markus Himmel 2026-03-24 11:40:03 +01:00
• 7ef25b8fe3
  chore: remove dead code (#13093) Henrik Böving 2026-03-24 10:07:47 +01:00
• 50544489a9 chore: update stage0 Lean stage0 autoupdater 2026-03-24 08:45:44 +00:00
• e9a8b965aa
  fix: remove extra universe parameter fromStd.Iter.intercalateString (#13092) Markus Himmel 2026-03-24 09:21:55 +01:00
• 0f277c72bf
  feat: verify String.join (#13091) Markus Himmel 2026-03-24 08:42:41 +01:00
• 59ce52473a
  feat: Char.toNat_mk (#13090) Markus Himmel 2026-03-24 08:16:29 +01:00
• 2b55144c3f
  feat: add extensible state mechanism for SymM (#13080) Leonardo de Moura 2026-03-23 20:58:45 -07:00
• c381c62060
  chore: use Lake remote cache in CI (#10880) Mac Malone 2026-03-23 20:06:19 -04:00
• e6df474dd9
  chore: improve inferInstanceAs error message on missing expected type and back compat (#13051) Sebastian Ullrich 2026-03-24 00:21:26 +01:00
• e0de32ad48
  fix: use declName? pattern for normalizeInstance meta marking (#13059) Kim Morrison 2026-03-24 10:01:01 +11:00
• fb1dc9112b
  perf: forward and backward borrow propagation is non-forced (#13066) Henrik Böving 2026-03-23 22:39:17 +01:00
• 86175bea00
  perf: teach borrow inference about arrays (#13064) Henrik Böving 2026-03-23 19:10:50 +01:00
• 9eb249e38c
  fix: lake: error on executables with duplicate root module names (#13028) Mac Malone 2026-03-23 14:10:10 -04:00
• b5036e4d81
  doc: rewrite ReducibilityHints docstring (#13065) Joachim Breitner 2026-03-23 18:02:27 +01:00
• fb1eb9aaa7 chore: update stage0 Lean stage0 autoupdater 2026-03-23 15:31:56 +00:00
• 33e63bb6c3
  perf: mark ReaderT context argument as borrow (#12942) Henrik Böving 2026-03-23 15:45:52 +01:00
• 482d7a11f2
  chore: handle empty dirs more gracefully (#13062) Garmelon 2026-03-23 15:23:47 +01:00
• aef0cea683 chore: update stage0 Lean stage0 autoupdater 2026-03-23 14:42:07 +00:00
• 720cbd6434
  feat: theorems are opaque (#12973) Joachim Breitner 2026-03-23 14:57:07 +01:00
• 26ad4d6972
  feat: name the functional argument to brecOn in structural recursion (#12987) Joachim Breitner 2026-03-23 14:40:18 +01:00
• 4a17b2f471
  chore: lemmas about BEq on List String.Slice (#13061) Markus Himmel 2026-03-23 14:34:46 +01:00
• fcdd9d1ae8
  feat: EquivBEq and LawfulHashable for String.Slice (#13058) Markus Himmel 2026-03-23 12:10:00 +01:00
• 47427f8c77 chore: update stage0 Lean stage0 autoupdater 2026-03-23 10:33:50 +00:00
• 08595c5f8f
  fix: interaction of extern annotations and calls to functions with borrowed parameters (#13052) Henrik Böving 2026-03-23 11:03:26 +01:00
• 019b104a7d
  chore: variants of String.toNat? lemmas (#13057) Markus Himmel 2026-03-23 10:32:32 +01:00
• 2e421c9970
  feat: Std.Iter.intercalateString (#13056) Markus Himmel 2026-03-23 10:28:42 +01:00
• e381960614
  feat: simproc for turning "c" into String.singleton 'c' (#13054) Markus Himmel 2026-03-23 10:06:49 +01:00
• 346c9cb16a
  chore: CI: bump git cache to 5GB (#13053) Sebastian Ullrich 2026-03-23 09:58:35 +01:00
• 189cea9f80
  chore: check for empty PRs in CI (#12956) Kim Morrison 2026-03-23 14:09:52 +11:00
• b9028fa6e9
  fix: handle lean4-nightly toolchain prefix in release checklist (#12865) Kim Morrison 2026-03-23 14:01:58 +11:00
• 0c0edcc96c
  feat: add control and arrow_telescope simproc DSL primitives (#13048) Leonardo de Moura 2026-03-22 19:19:13 -07:00
• 9f4db470c4
  feat: add permutation theorem support to Sym.simp (#13046) Leonardo de Moura 2026-03-22 17:22:36 -07:00
• 8ae39633d1
  fix: mark auxiliary definitions from normalizeInstance as meta (#13043) Kim Morrison 2026-03-23 09:41:57 +11:00
• cffacf1b10
  feat: support local hypotheses in simp [h] for sym => mode (#13042) Leonardo de Moura 2026-03-22 14:50:31 -07:00
• b858d0fbf2
  feat: adapt non-equality theorems in mkTheoremFromDecl (#13041) Leonardo de Moura 2026-03-22 12:34:37 -07:00
• 9a3678935d
  feat: add sanity checks to register_sym_simp (#13040) Leonardo de Moura 2026-03-22 10:41:30 -07:00
• c9708e7bd7
  doc: update docstring of Lean.Parser.Tactic.Grind.first (#12998) Chris Henson 2026-03-22 12:54:33 -04:00
• 8f6411ad57
  feat: add interactive simp tactic for sym => mode (#13039) Leonardo de Moura 2026-03-22 08:55:05 -07:00
• ae0d4e3ac4
  chore: remove change ... with tactic syntax (#13029) Kyle Miller 2026-03-22 08:25:21 -07:00
• 4bf7fa7447 chore: fix build after rebootstrap Sebastian Ullrich 2026-03-18 13:59:19 +00:00
• 40558129cf chore: update stage0 Sebastian Ullrich 2026-03-22 11:35:16 +00:00
• 88b746dd48 feat: unfold and rewrap instances in inferInstanceAs and deriving Sebastian Ullrich 2026-03-22 10:35:13 +00:00
• 2a25e4f3ae
  fix: nightly dispatch creates today's tag when retrying a failed nightly (#13035) Kim Morrison 2026-03-22 22:30:36 +11:00
• 13f8ce8492
  feat: add register_sym_simp command and SymSimpVariant infrastructure (#13034) Leonardo de Moura 2026-03-21 21:30:58 -07:00
• dbfd0d35f2
  fix: simp +arith and grind loop on normalized Int equalities (#13033) Leonardo de Moura 2026-03-21 21:04:56 -07:00
• b4c4f265aa
  fix: grind ring solver OOM on high-degree polynomials (#13032) Leonardo de Moura 2026-03-21 19:52:44 -07:00
• e848039ba9
  feat: add built-in sym_simproc and sym_discharger elaborators (#13031) Leonardo de Moura 2026-03-21 19:39:12 -07:00
• 9fa1a252f2
  fix: nondeterministic crash in grind congruence closure (#13027) Leonardo de Moura 2026-03-21 15:54:58 -07:00
• 1cf030c5d4 chore: update stage0 Lean stage0 autoupdater 2026-03-21 23:14:34 +00:00
• 545f27956b
  feat: add sym_simproc and sym_discharger DSL syntax categories (#13026) Leonardo de Moura 2026-03-21 15:29:25 -07:00
• 7897dc91e6
  fix: grind fails to prove conjunction of independently provable goals (#13024) Leonardo de Moura 2026-03-21 10:04:41 -07:00
• 98f5266407
  chore: remove temp bootstrap code (#13021) Sebastian Ullrich 2026-03-21 17:41:14 +01:00
• 90b5e3185b
  fix: export ABI mismatch (#13022) Sebastian Ullrich 2026-03-21 15:52:23 +01:00
• 973062e4e1
  feat: add Sym.simp theorem set attributes (#13018) Leonardo de Moura 2026-03-20 20:53:39 -07:00
• 4a62d4a79b chore: update stage0 Lean stage0 autoupdater 2026-03-21 00:19:46 +00:00