rlean-search

Type-aware search over Lean 4 theorem, lemma, and axiom declarations.

Parses .lean sources (not .olean), understands Lake package layout, writes XML indexes under the schema namespace

http://github.com/createyourpersonalaccount/rlean-search

and answers patterns such as:

Pattern	Meaning
`_ + _ = 0`	holes match any subexpression
`?a - ?a = 0`	named holes must unify to the same term
`\|- tsum _ = _ * tsum _`	match only the main conclusion

Build

cargo build --release

Index

rlean-search index path/to/Mathlib path/to/lean4/src \
  -o .rlean-search/index.xml.gz

The default cache is a gzipped XML file (index.xml.gz) written with the fastest gzip compression level for quick index dumps.

Lake-aware discovery reads lakefile.toml / lakefile.lean, srcDir, and lean_lib roots, then walks .lean files (skipping .lake, build, etc.).

One-shot search (uses cache when present)

rlean-search search '_ + _ = 0' -p path/to/pkg
rlean-search search '?a - ?a = 0' -p path/to/pkg --format jsonl
rlean-search search '|- _ * 1 = _' -p path/to/pkg --format xml

Daemon mode (Tokio, multi-client)

Keeps the full type index in memory for low-latency queries:

rlean-search daemon --bind 127.0.0.1:7878 path/to/pkg

Clients speak JSONL or XML; the response format matches the request:

# JSONL
echo '{"cmd":"search","pattern":"_ + 0 = _","limit":20}' | nc 127.0.0.1 7878

# XML
echo '<rlean:search xmlns:rlean="http://github.com/createyourpersonalaccount/rlean-search" pattern="?a - ?a = 0" limit="20"/>' \
  | nc 127.0.0.1 7878

rlean-search query --pattern '_ + 0 = _'
rlean-search query --xml --pattern '|- _ = 0'

Commands: search, stats, reload, ping.

XML schema

See schema/rlean-search.xsd. Index documents look like:

<rlean:index xmlns:rlean="http://github.com/createyourpersonalaccount/rlean-search" ...>
  <rlean:package name="mathlib" root="...">...</rlean:package>
  <rlean:declaration kind="theorem" name="add_comm" full_name="Nat.add_comm" ...>
    <rlean:typeSurface>∀ (n m : Nat), n + m = m + n</rlean:typeSurface>
    <rlean:type>...</rlean:type>
    <rlean:conclusion head="op:=">...</rlean:conclusion>
  </rlean:declaration>
</rlean:index>

Tests

Fixtures under tests/fixtures/ are derived from Lean 4 / Mathlib 4 type shapes (from the accompanying lean4-v4.32.2 / mathlib4-v4.32.2 sources):

cargo test

Coverage notes

The type parser targets a useful fragment of Lean surface types: binders, arrows/Pi, applications, common infix operators (+, *, =, ≤, ∧, ↔, …), quantifiers, sorts, and search holes. Extremely advanced syntax may be stored as raw nodes so declarations remain searchable by surface text and structure where parsed.

rlean-search 0.2.0