Cameron Zwarich f5e72d0962 feat: make guard_msgs.diff=true the default (#8596) ... This PR makes `guard_msgs.diff=true` the default. The main usage of `#guard_msgs` is for writing tests, and this makes staring at altered test outputs considerably less tiring.		2025-06-03 15:13:15 +00:00
..
Compiler	fix: support compiler.extract_closed option in the new compiler (#8604)	2025-06-03 05:58:32 +00:00
Data	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
DocString	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
Elab	feat: make guard_msgs.diff=true the default (#8596)	2025-06-03 15:13:15 +00:00
Language	fix: SnapshotTree.waitAll (#8532)	2025-05-29 20:12:23 +00:00
Linter	feat: := private instance syntax	2025-05-28 10:18:04 +02:00
Meta	feat: create private aux decls in private contexts	2025-06-03 15:53:05 +02:00
Parser	feat: do not export private declarations (#8337)	2025-06-02 08:01:08 +00:00
ParserCompiler
PrettyPrinter	feat: use dot notation for class parent projections (#8504)	2025-05-28 20:34:40 +00:00
Server	feat: reusable rpc refs (#8105)	2025-06-03 12:35:12 +00:00
Util	fix: improve error-message hint rendering and API (#8486)	2025-06-01 01:22:09 +00:00
Widget	feat: reusable rpc refs (#8105)	2025-06-03 12:35:12 +00:00
AddDecl.lean	feat: do not export private declarations (#8337)	2025-06-02 08:01:08 +00:00
Attributes.lean	feat: realizeConst for match equations (#7247)	2025-03-03 17:18:29 +00:00
AuxRecursor.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
BuiltinDocAttr.lean
Class.lean
Compiler.lean
CoreM.lean	feat: create private aux decls in private contexts	2025-06-03 15:53:05 +02:00
Data.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Declaration.lean	feat: do not export theorem bodies (#8090)	2025-04-25 20:22:32 +00:00
DeclarationRange.lean	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
DocString.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Elab.lean
EnvExtension.lean	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
Environment.lean	feat: do not export private declarations (#8337)	2025-06-02 08:01:08 +00:00
Exception.lean	fix: unknown identifier ranges (#8362)	2025-05-22 10:05:31 +00:00
Expr.lean	fix: block potential adversarial exploit of non-aborting assert! (#8560)	2025-05-31 03:14:01 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	fix: block adversarial exploit of non-aborting assert! (#8559)	2025-05-31 00:08:30 +00:00
Linter.lean	feat: implement "linter sets" that can be turned on as a group (#8106)	2025-05-14 23:30:42 +00:00
LoadDynlib.lean	feat: smarter plugin loading (#7090)	2025-02-18 23:03:52 +00:00
LocalContext.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Log.lean	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
Message.lean	fix: improve error-message hint rendering and API (#8486)	2025-06-01 01:22:09 +00:00
Meta.lean	feat: add labeled subcomponents and helper functions for error messages (#8225)	2025-05-07 21:15:27 +00:00
MetavarContext.lean	doc: fix typo in MetavarDecl docstring (#8069)	2025-04-23 22:00:13 +00:00
Modifiers.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
MonadEnv.lean	feat: revamp aux decl name generation (#8363)	2025-05-16 14:57:18 +00:00
Namespace.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
Parser.lean
ParserCompiler.lean
PremiseSelection.lean
PrettyPrinter.lean	fix: don't reset localInstances in delaboration (#8022)	2025-04-19 15:39:16 +00:00
PrivateName.lean	chore: do not use the coercion α → Option α in Init and Std (#8085)	2025-04-24 13:35:01 +00:00
ProjFns.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
ReducibilityAttrs.lean	feat: add async support to more extensions and constructions (#7363)	2025-03-06 14:27:45 +00:00
Replay.lean	chore: Mathlib fixes (#7327)	2025-03-04 13:41:30 +00:00
ReservedNameAction.lean	feat: elaborate theorem bodies in parallel (#7084)	2025-03-14 07:50:42 +00:00
ResolveName.lean	fix: unknown identifier ranges (#8362)	2025-05-22 10:05:31 +00:00
Runtime.lean
ScopedEnvExtension.lean	feat: make more constructions async-compatible (#7384)	2025-03-10 09:56:30 +00:00
Server.lean	fix: do not cancel async elaboration tasks (#7175)	2025-02-21 17:24:36 +00:00
Setup.lean	chore: fix spelling mistakes (#8324)	2025-05-14 06:52:16 +00:00
Structure.lean	refactor: factor out common code for structure default values (#7737)	2025-03-31 22:40:39 +00:00
SubExpr.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Syntax.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
ToExpr.lean	feat: ToExpr IntX (#7268)	2025-02-28 09:32:30 +00:00
ToLevel.lean
Util.lean
Widget.lean