rlean-search 0.2.2

Type-aware search over Lean 4 theorems, lemmas, and axioms
Documentation

= The rlean-search manual Nikolaos Chatzikonstantinou nchatz314@gmail.com 0.2.2 :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].

== 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

=== 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.