Commit graph

Select branches

Hide pull requests

master

Mono Color

• 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