rlean-search 0.2.3

= The rlean-search manual
Nikolaos Chatzikonstantinou <nchatz314@gmail.com>
0.2.3
:reproducible:
:source-highlighter: pygments
:toc:

== Introduction

The `rlean-search` utility is a humble search utility for Lean 4. Its
search functionality is not as good as
https://loogle.lean-lang.org/[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
https://loogle.lean-lang.org/[loogle] for those.

The project repository is
https://github.com/createyourpersonalaccount/rlean-search[here]. The
manual may be viewed online
https://createyourpersonalaccount.github.io/rlean-search[here].

== Installation

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

[,sh]
----
cargo install rlean-search
----

== Usage

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

1. Navigate to the Mathlib project root, for example
   `mathlib4-4.32.2/Mathlib`.
2. Execute `rlean-search daemon .`.
3. 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)_.
4. The server is now running on `127.0.0.1` on port `7878`.
5. Query the server using `rlean-search query -p '_ + _ = 0'`.
6. The response will be in JSON, and _*blazing fast*_!

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

=== Search

[#build-index]
==== Build the index

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

[,sh]
----
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:

[,sh]
----
rlean-search search -p /path/to/mathlib4 '_ + _ = 0'
----

The search mechanism supports:

1. Holes with `_`.
2. Metavariables with `?a`.
3. Searching the conclusion with `|- tsum _ = _ * tsum _`.

=== Fast search with the daemon

==== Launch the daemon

Build the link:#build-index[index] and then run the daemon server:

[,sh]
----
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:

[,sh]
----
rlean-search query -p '_ + _ = 0' | jq
----

You will get the results back *instantly!* (We pipe the result to
https://jqlang.org/[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:

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

===== Example query with JSON

Send the following query:

[,json]
----
{ "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:

[,json]
----
{"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 link:#build-index[index].

===== Example query with XML

Send the following query:

[,xml]
----
<rlean:search xmlns:rlean="http://github.com/createyourpersonalaccount/rlean-search" pattern="_ + _ = 0" limit="50"/>
----

IMPORTANT: The XML query must be in a single line.

The response will be a multi-line response in XML.

=== Command-line options

`rlean-search` follows the command interface that `git`
popularized. It has the following commands:

- `index`
- `search`
- `daemon`
- `query`

Use with `--help` to learn more information about each command, for
instance `rlean-search index --help`.