sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 8afae00064 refactor: merge two-phase split proof into single pass with metavariables Sebastian Graf 2026-03-12 07:11:45 +00:00
  • d1c1a7242c refactor: clean up split backward rule generation in sym MVCGen Sebastian Graf 2026-03-11 18:55:14 +00:00
  • f70abe08a5 feat: add dite and matcher splitting to sym-based MVCGen Sebastian Graf 2026-03-11 13:08:19 +00:00
  • aae827cb4c refactor: replace flat Array Expr with TransformAltFVars in MatcherApp.transform (#12902) Sebastian Graf 2026-03-13 05:48:08 +08:00
  • 9c87a9f044 Merge branch 'sofia/async-http-h1' into sofia/async-http-server sofia/async-http-server Sofia Rodrigues 2026-03-12 15:52:36 -03:00
  • 34c9cafc12 fix: type sofia/async-http-h1 Sofia Rodrigues 2026-03-12 15:52:29 -03:00
  • 014dd1d263 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-12 15:43:28 -03:00
  • 2a7a407875 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-12 15:43:06 -03:00
  • e359001026 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-12 15:39:08 -03:00
  • 72244398dc fix: test Sofia Rodrigues 2026-03-12 15:38:59 -03:00
  • c0e60b797c Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-12 15:33:48 -03:00
  • 400908a2f4 fix: port and fragment Sofia Rodrigues 2026-03-12 15:09:49 -03:00
  • 394c999c2a fix: uri Sofia Rodrigues 2026-03-12 15:03:49 -03:00
  • b7e88dadeb Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-12 15:01:03 -03:00
  • a39a0575a0 Merge branch 'master' into sofia/async-http-headers Sofia Rodrigues 2026-03-12 14:35:25 -03:00
  • 5815f33342 Merge branch 'sofia/fix-native-decide' into sofia/async-http-headers Sofia Rodrigues 2026-03-12 14:17:13 -03:00
  • 47833725ea feat: add String simprocs to cbv (#12888) Wojciech Różowski 2026-03-12 11:52:06 +00:00
  • 24acf2b895 chore: update stage0 Lean stage0 autoupdater 2026-03-11 21:36:12 +00:00
  • d9ebd51c04 feat: option to ignore borrowing annotations completely (#12886) Henrik Böving 2026-03-11 21:59:06 +01:00
  • 1fb5e0e40f feat: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen Sebastian Graf 2026-03-11 18:59:01 +00:00
  • 6a2a884372 chore: migrate pkg tests (#12889) Garmelon 2026-03-11 19:55:46 +01:00
  • 4740e044c8 test: add elab_bench for string literal simp performance (#12883) Joachim Breitner 2026-03-11 17:06:26 +01:00
  • 4deb8d5b50 chore: do not use internal append in ToString instances for basic types (#12885) Markus Himmel 2026-03-11 16:25:54 +01:00
  • d3db4368d4 chore: update stage0 Lean stage0 autoupdater 2026-03-11 14:53:48 +00:00
  • 9d30f6a0c5 perf: optimize string literal equality simprocs for kernel efficiency joachim/string-neq-proc2 Joachim Breitner 2026-03-11 14:27:23 +00:00
  • 652ca9f5b7 refactor: port EmitC to LCNF (#12781) Henrik Böving 2026-03-11 15:19:54 +01:00
  • e6c511a9a3 test: add elab_bench for string literal simp performance joachim/string-neq-proc Joachim Breitner 2026-03-11 14:18:07 +00:00
  • a32be44f90 feat: add @[mvcgen_witness_type] attribute for extensible witness classification (#12882) Sebastian Graf 2026-03-11 19:38:05 +08:00
  • e43b526363 feat: add cbv simprocs for arrays (#12875) Wojciech Różowski 2026-03-11 11:03:22 +00:00
  • 734566088f feat: add withEarlyReturnNewDo variants for new do elaborator (#12881) Sebastian Graf 2026-03-11 18:44:34 +08:00
  • c1a3636bae feat: add withEarlyReturnNewDo variants for new do elaborator withEarlyReturnNewDo Sebastian Graf 2026-03-11 10:33:11 +00:00
  • 17807e1cbe feat: apply @[mvcgen_invariant_type] to Invariant, StringInvariant, StringSliceInvariant (#12880) Sebastian Graf 2026-03-11 18:00:24 +08:00
  • 4450ff8995 chore: fix shlib rebuild detection under LAKE_USE_CACHE (#12879) Sebastian Ullrich 2026-03-11 09:35:53 +01:00
  • 9fac847f5f perf: faster LCNF internalization (#12878) Henrik Böving 2026-03-11 09:15:05 +01:00
  • 7acf5710c4 chore: update stage0 Lean stage0 autoupdater 2026-03-11 08:49:43 +00:00
  • 220a242f65 feat: add @[mvcgen_invariant_type] attribute for extensible invariant classification (#12874) Sebastian Graf 2026-03-11 16:04:22 +08:00
  • 7217ddc052 perf: faster LCNF internalization hbv/perf_internalize Henrik Böving 2026-03-10 12:59:31 +00:00
  • 230dcd5cec Merge branch 'master' into mvcgen-invariant-attr mvcgen-invariant-attr Sebastian Graf 2026-03-11 15:42:02 +08:00
  • b9ab24a001 chore: trigger stage0 update for @[mvcgen_invariant_type] Sebastian Graf 2026-03-11 06:56:49 +00:00
  • dbcdfd080c test: add end-to-end test for @[mvcgen_invariant_type] with String iteration Sebastian Graf 2026-03-11 06:40:30 +00:00
  • ff6816a854 fix: avoid duplicate lake test registration when LAKE_CI is on (#12877) Kim Morrison 2026-03-11 16:51:09 +11:00
  • 25a72632be fix: avoid duplicate lake test registration when LAKE_CI is on fix-lake-ci-duplicate-test Kim Morrison 2026-03-11 03:39:35 +00:00
  • cd85b93d93 fix: lake-ci test glob (#12876) Mac Malone 2026-03-10 23:31:44 -04:00
  • bb047b8725 fix: improve Name.isMetaprogramming (#12767) Jovan Gerbscheid 2026-03-10 21:35:47 +00:00
  • 0b6cf8e962 [Backport releases/v4.29.0] fix: remove @[grind →] from getElem_of_getElem? (#12823) github-actions[bot] 2026-03-11 08:34:51 +11:00
  • 2ea4d016c4 doc: remark that CoreM.toIO ignores ctx.initHeartbeats (#12859) Eric Wieser 2026-03-11 06:34:11 +09:00
  • 4fdf94ed3d refactor: simplify error Sofia Rodrigues 2026-03-10 15:58:40 -03:00
  • 66743e80a6 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-10 15:58:20 -03:00
  • 2d0d63f5d3 refactor: move logic Sofia Rodrigues 2026-03-10 15:58:07 -03:00
  • 10951fdb57 refactor: use closewitherror Sofia Rodrigues 2026-03-10 15:37:06 -03:00
  • 71d3967338 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-10 15:36:54 -03:00
  • 34dbcb2ca5 refactor: add close with error Sofia Rodrigues 2026-03-10 15:35:34 -03:00
  • abb60e47c8 refactor: make smaller Sofia Rodrigues 2026-03-10 15:19:27 -03:00
  • feed36e06e feat: add @[mvcgen_invariant_type] attribute for extensible invariant classification Sebastian Graf 2026-03-10 18:05:27 +00:00
  • 560387b2e4 perf: skip redundant typeclass synthesis retries in synthesizeSyntheticMVarsStep joachim/synthRetry Joachim Breitner 2026-03-10 16:05:06 +00:00
  • b626c6d326 test: apply simp theorems in SymM mvcgen' (#12872) Sebastian Graf 2026-03-11 01:15:04 +08:00
  • 7bdea921d4 test: apply simp theorems in SymM mvcgen' mvcgen-simp Sebastian Graf 2026-03-10 16:01:43 +00:00
  • ebfc34466b refactor: use builtin_cbv_simproc for the control-flow simprocs in cbv (#12870) Wojciech Różowski 2026-03-10 16:37:09 +00:00
  • 49ed556479 test: add VCGen test suite for sym mvcgen benchmarks (#12855) Sebastian Graf 2026-03-10 21:32:13 +08:00
  • e9060e7a4e fix: remove use of native_decide in the HTTP library (#12857) Sofia Rodrigues 2026-03-10 10:25:22 -03:00
  • 0ebc126718 chore: update stage0 Lean stage0 autoupdater 2026-03-10 13:16:48 +00:00
  • 7a852aedb6 fix: squeeze simp and paren sofia/fix-native-decide Sofia Rodrigues 2026-03-10 10:08:22 -03:00
  • 310d3e2a8c remove letToHave mvar dep let check kmill_fix_8488 Kyle Miller 2026-03-10 06:04:47 -07:00
  • daddac1797 feat: support expected type annotation in doPatDecl (#12866) Sebastian Graf 2026-03-10 19:42:03 +08:00
  • 04f676ec64 chore: update stage0 Lean stage0 autoupdater 2026-03-10 11:49:44 +00:00
  • 2fb69bec1f feat: support expected type annotation in doPatDecl do-let-arrow-pat-expected-type Sebastian Graf 2026-03-10 11:03:45 +00:00
  • 9b1973ada7 feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures (#12597) Wojciech Różowski 2026-03-10 10:59:13 +00:00
  • 9ecc7e2b4a refactor: use skip lists for grind_lint tests and avoid redundant struct matching grind-eta-struct-for-eq Kim Morrison 2026-03-10 09:27:35 +00:00
  • 3e85da2305 test: update try_first_par test for Eq-triggered eta-expansion Kim Morrison 2026-03-10 05:41:17 +00:00
  • 3713cfa10c test: update grind_lint expected output for new eta-expansion Kim Morrison 2026-03-10 01:56:07 +00:00
  • 3729e0e5b5 feat: auto eta-expand structures in grind when equality with constructor is present Kim Morrison 2026-03-10 01:25:17 +00:00
  • 85d38cba84 feat: allow erasing cbv_eval attributes (#12851) Wojciech Różowski 2026-03-10 09:40:19 +00:00
  • e5e7dcc00f chore: measure EmitC accurately (#12864) Henrik Böving 2026-03-10 10:19:32 +01:00
  • fe323eaf97 fix: handle lean4-nightly toolchain prefix in release checklist fix-checklist-nightly-parsing Kim Morrison 2026-03-10 09:10:29 +00:00
  • 035baff73b take/drop array lemmas paul/extractdroptakenf Paul Reichert 2026-03-10 09:43:02 +01:00
  • d266968343 chore: add leansqlite to release repos chore/add-leansqlite-to-release-repos Kim Morrison 2026-03-10 08:41:06 +00:00
  • ce6a07c4d9 feat: persistent hash map iterator (#12852) Paul Reichert 2026-03-10 09:01:32 +01:00
  • 320ddae700 feat: add lake-ci label to enable full Lake test suite (#12836) Kim Morrison 2026-03-10 14:23:35 +11:00
  • 073af2ad03 fix: lake-ci no longer implies release-ci feat/lake-ci-label Kim Morrison 2026-03-10 03:06:27 +00:00
  • ada53633dc feat: add grind.unusedLemmaThreshold option to report unused E-matching activations (#12805) Kim Morrison 2026-03-10 13:57:37 +11:00
  • 329c35b3f0 chore: merge master (test directory rename) kim/grind-unused-lemma-threshold Kim Morrison 2026-03-10 02:44:13 +00:00
  • e01cbf2b8f feat: add structured TraceResult to TraceData (#12698) Kim Morrison 2026-03-10 13:42:57 +11:00
  • 1554f57525 fix: import Sofia Rodrigues 2026-03-09 21:18:57 -03:00
  • 1fa01cdadb style: just removed variable Sofia Rodrigues 2026-03-09 20:16:50 -03:00
  • 758e5afb07 refactor: simplify Sofia Rodrigues 2026-03-09 20:15:26 -03:00
  • 11516bbf09 fix: import Sofia Rodrigues 2026-03-09 20:12:32 -03:00
  • f76dca5bba fix: proof Sofia Rodrigues 2026-03-09 20:11:12 -03:00
  • fe6ac812af fix: panic Sofia Rodrigues 2026-03-09 16:21:05 -03:00
  • 51a00843ea fix: remove usage of Sofia Rodrigues 2026-03-09 10:01:29 -03:00
  • 71ff366211 feat: use unicode(...) in Init/Notation and elsewhere (#10384) Kyle Miller 2026-03-09 15:17:32 -07:00
  • 670360681f perf: handle match_same_ctor.het similar to matchers in compiler (#12850) Henrik Böving 2026-03-09 23:02:06 +01:00
  • 8dae7f3705 cleanups Paul Reichert 2026-03-09 21:54:47 +01:00
  • c7fd74b6e3 update patchwork Paul Reichert 2026-02-28 16:03:08 +01:00
  • 9c93e7e6c1 fix tests Paul Reichert 2026-02-28 15:40:16 +01:00
  • 6730dbdc25 add extract_eq_take_drop Paul Reichert 2026-02-28 01:44:27 +01:00
  • d1fb514587 Array.take/drop Paul Reichert 2026-02-28 01:40:29 +01:00
  • d1200f0234 start changing Array Paul Reichert 2026-02-27 21:09:29 +01:00
  • 64029912df fixes Paul Reichert 2026-02-27 12:58:11 +01:00
  • 7c92bebd0c ... Paul Reichert 2026-02-27 12:40:24 +01:00
  • e63d0e1cd0 patchwork file Paul Reichert 2026-02-26 16:22:44 +01:00