142ca24192
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>
1 line
30 B
Text
1 line
30 B
Text
../../../build/release/stage2
|