The rlean-search manual

Introduction

The rlean-search utility is a humble search utility for Lean 4. Its search functionality is not as good as loogle, but it is much faster. It was vibe-coded with Grok Build.

rlean-search parses the source code of the Lean 4 projects and produces a cache file that it then loads into memory and runs queries on. It will probably miss very complicated types; use loogle for those.

The project repository is here. The manual may be viewed online here.

Installation

rlean-search is written in Rust and uses the Cargo build system. You can install it for your local user with:

cargo install rlean-search

Usage

The typical usage is to search Mathlib. The steps are:

Navigate to the Mathlib project root, for example mathlib4-4.32.2/Mathlib.
Execute rlean-search daemon ..
The first time, this command will take a while as it builds the index. Eventually it will print INFO rlean_search::daemon: indexed 181543 declarations from 1 package(s).
The server is now running on 127.0.0.1 on port 7878.
Query the server using rlean-search query -p '_ + _ = 0'.
The response will be in JSON, and *blazing fast*!

If you want to learn a bit more about rlean-search, read on!

Search

Build the index

First you must build the index file. For Mathlib, you could do:

rlean-search index /path/to/mathlib4

This creates a cached index file named index.xml.gz under /path/to/mathlib4/.rlean-search/.
The index file will be created automatically if you attempt to search without running the above command first.
The indexing command is a slow operation, but it only needs to be run once.

Perform a search

Now you can search Mathlib using:

rlean-search search -p /path/to/mathlib4 '_ + _ = 0'

The search mechanism supports:

Holes with _.
Metavariables with ?a.
Searching the conclusion with |- tsum _ = _ * tsum _.

Fast search with the daemon

Launch the daemon

Build the index and then run the daemon server:

rlean-search daemon /path/to/mathlib4

Note	The daemon startup will be a little slow, even if the index has been built.

The daemon by default runs on 127.0.0.1:7878. Now clients can communicate with the daemon using either JSON or XML queries.

Query with `rlean-search`

The rlean-search utility provides a client:

rlean-search query -p '_ + _ = 0' | jq

You will get the results back instantly! (We pipe the result to jq for neat viewing.)

Query with a script

If you wish to query the daemon from your own script without invoking rlean-search, follow the steps:

Establish a connection to 127.0.0.1:7878.
Send queries either in JSON or XML.
Read the responses.

Example query with JSON

Send the following query:

{ "cmd": "search", "limit": 2, "pattern": "_ + _ = 0" }

Important

The JSON query must be in a single line. NOTE: For this example we limit the results to only 2.

The response will be a single line like this:

{"type":"search","pattern":"_ + _ = 0","count":2,"hits":[{"name":"Odd","full_name":"Odd","kind":"lemma","type_surface":"a ^ n + b ^ n = 0","file":"/home/grok/mathlib4/Mathlib/Algebra/Ring/Parity.lean","line":153,"score":149},{"name":"term","full_name":"term","kind":"axiom","type_surface":"∀ a b : ℚ, a + b = 0","file":"/home/grok/mathlib4/MathlibTest/Tactic/Grind/Grobner.lean","line":70,"score":147}]}

Note	The above command returned a result from Mathlib’s test suite! You can perform subsequent filtering yourself on the result of the query, or you can delete the test suite from the Mathlib directory prior to building the index.

Example query with XML