[kmehltretter82]

This PR interns RefInfo.Location.parentDecl strings across a module when decoding ModuleRefs (and standalone RefInfo) from JSON, so that locations sharing the same enclosing declaration within a loaded .ilean module retain a single shared String allocation after the intermediate Json value is released. It also reuses the already computed parentDeclNameString? in RefInfo.toLspRefInfo instead of converting parentDeclName? to a String twice.

Closes #16100.

Benchmarks

Measured on native compiled code (lean -c + leanc -O3, average of 20 runs) across Json.parse followed by FromJson ModuleRefs after releasing the intermediate Json value:

Workload	Locations	Distinct parentDecls	Retained parentDecl Strings (Before → After)	Retained parentDecl Bytes (Before → After)	fromJson? avg (Before → After)	Json.parse + fromJson? avg (Before → After)
Representative (400 idents × 25 usages, ~808 KB JSON)	10,400	50	10,400 → 50	892,320 B → 4,290 B (-99.5%)	2.41 ms → 2.95 ms	9.95 ms → 10.47 ms
High sharing (100 idents × 200 usages, ~1.43 MB JSON)	20,100	10	20,100 → 10	1,708,500 B → 850 B (-99.95%)	4.32 ms → 5.15 ms	19.63 ms → 19.25 ms
All distinct (400 idents × 25 usages, ~830 KB JSON)	10,400	10,400	10,400 → 10,400	914,490 B → 914,490 B (0%)	3.44 ms → 5.06 ms	12.43 ms → 14.87 ms

[github-actions]

Thank you for your interest in contributing to Lean!

This repository currently only accepts pull requests from regular contributors, primarily from the Lean FRO, so this PR has been closed automatically.

If you have found a bug or want to propose a change, please open an issue describing it instead; see also our contribution guidelines. A maintainer may reopen this PR if appropriate.