DOCSEARCHbyAlgolia
Submit Docs

Loogle Search Tool

repository·master·Indexed 41 days ago

https://github.com/nomeata/loogle

A search engine for Lean and Mathlib declarations that supports pattern matching, constant search, and subexpression queries. Available as a CLI tool, web service with a JSON API, Zulip bot, and integrations for VS Code and Neovim.

Tokens
2.8K
Snippets
6
Records
13
Agent score
99%

What's inside Loogle

  1. Search Lean and Mathlib with Loogle

    master
    Loogle is a search engine for Lean and Mathlib definitions and theorems. It can be accessed via the web service, the CLI, the Zulip bot, or integrated into editors like VS Code (via the Loogle command or the Loogle VS Code extension), Neovim (lean.nvim), and LeanSearchClient.

  2. Use loogle in Zulip chat

    master

    The Leanprover Zulip chat includes a loogle bot. To use it, mention the bot in a public stream followed by your query:

    @**loogle** query

    The bot will respond with the first two hits from the loogle search engine.

  4. Run the loogle web service locally

    master

    The loogle web service can be run locally using the provided server.py wrapper. The wrapper must be executed from within the loogle repository directory.

    To run the server, pass the directory of the project you wish to search via --project-dir. Any arguments following -- are forwarded directly to the loogle binary.

    Example:

    ./server.py --project-dir /path/to/project -- --module RootModule

    Supported Wrapper Arguments:

    • --host
    • --port
    • --loogle-bin
    • --project-dir

    API Endpoint:

    • Results can be retrieved in JSON format by accessing /json?q=... (instead of the standard /?q=... web interface). Note that the JSON format stability is not guaranteed.
    ./server.py --project-dir /path/to/project -- --module RootModule

  5. Search Loogle by constant, name, or subexpression

    master

    Loogle supports several search modes to find definitions and lemmas:

    • By constant: Search for a specific constant to find all lemmas mentioning it. Example: Real.sin finds lemmas mentioning the sine function.
    • By lemma name substring: Search for a substring within the lemma's name. Use quotes for the substring. Example: "differ" finds lemmas with "differ" in their name.
    • By subexpression: Search for lemmas containing a specific pattern or shape.
      • Linear patterns: _ * (_ ^ _) finds products where the second argument is raised to a power.
      • Non-linear patterns with parameters: Use ?a, ?b, etc., to match terms. Parameters are matched in any order. Example: (?a -> ?b) -> List ?a -> List ?b will match List ?a -> (?a -> ?b) -> List ?b.
    • By main conclusion: Use the |- prefix to search for lemmas where the conclusion (the part to the right of all → and ∀) matches a specific shape. Example: |- tsum _ = _ * tsum _.
    🔍 Real.sin
🔍 "differ"
🔍 _ * (_ ^ _)
🔍 Real.sqrt ?a * Real.sqrt ?a
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 |- tsum _ = _ * tsum _

  6. Run loogle locally for a Lake project

    master

    To use the loogle binary to search a specific Lake project, the binary must be built with the same Lean toolchain as the target project. Follow these steps:

    1. Clone the loogle repository and enter the directory.
    2. Copy the target project's lean-toolchain into the loogle directory to ensure toolchain parity:
      cp /path/to/project/lean-toolchain .
    3. Build loogle using lake:
      lake build
    4. Execute the binary from within your target project using lake env, pointing it to the built loogle binary and specifying the module to search:
      lake env /path/to/loogle/.lake/build/bin/loogle --module MyModule "<query>"

    Indexing Behavior:

    • The first call builds a search index (this is slow).
    • By default, loogle caches the index on disk next to the module's .olean file. Subsequent calls are fast and the index is automatically rebuilt if .olean files change.
    • If the default location is read-only, use --index-file PATH to specify a writable location.
    • To skip caching entirely, use --index-mode none.
    cp /path/to/project/lean-toolchain .
lake build
lake env /path/to/loogle/.lake/build/bin/loogle --module MyModule "<query>"

  7. Filter Loogle results by definition or theorem type

    master

    You can refine your search by specifying whether you are looking for definitions (data) or theorems (propositions):

    • Definitions (Data): Use ⊢ (_ : Type _).
    • Theorems (Propositions): Use ⊢ (_ : Prop).

    Combining Filters: You can pass multiple filters separated by commas to perform an AND search. Each filter's metavariables (?a) are assigned independently.

    Example of a complex combined search: Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ This finds lemmas that mention Real.sin AND tsum, have "two" in the name, include a product and a power, AND have a hypothesis of the form _ < _.

    ⊢ (_ : Type _)
⊢ (_ : Prop)
Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _

  8. Run the Loogle HTTP server

    master

    The server.py script provides an HTTP frontend for the Loogle search tool. It manages a pool of loogle subprocesses (workers) to handle search queries. You can configure the server using several command-line arguments.

    To run the server with default settings (localhost:8088, 1 worker), use:

    python3 server.py

    To forward specific arguments to the underlying loogle binary, use the -- separator. For example, to pass --module and --max-results to the loogle subprocess:

    python3 server.py -- --module Init.Data.List.Basic --max-results 50
    python3 server.py

  9. CLI Reference for loogle

    master

    The loogle command-line tool allows searching Lean/Mathlib declarations.

    Usage: loogle [OPTIONS] [QUERY]

    Options:

    USAGE:      loogle [OPTIONS] [QUERY]

OPTIONS:
      --help
      --interactive, -i     read querys from stdin
      --json, -j            print result in JSON format
      --module mod          import this module (default: Mathlib)
      --path path           search for .olean files here (default: the build time path)
      --index-mode MODE     how to manage the on-disk search index. One of:
                              use   (default) load if present and up-to-date,
                                    otherwise build and write
                              read  load existing index; refuse to start if it
                                    is missing or out of date
                              write always (re)build the index and write it
                              none  build in memory and discard on exit
      --index-file PATH     override the default index path. The default lives
                            next to the root module's .olean (with .loogle-index
                            extension); pass this if that location is read-only.
      --max-results n       limit the number of returned hits (default: 200)

  10. Use the Loogle Zulip bot endpoint

    master

    The server supports a /zulipbot endpoint for integration with Zulip. This endpoint expects a POST request with a JSON body containing message data.

    Endpoint: POST /zulipbot Content-Type: application/json

    Request Body Example:

    {
  "data": "@**loogle** Real.sin"
}

    Behavior:

    • The bot parses the query from the data field, looking for the @**loogle** trigger.
    • It returns a JSON response containing a formatted content string suitable for Zulip, including markdown links to documentation or suggestions if the query was ambiguous.

  11. Use the Loogle JSON API

    master

    The Loogle server provides a JSON endpoint for programmatic access to search results. To use it, send a GET request to the /json path with a query parameter q.

    Endpoint: GET /json?q=<query>

    Example Request: GET /json?q=Real.sin

    Response Format: Returns a JSON object containing search results. If the server is overloaded, it returns an HTTP 503 with a JSON error message. If a worker crashes, it may return an error field in the JSON.

    Client Identification: To ensure proper metrics tracking, clients should identify themselves via the x-loogle-client header or the User-Agent header. Supported identifiers include:

    • vscode-lean4 (via x-loogle-client)
    • LeanSearchClient (via User-Agent)
    • vscode-loogle (via User-Agent)
    • nvim (via User-Agent)
    • lean-lsp-mcp (via User-Agent)
    • meta-agent (via User-Agent)
    • AutoLeanPaper (via User-Agent)
    • zulip (via POST to /zulipbot)
    • json (default for other programmatic clients)

  12. Monitor Loogle via Prometheus metrics

    master

    If the prometheus_client package is installed, the server exposes a /metrics endpoint for monitoring.

    Key Metrics:

    • versions: Info about Lean and mathlib versions.
    • queries: Total number of queries.
    • errors_backend: Queries failed because the backend crashed or timed out.
    • errors_loogle: Queries where loogle itself returned an error response.
    • errors_denylist: Requests rejected by the user-agent denylist.
    • load_shed: Requests rejected because all workers were busy.
    • restarts: Backend worker restarts (labeled by reason: sandbox, died, or unresponsive).
    • workers_lost: Workers permanently removed from the pool after a failed restart.
    • results: Histogram of results per query.
    • heartbeats: Histogram of heartbeats per query.
    • clients: Counter of clients used (labeled by client type).
    • workers_available: Gauge of workers currently in the pool ready to serve requests.