v0.1.0
Initial release of the shared semantic-search package for Lean tooling.
Added
lean-semantic-search-contract: stable serde DTOs, opaque keys, diagnostics, version constants, and
response envelopes — the cross-repository JSON contract.lean-semantic-search-capability: worker-facing command names, export names, advertised facts, and
empty-diagnostic helpers.lean-semantic-search-retrieval: storage-neutral semantic candidate generation over feature rows,
carrying its ownRETRIEVAL_POLICY_VERSION.- Lean feature-extraction package (
lean/LeanSemanticSearch): canonical traversal, role features, module
and declaration extraction, proof-goal features, JSON envelopes, and the five@[export]capability
entry points.