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

  • 347fcf9531 whitespace, oof paul/fix-warnings Paul Reichert 2026-03-06 22:19:25 +01:00
  • 6363a984cf fix test Paul Reichert 2026-03-06 18:30:15 +01:00
  • bde339f961 String.Pattern.Basic Paul Reichert 2026-03-06 17:51:49 +01:00
  • 169d910ff8 Init.Dynamic Paul Reichert 2026-03-06 17:19:32 +01:00
  • c9b888e2b1 build-template Paul Reichert 2026-03-06 17:16:34 +01:00
  • fcd8c75b2a more implicit_reducibles Paul Reichert 2026-03-06 17:14:54 +01:00
  • 0bd33a9283 fix warnings Paul Reichert 2026-03-06 15:49:30 +01:00
  • a3cb39eac9 chore: migrate more tests to new test suite (#12809) Garmelon 2026-03-06 17:52:01 +01:00
  • 54f188160c fix: cbv handling of ite/dite/decide (#12816) Wojciech Różowski 2026-03-06 16:18:39 +00:00
  • 68ea28c24f feat: Array.mergeSort (#12385) Paul Reichert 2026-03-06 14:18:13 +01:00
  • 35944c367b feat: leading whitespace on first token (#12662) Marc Huisinga 2026-03-06 13:46:44 +01:00
  • 5f3ca3ac3d feat: unify name demangling with single Lean implementation (#12539) Kim Morrison 2026-03-06 23:29:35 +11:00
  • ee293de982 test: add instantiateMVars tests and benchmark for delayed assignments (#12808) Joachim Breitner 2026-03-06 11:59:13 +01:00
  • 25e8e043b8 fix: address review feedback for name demangling (round 2) feat/lean-name-demangling Kim Morrison 2026-03-06 05:05:38 +00:00
  • 1c37c3b734 fix: remove reentrancy guard from backtrace demangler Kim Morrison 2026-02-20 10:03:36 +00:00
  • 8b27fdb2d6 refactor: replace shadow string API with modern String API in name demangling Kim Morrison 2026-02-20 05:42:49 +00:00
  • bee68d41aa fix: address further review feedback for name demangling Kim Morrison 2026-02-20 04:46:15 +00:00
  • f2694b8bc2 fix: address review feedback for name demangling Kim Morrison 2026-02-18 05:41:32 +00:00
  • 6cdaee43b8 fix: use weak symbol for backtrace demangler to avoid leanrt → libLean link dependency Kim Morrison 2026-02-18 03:53:38 +00:00
  • 8c3d05621b feat: unify name demangling with single Lean implementation Kim Morrison 2026-02-18 00:09:55 +00:00
  • 10ccc015ff test: add scope_cache verification model and dual tests Joachim Breitner 2026-03-06 07:02:07 +00:00
  • 88b3086444 doc: improve scope_cache documentation, make rewind private Joachim Breitner 2026-03-06 06:44:51 +00:00
  • 1822df59d3 chore: grind guard condition for eq_or_mem_of_mem_cons eq_or_mem_of_mem_cons Kim Morrison 2026-03-06 06:42:28 +00:00
  • 596d13f6d4 fix: remove @[grind →] from getElem_of_getElem? (#12821) Kim Morrison 2026-03-06 15:18:21 +11:00
  • ef26f95ee6 feat: move instance-class check to declaration site (#12325) Sebastian Ullrich 2026-03-06 11:23:27 +08:00
  • 20059c0c99 fix: remove @[grind →] from getElem_of_getElem? (#12821) backport-12821-to-releases/v4.29.0 Kim Morrison 2026-03-06 15:18:21 +11:00
  • a165292462 fix: remove @[grind →] from getElem_of_getElem? (#12821) Kim Morrison 2026-03-06 15:18:21 +11:00
  • db6aa9d8d3 feat: move instance-class check to declaration site (#12325) Sebastian Ullrich 2026-03-06 11:23:27 +08:00
  • ed910f9b59 fix: mark Id.run as [implicit_reducible] (#12757) Leonardo de Moura 2026-03-04 17:38:07 -08:00
  • 1c667a8279 chore: update stage0 Kim Morrison 2026-03-06 03:19:45 +00:00
  • 847c32c0df refactor: replace isImplicitReducible with Meta.isInstance in shouldInline (#12759) Leonardo de Moura 2026-03-02 13:49:46 -08:00
  • 4e4b609411 fix: use fully qualified names in grind.unusedLemmaThreshold output Kim Morrison 2026-03-05 23:43:48 +00:00
  • 9284c3c2d5 refactor: overhaul terminology in instantiate_mvars_all.cpp Joachim Breitner 2026-03-05 22:59:29 +00:00
  • f51fb1e866 fix: format sofia/time-format-refactor Sofia Rodrigues 2026-03-05 16:03:25 -03:00
  • d05e772630 fix: format Sofia Rodrigues 2026-03-05 15:43:15 -03:00
  • f67de6649f refactor: assert fvar_subst_empty in non-resolvable delayed mvar path Joachim Breitner 2026-03-05 18:02:01 +00:00
  • 07f526d035 style: flip is_resolvable_pending branch to avoid negation Joachim Breitner 2026-03-05 18:00:55 +00:00
  • 32948acdd9 refactor: make args buffer local to visit_delayed Joachim Breitner 2026-03-05 18:00:21 +00:00
  • 99e9da1a7d doc: explain write-back behavior of pass 2 delayed mvar resolution Joachim Breitner 2026-03-05 17:58:08 +00:00
  • ad9be0f985 refactor: add proper accessors for DelayedMetavarAssignment fields Joachim Breitner 2026-03-05 17:49:42 +00:00
  • bcf308b6be Redundant checks Joachim Breitner 2026-03-05 17:43:04 +00:00
  • a61d5b61ee refactor: merge resolvability checker into pass 2, simplify pass 1 Joachim Breitner 2026-03-05 17:35:25 +00:00
  • 5ce31b8036 Manual comment tweaks Joachim Breitner 2026-03-05 17:08:49 +00:00
  • 6ebe573c19 fix: kernel: move level parameter count and thm-is-prop checks for robustness (#12817) Joachim Breitner 2026-03-05 18:03:01 +01:00
  • f42e6dd589 refactor: clarify pass 2 invariants for mvar and delayed assignment handling Joachim Breitner 2026-03-05 16:59:01 +00:00
  • e2bbd746ef refactor: remove m_global_cache from pass 2, use has_expr_mvar Joachim Breitner 2026-03-05 16:31:40 +00:00
  • d39e16e522 test: improve instantiateMVars tests and add sharing benchmark joachim/instmvarstests Joachim Breitner 2026-03-05 16:10:58 +00:00
  • f059a1ebd3 chore: update stage0 Lean stage0 autoupdater 2026-03-05 15:36:46 +00:00
  • a34777a08d feat: make the borrow inference explain itself (#12810) Henrik Böving 2026-03-05 15:18:13 +01:00
  • 5be03078fa fix: check scope generation at all levels in scope_cache rewind Joachim Breitner 2026-03-05 13:37:21 +00:00
  • 8e26cadf9b fix: selector sofia/fix-signal Sofia Rodrigues 2026-03-05 10:35:47 -03:00
  • c5e7a30610 test: add cross-scope sharing test for instantiateMVars Joachim Breitner 2026-03-05 12:04:24 +00:00
  • 3650e9f6b7 test: add instantiateMVars tests and benchmark for delayed assignments Joachim Breitner 2026-03-05 12:01:40 +00:00
  • 336c060a5b test: add cross-scope sharing test for scope_cache insert Joachim Breitner 2026-03-05 10:47:53 +00:00
  • 3c17c8c1b0 perf: reuse cached values across scopes in scope_cache insert Joachim Breitner 2026-03-05 10:32:00 +00:00
  • 56aa64e15c refactor: extract scope-aware cache into scope_cache.h Joachim Breitner 2026-03-05 09:07:41 +00:00
  • fe1ad52f88 fix: export String.find? and String.contains lemmas (#12807) Markus Himmel 2026-03-05 11:00:17 +01:00
  • 7973ba1880 fix hbv/persistent_simple_ground Henrik Böving 2026-03-05 09:08:50 +00:00
  • cead4665d0 chore: remove instantiateMVarsNoUpdate variant Joachim Breitner 2026-03-05 09:02:09 +00:00
  • 285a1e2831 for now hbv/xid Henrik Böving 2026-03-05 08:42:24 +00:00
  • 46f6b43eb4 feat: add grind.unusedLemmaThreshold option to report unused E-matching activations Kim Morrison 2026-03-05 06:51:01 +00:00
  • 0bb0dd0685 feat: track persistently which declarations are simple ground Henrik Böving 2026-03-05 08:38:02 +00:00
  • 8d42ad4796 fix: re-apply "mark Id.run as [implicit_reducible]" (#12802) Kim Morrison 2026-03-05 19:03:09 +11:00
  • 9af33d5d32 Revert "fix: revert "mark Id.run as [implicit_reducible]" (#12801)" re-apply-12757 Kim Morrison 2026-03-05 06:23:33 +00:00
  • 333ab1c6f0 fix: revert "mark Id.run as [implicit_reducible]" (#12801) Kim Morrison 2026-03-05 16:40:16 +11:00
  • 4384344465 feat: lake: use trace mtime for arts when possible (#12799) Mac Malone 2026-03-04 23:53:59 -05:00
  • 1a77a5f631 Revert "fix: mark Id.run as [implicit_reducible] (#12757)" revert-12757 Kim Morrison 2026-03-05 04:05:06 +00:00
  • 3cfa2dac42 fix: handle CACHE STRING syntax in LEAN_VERSION_IS_RELEASE check (#12800) Kim Morrison 2026-03-05 13:09:51 +11:00
  • b83c0eefc3 perf: add high priority to OfSemiring.Q instances (#12782) v4.29.0-rc5 Leonardo de Moura 2026-03-04 04:58:15 -08:00
  • 24a254aec2 fix: handle CACHE STRING syntax in LEAN_VERSION_IS_RELEASE check fix-release-checklist-is-release-check Kim Morrison 2026-03-05 01:59:25 +00:00
  • 1a612b77f6 fix: release_checklist LEAN_VERSION_IS_RELEASE check with CACHE STRING syntax Kim Morrison 2026-03-05 01:57:25 +00:00
  • e044ffae6a fix: mark Id.run as [implicit_reducible] (#12757) Leonardo de Moura 2026-03-04 17:38:07 -08:00
  • 3b6e65dcae fix: mark Id.run as [implicit_reducible] idrun_issue Leonardo de Moura 2026-03-01 14:28:02 -08:00
  • 937b0fc92e perf: lazy persistent-list cache for pass 2 scope tracking Joachim Breitner 2026-03-04 23:06:16 +00:00
  • cfc8f2f7f2 onward Henrik Böving 2026-03-04 22:05:30 +00:00
  • 09f8cfc539 fix: deadlock when uv_tcp_accept is under contention (#12796) Henrik Böving 2026-03-04 21:01:28 +01:00
  • 5191b30b20 fix: memleak on lean_uv_dns_get_name error path (#12795) Henrik Böving 2026-03-04 20:56:43 +01:00
  • c8c702af8d Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-04 16:40:39 -03:00
  • 5b5b0fad70 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-04 16:40:33 -03:00
  • eab144bbb2 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-04 16:40:27 -03:00
  • cfe282f024 fix: port parse Sofia Rodrigues 2026-03-04 16:40:03 -03:00
  • e7f06c8fa2 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-04 16:34:41 -03:00
  • beb85dd6b0 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-04 16:34:27 -03:00
  • debafcf0ef Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-04 16:29:43 -03:00
  • 2668f07808 fix: alpha and isdigit Sofia Rodrigues 2026-03-04 16:29:31 -03:00
  • e8b7619b09 fix hbv/fix_uv_tcp_accept_deadlock Henrik Böving 2026-03-04 19:28:03 +00:00
  • e3928b7b1a Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-04 16:26:56 -03:00
  • 2f3a97ed8a Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-04 16:26:48 -03:00
  • 0315d56389 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-04 16:26:38 -03:00
  • 354a968b13 fix: memleak on libuv error path hbv/fix_uv_memleak Henrik Böving 2026-03-04 19:26:03 +00:00
  • b9e489cc8f Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-04 16:22:58 -03:00
  • 10ece4e082 refactor: reduce duplication in string pattern lemmas (#12793) Markus Himmel 2026-03-04 18:50:32 +01:00
  • 7223b0c025 feat: XID identifier support Henrik Böving 2026-02-27 14:00:33 +00:00
  • 135b049080 Merge branch 'master' into sofia/async-http-headers Sofia Rodrigues 2026-03-04 13:22:45 -03:00
  • 8526edb1fc feat: uniquification of binder names in LCNF.Internalize (#12792) Henrik Böving 2026-03-04 17:17:58 +01:00
  • caad260789 chore: update stage0 Lean stage0 autoupdater 2026-03-04 16:32:35 +00:00
  • 27721aaf8e feat: uniqification of binder names in LCNF.Internalize hbv/lcnf_internalize_unique_binders Henrik Böving 2026-03-04 16:07:17 +00:00
  • 2f3d0ee6ad feat: add cbv.maxSteps option to control step limit (#12788) Wojciech Różowski 2026-03-04 16:05:57 +00:00
  • eacb82e5f3 test: move cbv tests to appropriate directories (#12791) Wojciech Różowski 2026-03-04 15:53:05 +00:00
  • e78ba3bd85 perf: remove void JP arguments (#12790) Henrik Böving 2026-03-04 16:46:42 +01:00