This PR re-enables `#print axioms` under the module system by computing
axiom dependencies at olean serialization time. It reverts #8174 and
replaces it with a proper fix.
Depends on #13142, which refactors `exportEntriesFnEx` to return all
three olean levels at once via a new `OLeanEntries` structure, allowing
extensions to share expensive computation.
The axiom extension uses `exportEntriesFnEx` to walk bodies of all
public declarations in the current module, collecting axiom dependencies
in a single batch with a shared cache across declarations. The results
are stored sorted for binary search and exported uniformly to all olean
levels. Downstream modules look up pre-computed axiom data from imported
oleans, so axiom collection never crosses module boundaries. During
elaboration of the current module, `collectAxioms` walks bodies directly
since they are always available locally.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
142ca24192