This PR threads `BaseIO` through `getModuleIREntries` and the interpreter/codegen lookups that consume imported IR, in preparation for loading imported IR on demand. There is no behavior change yet: the lookups still read the eagerly-imported state.
`getModuleIREntries`, `findInterpDecl`/`findInterpDeclBoxed`, `findEnvDecl`/`findEnvDecl'`, `getSorryDep`, and `getRegularInitAttrModIdxs` become `BaseIO`; `findExtEntry?` is split so the non-IR LCNF lookups stay pure and a new `findIRExtEntry?` carries the IR branch. The C-export ABI is unchanged: `BaseIO` compiles to a bare value-return (no world argument, no error wrapper), so `ir_interpreter.cpp` needs no changes.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

This PR makes `[inherit_doc]` copy the resolved docstring when a public declaration inherits one from a private declaration, instead of storing an alias to the private name. An importer cannot resolve such an alias because the private target is not exported and has no module index, so the inherited docstring would be lost across modules. Since the source is available where the attribute is applied, its docstring is copied eagerly; all other cases keep the existing alias behavior.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

This PR loads a module's interpreter IR (`.ir`) lazily, on first use, instead of eagerly populating the IR extension state for every imported module at import time. Modules whose interpreter IR is already part of the imported `.olean` data are read as before; module-system modules with a separate `.ir` are memory-mapped and cached on first access.
`Kernel.Environment`'s `irBaseExts : Array EnvExtensionState` field becomes `irData : Option LazyIR`, holding the per-module `.ir` paths and a mutable `IO.Ref` cache populated via `modifyGet`. `getModuleIREntries` becomes `BaseIO`; the C-export ABI is unchanged because `BaseIO` compiles to a bare value return. A lazy index maps code-generator auxiliary constants discovered while loading `.ir` files, consulted by the interpreter and codegen lookups when `getModuleIdxFor?` misses. `const2ModIdx` auxiliaries are sourced from the already-loaded `.olean` data.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Reconcile the lazy interpreter-IR loading work with master's multi-part IR refactor (`irParts` = `.ir.sig` + `.ir`).
Master split a module's interpreter IR into chained compacted regions (the `.ir` is compacted relative to the `.ir.sig` region), while this branch made that IR load lazily. The two are reconciled with a per-module `Kernel.IRSource` (`loaded` / `deferred` / `absent`):
* `deferred` modules store their IR part paths and load them on demand via `readModuleDataParts` (the same region chaining as the eager path), caching the full `.ir` and keeping every part region alive. Reading the `.ir` on its own left its cross-region pointers into the `.ir.sig` region dangling, segfaulting the interpreter on first use.
* The lazy cache `IO.Ref` is swapped for a fresh, non-persistent one after each `markPersistent` (in both `base.private` and `checked`), mirroring `realizeMapRef`, so the persistent environment never freezes a mutable cell.
* Eagerly-loaded (`import all`, IR-only, leanir) modules source their `const2ModIdx` code-generator auxiliaries from the `.ir` (the full set, including private ones, as before the lazy change); deferred modules register theirs in `extraIdx` when their `.ir` is loaded on demand.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

...table
This PR lets the interpreter load a module's IR on demand even when it references code-generator auxiliaries or private symbols defined in another module, by recording in each `.ir` the defining module of every such symbol its code references.
When the interpreter runs an imported module's IR and calls a symbol that is not a kernel constant (a specialization, a private initializer, a boxed wrapper), `const2ModIdx` cannot locate it and the defining module may never have been loaded, so the lookup fails with `(interpreter) unknown declaration`. Each `.ir` now ships a referenced-symbol → defining-module side table, computed at code-generation time when `const2ModIdx` is complete; loading a `.ir` merges it into the on-demand index, so the referenced module's `.ir` is loaded when the symbol is first called. Only the interpreter needs this: code generation, the IR checker, and `getSorryDep` only reference kernel constants or current-module declarations, which are already in `const2ModIdx`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

...declaration lookup
This PR removes the `lazyIRModuleIdxFor?` fallback from `findIRExtEntry?`, the lookup behind code generation's `findEnvDecl`. Code generation only references kernel constants (which are in `const2ModIdx`) and current-module declarations, so it never reaches the on-demand auxiliary index; only the interpreter does, and it keeps its own fallback.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

This PR removes the `ModuleData.extraConstNames` field and fills `const2ModIdx`'s code-generator auxiliaries at import time from each module's already-loaded `declMapExt` and `monoExt` entries instead, dropping a duplicated copy of those names from the olean.
For eagerly-loaded IR (`import all`, leanir, IR-only modules) the auxiliaries come from the full `.ir` `declMapExt`; for a deferred module they come from the `.olean`'s `declMapExt` (public IR and boxed externs) together with `monoExt`'s private specializations, which `monoExt` keeps in `.olean.private` so that inlineable bodies referencing them stay resolvable. Remaining private auxiliaries register in `extraIdx` when the module's `.ir` is loaded on demand. The extraction runs in the compiler layer via `extractIRConstNames` and `extractMonoConstNames` so `finalizeImport` need not see the IR declaration types.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>