This PR replaces the per-level `OLeanLevel → Array α` return type of
`exportEntriesFnEx` with a new `OLeanEntries (Array α)` structure that
bundles exported, server, and private entries together. This allows
extensions to share expensive computation across all three olean levels
instead of being called three separate times.
A new `computeExtEntries` function in `Environment.lean` calls each
extension's export function once and distributes results across levels.
`mkModuleData` accepts optional pre-computed entries, and `writeModule`
uses `computeExtEntries` to compute once for all three olean parts.
Extensions that previously relied on `env.setExporting` being
pre-applied by `mkModuleData` now call `env.setExporting true`
internally for their exported/server-level filtering, since the export
function is called once rather than per-level.
Extracted from #13117 to be reviewed independently.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
439c3c5544