Henrik Böving 795edcf8ad perf: reduce allocations in Json.compress (#5222) ... 1. Remove the need to allocate an intermediate `String` for literally every character in a JSON `String`. 2. Use a single `String` buffer in the entire `Json.compress` machinery. 3. Use `toListAppend` Number 1 is doing most of the lifting in the perf diff, the rest are some minor but measurable improvements.		2024-09-04 19:52:10 +00:00
..
Compiler	chore: remove LEAN_EXPORT denylist workaround	2024-08-12 14:14:42 +02:00
Data	perf: reduce allocations in Json.compress (#5222)	2024-09-04 19:52:10 +00:00
DocString	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Elab	refactor: make extractLsb' the primitive bv_decide understands, rather than extractLsb (#5211)	2024-09-04 08:02:04 +00:00
Language	chore: remove stray markPersistent (#5056)	2024-08-15 15:41:42 +00:00
Linter	feat: improve unused section variable warning (#5036)	2024-08-22 10:18:09 +00:00
Meta	refactor: rfl tactic: do not use Kernel.isDefEq (#3772)	2024-09-03 19:51:14 +00:00
Parser	doc: include: currently applies to theorems only (#5206)	2024-08-30 12:51:50 +00:00
ParserCompiler	feat: reserved names (#3675)	2024-03-15 00:33:22 +00:00
PrettyPrinter	fix: check is valid structure projection when pretty printing (#4982)	2024-08-12 15:52:17 +00:00
Server	fix: include identifier before cursor in document highlight request (#5237)	2024-09-04 08:05:54 +00:00
Util	chore: don't use simp_arith when simp will do (#5256)	2024-09-04 07:56:25 +00:00
Widget	chore: remove >6 month deprecations (#5199)	2024-08-29 05:18:44 +00:00
AddDecl.lean	fix: adapt kernel interruption to new cancellation system (#4584)	2024-07-01 14:52:42 +00:00
Attributes.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
AuxRecursor.lean	refactor: IndGroupInst.brecOn (#4787)	2024-07-19 10:20:50 +00:00
BuiltinDocAttr.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Class.lean
Compiler.lean
CoreM.lean	chore: shorten suggestion about diagnostics (#4882)	2024-07-31 17:56:43 +00:00
Data.lean	chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115)	2024-08-21 15:26:17 +00:00
Declaration.lean	refactor: use indVal.numNested or indVal.numTypeFormers where applicable (#4734)	2024-07-12 22:07:25 +00:00
DeclarationRange.lean	feat: snapshot trees and language processors (#3014)	2024-03-14 13:40:08 +00:00
DocString.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Elab.lean	chore: upstream #time command (#5044)	2024-08-15 00:17:48 +00:00
Environment.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
Eval.lean
Exception.lean	chore: cleanup unused arguments (from linter) (#4621)	2024-07-07 21:20:06 +00:00
Expr.lean	chore: use Expr.numObjs instead of lean_expr_size_shared (#5239)	2024-09-02 21:26:00 +00:00
HeadIndex.lean	chore: fix linter errors (#4502)	2024-06-19 18:24:08 +00:00
Hygiene.lean	chore: remove the coercion from String to Name (#3589)	2024-03-21 23:46:03 +00:00
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean	fix: handle AttributeKinds in LabelAttributes correctly (#3698)	2024-08-29 17:57:14 +02:00
LazyInitExtension.lean
Level.lean	chore: deprecate Lean.HashMap and Lean.HashSet (#4954)	2024-08-08 12:46:10 +00:00
Linter.lean	feat: omit (#5000)	2024-08-21 13:22:34 +00:00
LoadDynlib.lean
LocalContext.lean
Log.lean
Message.lean	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00
Meta.lean	feat: improve set_option diagnostics true (#4031)	2024-04-30 05:07:03 +00:00
MetavarContext.lean	perf: maximize term sharing at instantiateMVarDeclMVars (#5226)	2024-09-01 23:00:48 +00:00
Modifiers.lean	refactor: constructions: modify environment in lean world (#4474)	2024-06-19 08:58:53 +00:00
MonadEnv.lean	refactor: use indVal.numNested or indVal.numTypeFormers where applicable (#4734)	2024-07-12 22:07:25 +00:00
Parser.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
ParserCompiler.lean	refactor: Offset.lean and related files (#3614)	2024-03-05 19:40:15 -08:00
PrettyPrinter.lean	chore: use Expr.numObjs instead of lean_expr_size_shared (#5239)	2024-09-02 21:26:00 +00:00
ProjFns.lean
ReducibilityAttrs.lean	chore: fix linter errors (#4502)	2024-06-19 18:24:08 +00:00
Replay.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
ReservedNameAction.lean	fix: FunInd: support structural recursion on reflexive types (#4327)	2024-06-05 07:54:48 +00:00
ResolveName.lean	chore: cleanup unused arguments (from linter) (#4621)	2024-07-07 21:20:06 +00:00
Runtime.lean	feat: link LibUV (#4963)	2024-08-12 12:33:24 +00:00
ScopedEnvExtension.lean	feat: flexible reducibility attributes	2024-04-29 05:46:11 +02:00
Server.lean
Structure.lean
SubExpr.lean	fix: use correct expr positions when delaborating match patterns (#4034)	2024-05-01 12:02:10 +00:00
Syntax.lean	refactor: move Synax.hasIdent, shake dependencies (#4766)	2024-07-16 21:19:26 +00:00
ToExpr.lean	chore: upstream ToExpr FilePath and compile_time_search_path% (#4453)	2024-07-08 15:41:03 +00:00
Util.lean	feat: theorem diagnostics (#4924)	2024-08-06 01:01:28 +00:00
Widget.lean