Commit graph

  • ba016b2130 Phase 0: fork infrastructure master Maximus Gorog 2026-05-22 12:43:41 -06:00
  • ad1c983a43
    fix: run beforeElaboration attributes on inductives (#13813) Kyle Miller 2026-05-21 12:45:59 -07:00
  • 47e96cd458
    feat: add module features to #where command (#13811) Kyle Miller 2026-05-21 11:11:43 -07:00
  • 1842bb5476
    feat: improve performance of structure instance notation elaboration (#13760) Kyle Miller 2026-05-21 09:53:33 -07:00
  • ed790e99b0
    fix: strip hypothesis-naming metadata from proof-mode targets (#13812) Sebastian Graf 2026-05-21 17:18:17 +01:00
  • df2a367958
    doc: fix wrong example for String.split (#13787) Christian Krause 2026-05-21 12:17:58 +02:00
  • 8f49fe9864
    chore: clean up string processing (#13802) Julia Markus Himmel 2026-05-21 09:46:57 +01:00
  • 0db4ac18e5
    feat: beta reduce while elaborating applications (#13807) Kyle Miller 2026-05-21 00:26:00 -07:00
  • acfe1d1a4b
    fix: enforce proper meta discipline for Verso docstring extensions (#13808) David Thrane Christiansen 2026-05-21 07:58:09 +02:00
  • 65b34530d3
    feat: support more indexed monads in elabDoWith (#13801) Sebastian Graf 2026-05-20 18:59:25 +01:00
  • da8bcf7916
    refactor: rename mkMonadicType to mkMonadApp (#13800) Sebastian Graf 2026-05-20 17:52:58 +01:00
  • ada1696f04
    chore: clean up string processing (#13797) Julia Markus Himmel 2026-05-20 15:23:26 +01:00
  • a3fff15212
    perf: optimize String.compare (#13796) Henrik Böving 2026-05-20 13:57:48 +01:00
  • 34df732066 chore: update stage0 Lean stage0 autoupdater 2026-05-20 11:40:02 +00:00
  • 8398048832
    chore: preparation for String.compare optimization (#13795) Henrik Böving 2026-05-20 11:52:48 +01:00
  • fa2384726f
    chore: clean up string processing (#13785) Julia Markus Himmel 2026-05-20 11:39:40 +01:00
  • 727b4aad2b
    fix: lake: noRelease test flakiness (#13786) Mac Malone 2026-05-20 00:35:28 +01:00
  • 1f23107ad9
    perf: dec specialization (#13788) Henrik Böving 2026-05-19 20:56:34 +01:00
  • 0a75e1d92f
    chore: CI: fix stage2 release build (#13790) Garmelon 2026-05-19 20:23:57 +01:00
  • 29adf42309
    refactor: use builtin command elaborators for configuration evaluation (part 2) (#13780) Kyle Miller 2026-05-19 11:16:21 -07:00
  • 731d0c4878 chore: update stage0 Lean stage0 autoupdater 2026-05-19 17:02:51 +00:00
  • 690d27ebc7
    chore: clean up string processing (#13789) Julia Markus Himmel 2026-05-19 17:17:42 +01:00
  • e38c698392
    refactor: use builtin command elaborators for configuration evaluation (#13779) Kyle Miller 2026-05-19 09:08:11 -07:00
  • 3bb1493139
    refactor: remove use of liftCommandElabM from Coinductive (#13782) Kyle Miller 2026-05-19 03:53:44 -07:00
  • a0de9024e9
    refactor: avoid liftCommandElabM in @[ext] (#13781) Kyle Miller 2026-05-19 03:53:07 -07:00
  • e09155b6f9
    chore: CI: fold Linux Lake into Linux release (#13759) Sebastian Ullrich 2026-05-18 23:52:22 +01:00
  • ebbbec00f7
    refactor: dispatch try? builtins via @[builtin_try_tactic] (#13766) Joachim Breitner 2026-05-18 20:41:24 +01:00
  • 705ba6404b
    refactor: extract try? suggestions via TryThisInfo (#13774) Joachim Breitner 2026-05-18 19:41:55 +01:00
  • 6d5ec050f4
    fix: instantiate metavariables when collecting a goal's constants (#13748) Kim Morrison 2026-05-19 01:52:13 +10:00
  • 5d22886aff
    refactor: app elaborator refactoring and improvements (#13762) Kyle Miller 2026-05-18 07:41:09 -07:00
  • 3f3a26c53c
    feat: filter MePo candidates to theorems and order output by iteration (#13750) Kim Morrison 2026-05-19 00:15:06 +10:00
  • 2c38bb3306
    fix: lake: rm examples/hello use in tests/env (#13769) Mac Malone 2026-05-18 09:11:03 -04:00
  • 8f508e3c91
    fix: include zetaUnused in Meta.Config cache key (#13772) Kim Morrison 2026-05-18 22:47:19 +10:00
  • a68d753729
    fix: widen transparency field to 3 bits in Meta.Config cache key (#13768) Kim Morrison 2026-05-18 20:51:59 +10:00
  • 9df1caeb77
    feat: add ToJson/FromJson for Unit (#13525) Wojciech Nawrocki 2026-05-18 06:03:30 -04:00
  • 385efbbaa7
    fix: drop stale .reverse in MePo premise selector (#13747) Kim Morrison 2026-05-18 05:37:49 +10:00
  • 2bdc67756c
    chore: remove addInfo flag from elabSetOption (#13736) Thomas R. Murrills 2026-05-17 13:28:27 -04:00
  • ce5814043b
    feat: add MessageData.withExprHover (#13763) Kyle Miller 2026-05-17 06:39:49 -07:00
  • 43ef70db63
    fix: pp.universes should not affect constants with no universe levels (#13761) Kyle Miller 2026-05-16 18:41:04 -07:00
  • 5dea2142c3
    feat: improve performance of instantiateBetaRevRange (#13758) Kyle Miller 2026-05-16 13:55:18 -07:00
  • ef2dc0f66a
    chore: CI: build everything with Lake (#13721) Sebastian Ullrich 2026-05-16 19:11:25 +02:00
  • d64eaf4597
    chore: CI: verify lake cache step (#13735) Mac Malone 2026-05-16 12:08:38 -04:00
  • 895752dc2e
    feat: add Lean.CompactedRegion.save/read supporting cross-file object sharing (#13185) Sebastian Ullrich 2026-05-16 14:53:20 +02:00
  • 1b8f1f140c
    feat: add ByteArray indexing and set! lemmas (#13457) Kim Morrison 2026-05-16 16:28:43 +10:00
  • c993d3f237
    feat: add Dyadic.divAtPrec for round-down dyadic division at given precision (#13654) Kim Morrison 2026-05-16 15:47:39 +10:00
  • d5bcec28e5
    chore: adjust dev-release preset (#13741) Sebastian Ullrich 2026-05-16 07:32:16 +02:00
  • 1708293920
    feat: shake: precise reasons in --explain output (#13740) Sebastian Ullrich 2026-05-15 22:24:36 +02:00
  • 2acdaafcfe
    chore: CI: fix jira-sync (#13739) Sebastian Ullrich 2026-05-15 11:55:25 +02:00
  • 6749463072 chore: update stage0 Lean stage0 autoupdater 2026-05-15 09:14:30 +00:00
  • f8b7f30f5c
    fix: change plugin separator to = (#13737) Mac Malone 2026-05-15 04:28:21 -04:00
  • 047f6aaf89
    feat: efficient tactic configuration elaborators and configurability (#13651) Kyle Miller 2026-05-14 10:20:57 -07:00
  • f459c1436e
    feat: upstream unusedDecidableInType linter (#13688) Wojciech Różowski 2026-05-14 12:56:22 +01:00
  • 48729abf4a
    feat: better error messages and more complete logic for checkImpossibleInstance and checkNonClassInstance (#13550) MoritzBeroRoos 2026-05-14 11:40:03 +02:00
  • 80a85cd3d9
    fix: respect fixed-parameter permutation when reporting structural recursion failures (#13730) Joachim Breitner 2026-05-14 10:17:13 +02:00
  • 803553a556
    feat: additional fieldinfo in structure instance notation (#13728) Kyle Miller 2026-05-13 17:11:05 -07:00
  • bba3868b3b
    fix: omit empty moreLeancArgs when leanc flags are unset (#13723) pandaman 2026-05-13 23:00:35 +09:00
  • 6279ae98c7
    test: resurrect try cancellation tests (#13707) Joachim Breitner 2026-05-13 15:54:48 +02:00
  • 793cd14b38
    feat: improve message of unusedVariables linter (#13715) Wojciech Różowski 2026-05-13 10:40:18 +01:00
  • ed0d50fcf0
    fix: timing issues and race conditions in ContextAsync.race (#13718) Sofia Rodrigues 2026-05-12 22:25:01 -03:00
  • cc103d8ed6
    chore: remove worker_crash test (#13720) Joachim Breitner 2026-05-13 00:21:11 +02:00
  • 7a6c59a357
    fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) Joachim Breitner 2026-05-12 22:53:17 +02:00
  • d33a771ea3
    test: always clean full .lake (#13703) Sebastian Ullrich 2026-05-12 18:25:00 +02:00
  • 8c82f9ed4a
    feat: add Locale and LocaleSymbols for configurable date/time formatting (#13567) Sofia Rodrigues 2026-05-12 10:21:25 -03:00
  • c04a83a2e5
    refactor: turn dupNamespace into a Lean.Linter (#13708) Wojciech Różowski 2026-05-12 07:39:08 +01:00
  • ea73a5b508
    fix: prioritize TZ and TZDIR over /etc/localtime in TZDB search (#13565) Sofia Rodrigues 2026-05-11 21:51:48 -03:00
  • f67ea44b6a
    feat: add WallTime and simplify Timestamp API (#13675) Sofia Rodrigues 2026-05-11 20:26:19 -03:00
  • d055778913
    chore: delete flaky tests for now (#13711) Joachim Breitner 2026-05-11 21:31:54 +02:00
  • f52a18a947
    chore: re-enable Lake tests (#13692) Mac Malone 2026-05-11 10:56:40 -04:00
  • 48ad8401cd
    fix: do not modify infotrees in withSetOptionIn (#11313) Thomas R. Murrills 2026-05-11 07:36:39 -04:00
  • 0c4d2648b5
    test: harden cancellation_empty_by against scheduling races (#13704) Joachim Breitner 2026-05-11 12:34:38 +02:00
  • 139e6732bd
    chore: align cbv tactic with SymM framework conventions (#13682) Wojciech Różowski 2026-05-11 11:04:26 +01:00
  • 2229b077d6
    feat: empty by runs try? to suggest a proof (#13430) Joachim Breitner 2026-05-11 08:31:42 +02:00
  • d98f40cda2
    feat: add genLocal configuration option for grind (#13699) Leonardo de Moura 2026-05-10 20:23:00 -07:00
  • 2674a1307c
    feat: improve diagnostiscs for grind local theorems (#13698) Leonardo de Moura 2026-05-10 16:31:08 -07:00
  • 0eb80e34a6 chore: update stage0 Lean stage0 autoupdater 2026-05-10 18:39:36 +00:00
  • 62142c5a4a
    chore: add missing noexcepts (#13370) Eric Wieser 2026-05-10 10:58:04 -07:00
  • 654017fb3c
    feat: serve trace.profiler data via local HTTP server (#13530) Sebastian Ullrich 2026-05-10 19:55:25 +02:00
  • 805fbca948 chore: update stage0 Lean stage0 autoupdater 2026-05-10 17:22:00 +00:00
  • a71f158f7b
    fix: allow various Vector append lemmas to take vectors of different sizes (#13693) Kim Morrison 2026-05-10 14:36:32 +10:00
  • 1e367b550a
    chore: make Glob.ofString? public (#13563) Kim Morrison 2026-05-09 21:48:08 +10:00
  • 68764f5382
    doc: add CLAUDE.md guidance on rebasing vs changing PR base (#13652) Kim Morrison 2026-05-09 21:34:50 +10:00
  • 41ecccec6d
    feat: lake: hoist compiled configurations (#13683) Mac Malone 2026-05-08 14:00:37 -04:00
  • 819f4549d9
    chore: remove some more String.length calls (#13687) Julia Markus Himmel 2026-05-08 12:46:34 +02:00
  • 85d46c351f
    chore: pin test-summary action to v2.4 SHA to unblock CI (#13686) Kim Morrison 2026-05-08 20:38:53 +10:00
  • a416b90d22
    feat: remove redundant deprecation warnings (#13595) Wojciech Różowski 2026-05-07 16:43:34 +01:00
  • 79659457fb
    chore: reduce usage of String.length (#13681) Julia Markus Himmel 2026-05-07 16:27:06 +02:00
  • 422920f643
    feat: mvcgen', an experimental SymM-based implementation mvcgen (#13644) Sebastian Graf 2026-05-07 14:53:02 +02:00
  • 049b7ebee2
    feat: verifiable repeat/while loops (#13209) Sebastian Graf 2026-05-07 14:48:42 +02:00
  • 9151360469
    fix: preserve symbol hover for fun_induction function target (#13678) Joachim Breitner 2026-05-07 14:09:36 +02:00
  • 443615f27e
    test: remove printDecls test (#13677) Sebastian Ullrich 2026-05-07 13:18:33 +02:00
  • c17c4598bc
    chore: refactor the usages of Meta.mkCongrArg with SymM primitives in cbv (#13665) Wojciech Różowski 2026-05-07 11:31:48 +01:00
  • 355dca6f57
    perf: optimize lean_dec_ref_cold (#13669) Henrik Böving 2026-05-07 10:18:39 +02:00
  • 5d5642107d
    fix: elaborate and render blockquotes in Verso docstrings (#13670) David Thrane Christiansen 2026-05-07 01:59:11 +02:00
  • 36a54dbe9c
    test: mvcgen' with grind should fail when grind fails (#13672) Sebastian Graf 2026-05-06 23:41:38 +02:00
  • a81628ddbf
    test: add BackwardRule.applyChecked debug wrapper for mvcgen' (#13671) Sebastian Graf 2026-05-06 23:33:27 +02:00
  • 0c6785c68f
    test: simplify cancellation_par test infrastructure (#13663) Joachim Breitner 2026-05-06 21:10:35 +02:00
  • d34811b5c9
    test: tidy Util.lean in the mvcgen' prototype (#13667) Sebastian Graf 2026-05-06 20:00:25 +02:00
  • 65906d9ccc
    test: unfold reducible abbreviations in inline-elaborated invariant values (#13668) Sebastian Graf 2026-05-06 19:58:03 +02:00
  • 22abf93a59
    chore: CLAUDE.md: test moddocs (#13662) Sebastian Ullrich 2026-05-06 16:03:06 +02:00
  • 036bd4f0df
    fix: withoutExporting around diagnostic reporting (#13630) Kim Morrison 2026-05-06 23:47:26 +10:00