### Install Prometheus Client

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Install the prometheus_client Python package to enable the metrics endpoint. Restart the server after installation.

```bash
pip install prometheus_client
# Then restart the server
```

--------------------------------

### Install Prometheus Client

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Install the necessary Python package to enable Prometheus metrics for the Loogle server. Metrics will then be available at the /metrics endpoint.

```bash
pip install prometheus_client
```

--------------------------------

### Help Command Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Display the usage message for the Loogle CLI.

```bash
loogle --help
```

```bash
loogle
```

--------------------------------

### Example Usage of ConstMatcher

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Demonstrates how to use a ConstMatcher function after obtaining it, for example, from a pattern.

```lean
let matcher ← matchConclusion pat
let matched : Bool ← matcher someConstant
```

--------------------------------

### Server Binding Examples

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Configure the host and port for the HTTP server. Use '0.0.0.0' to listen on all available network interfaces.

```bash
# Local only (default)
./server.py
```

```bash
# Open to network
./server.py --host 0.0.0.0 --port 8080
```

```bash
# Specific interface
./server.py --host 192.168.1.100
```

--------------------------------

### Interactive Mode Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Start Loogle in interactive mode to process queries from standard input. Use --interactive and --json for JSON output.

```bash
loogle --interactive --json
```

--------------------------------

### Python HTTP Server Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/MANIFEST.txt

This snippet shows a basic structure for HTTP handlers in Python, including GET, POST, and OPTIONS methods. It's relevant for understanding the server's endpoint implementation.

```python
from flask import Flask, request, jsonify

app = Flask(__name__)

@app.route('/')
def index():
    return "Hello, Loogle!"

@app.route('/json', methods=['GET', 'OPTIONS'])
def json_data():
    if request.method == 'GET':
        return jsonify({"message": "This is JSON data"})
    else:
        return '', 204 # No Content for OPTIONS

@app.route('/zulipbot', methods=['POST'])
def zulip_bot():
    data = request.get_json()
    # Process Zulip bot data
    return jsonify({"status": "received", "data": data}), 200

@app.route('/metrics')
def metrics():
    # Return Prometheus metrics
    return "# HELP python_gc_collections_total Number of garbage collections."

@app.route('/loogle.png')
def loogle_png():
    # Serve Loogle PNG image
    with open('loogle.png', 'rb') as f:
        return f.read(), 200, {'Content-Type': 'image/png'}

@app.route('/loogle-banner.png')
def loogle_banner_png():
    # Serve Loogle banner PNG image
    with open('loogle-banner.png', 'rb') as f:
        return f.read(), 200, {'Content-Type': 'image/png'}

if __name__ == '__main__':
    app.run(debug=True)
```

--------------------------------

### Loogle Find Example Usage

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

An example demonstrating how to use the 'find' function with specific filters and how to handle the result, whether it's a success or an error.

```Lean
let filters := #[⟨Lean.mkIdent `List⟩, ⟨Syntax.mkStrLit "map"⟩]
let result ← find index filters 200
match result with
| .ok r => IO.println s!"{r.hits.size} results"
| .error err => IO.println s!"Error: {err.message}"
```

--------------------------------

### Example: Print Query Results

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

Shows how to execute a query using `runQuery` and then immediately print the formatted results to standard output using the `printPlain` function.

```lean
let (result, suggs, hb) ← runQuery index 200 "Real.sin"
← printPlain (result, suggs, hb)  -- Direct printing to stdout
```

--------------------------------

### Example: Run and Process Query

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

Demonstrates how to create a search index, run a query using `runQuery`, and then process the result, printing either the success message with count or an error message.

```lean
let index ← Find.Index.mk
let (result, suggs, hb) ← runQuery index 200 "List.map"
match result with
| .ok r => IO.println s!"{r.header}, found {r.count} total"
| .error err => IO.println s!"Error: {err.message}"
```

--------------------------------

### Loogle Binary Path Configuration Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Set a custom path to the Loogle executable. If not found, server startup will fail.

```bash
./server.py --loogle-bin /usr/local/bin/loogle
```

--------------------------------

### HTTP Server Usage

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Shows how to start the Loogle HTTP server with custom configurations and how to query it using curl.

```bash
./server.py --port 8088 -- --module Mathlib
```

```bash
./server.py --workers 4 --host 0.0.0.0 -- --module Mathlib
```

```bash
curl 'http://localhost:8088/json?q=List.map'
```

--------------------------------

### Loogle Class Start Method

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Starts the loogle subprocess and waits for a readiness signal. Returns `True` on success and `False` if the subprocess fails to start or times out.

```APIDOC
## Method: start

### Description
Start the loogle subprocess and wait for readiness signal.

### Return:
`True` if subprocess started and sent valid greeting within `startupTimeout`.
`False` if subprocess died, did not start, or timed out.

### Behavior:
1. Constructs command: `loogle --json --interactive [extra args]`
2. If `--project-dir` set, wraps: `lake -d <dir> env <command>`
3. Spawns subprocess with pipes for stdin/stdout
4. Waits for "Loogle is ready.\n" greeting with `startupTimeout` deadline
5. On timeout: kills process and returns `False`
6. On bad greeting: kills process and returns `False`

### Timeout:
Default 600s, configurable via `--startup-timeout` flag

### Error Logging:
Prints to stderr if greeting fails (e.g., "Backend did not send greeting within 600s.").

### Worker Pool Behavior:
Workers are only added to the pool after this returns `True`. Dead workers are never pooled.
```

--------------------------------

### Lean Source Code Example with Line References

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/MANIFEST.txt

This is an example of Lean source code, showing correct syntax with line references. It's representative of the core Loogle logic.

```lean
def runQuery (opts : LoogleOptions) (query : String) : IO (List String) := do
  -- Implementation details for running a query
  pure ["result1", "result2"] -- Placeholder result
#eval runQuery Loogle.defaultOptions "example query"
```

--------------------------------

### Production Server Setup

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Configure the server for production with high availability, multiple workers, and an explicit Mathlib version. Ensure the project directory is correctly set and use 'read' mode for the index.

```bash
# High availability, multiple workers, explicit Mathlib version
./server.py \
  --host 0.0.0.0 \
  --port 8080 \
  --workers 8 \
  --project-dir /var/lib/mathlib \
  -- --module Mathlib --index-mode read --max-results 100
```

--------------------------------

### GET /

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Handles GET requests to the root path, providing an HTML web form for queries. It processes 'q' and optional 'lucky' query parameters.

```APIDOC
## GET /

### Description
Handles GET requests to the root path, providing an HTML web form for queries. It processes 'q' and optional 'lucky' query parameters.

### Method
GET

### Endpoint
/

### Parameters
#### Query Parameters
- **q** (string) - Required - The search query.
- **lucky** (string) - Optional - If set to 'yes', redirects to the first result's documentation link.

### Request Example
GET /

### Response
#### Success Response (200)
- HTML content with a search form, results, and suggestions.

#### Response Example
(HTML content)

**CORS Headers:**
```
Access-Control-Allow-Origin: *
Access-Control-Allow-Headers: User-Agent, X-Loogle-Client
```
```

--------------------------------

### Example CLI Usage

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Illustrates common ways to invoke the loogle executable from the command line, including searching for an identifier, displaying help, and handling unknown identifiers.

```bash
$ loogle "List.map"
# Prints results, returns 0

$ loogle --help
# Prints usage, returns 0

$ loogle "unknown.identifier"
# Prints error to stderr, returns 1
```

--------------------------------

### Local Development Server Setup

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Run the server locally for development with a single worker and fast iteration. Use 'use' mode for quick checks and 'write' mode to force a rebuild after code changes.

```bash
# Local Mathlib search, single worker, fast iteration
./server.py --host localhost --port 8088 \
  -- --module Mathlib --index-mode use

# Later, after code changes:
./server.py --host localhost --port 8088 \
  -- --module Mathlib --index-mode write  # Force rebuild
```

--------------------------------

### Start Loogle Subprocess

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Starts the loogle subprocess and waits for a readiness signal. Returns `True` on success, `False` if the subprocess dies, fails to start, or times out. Configurable via `--startup-timeout`.

```python
def start(self) -> bool
```

--------------------------------

### Lean Type Signature Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/README.md

Demonstrates the syntax for Lean type signatures, including parameters and return types. This is used throughout the Lean source code.

```lean
def find (index : Index) (filters : Array Term) (maxShown := 200) :
    TermElabM (Except Failure Result)
```

--------------------------------

### Loogle CLI: Single Query Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

Example of invoking the Loogle command-line interface for a single search query.

```bash
loogle [OPTIONS] QUERY
```

--------------------------------

### Loogle CLI: Interactive Mode Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

Example of invoking the Loogle command-line interface in interactive mode, reading queries from standard input.

```bash
loogle --interactive [OPTIONS]
```

--------------------------------

### Prometheus Metrics Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Example output format for the Prometheus metrics endpoint. This includes various metrics like versions, query counts, errors, and results.

```text
# HELP versions Lean and mathlib versions
# TYPE versions gauge
versions_info{loogle="abc1234",project="Mathlib",project_rev="def5678"} 1.0

# HELP queries Total number of queries
# TYPE queries counter
queries_total 42.0

# HELP errors_backend Queries failed because the backend crashed or timed out
# TYPE errors_backend counter
errors_backend_total 2.0

# ... (more metrics)

# HELP results Results per query
# TYPE results histogram
results_bucket{le="0"} 5.0
results_bucket{le="1"} 10.0
results_bucket{le="2"} 20.0
... results_bucket{le="+Inf"} 42.0
results_sum 150.0
results_count 42.0

# ... (more histogram buckets)
```

--------------------------------

### Bash Command Line Usage Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/MANIFEST.txt

This example demonstrates how to use curl to interact with the Loogle HTTP API, specifically for sending a query and receiving JSON output. It's useful for testing and integration.

```bash
curl -X POST -d '{"query": "data structure"}' http://localhost:8000/query
```

--------------------------------

### Single Query Examples

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Execute a single search query directly from the command line. Options like --json, --module, and --max-results can refine the search.

```bash
loogle "List.map"
```

```bash
loogle --json --module Mathlib.Data.List "List.replicate"
```

```bash
loogle --module Init "Real.sin" --max-results 50
```

--------------------------------

### LoogleOptions Example Usage

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

Demonstrates how to instantiate and configure LoogleOptions for a specific search, setting the module, maximum results, JSON output, and requiring an existing index cache.

```lean
let opts : LoogleOptions := {
  module := "Data.List.Basic"
  maxResults := 50
  json := true
  indexMode := .readIndex  -- Require existing cache
}
```

--------------------------------

### Complex Query Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Execute multiple queries with various options, including specifying multiple Olean paths, a custom index file, and JSON output.

```bash
loogle \
  --module Mathlib.Data.List.Basic \
  --path /path/to/olean1 \
  --path /path/to/olean2 \
  --index-file /tmp/my-cache.loogle-index \
  --json \
  "List.filter" \
  "List.map"
```

--------------------------------

### Example CLI Search Query

Source: https://github.com/nomeata/loogle/blob/master/README.md

Demonstrates how to use the loogle CLI to search for a specific pattern in Lean code. The first call builds the search index, which is cached for subsequent faster searches.

```bash
$ loogle '(List.replicate (_ + _) _ = _)'
```

--------------------------------

### Run Loogle server

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Starts the Loogle server with a specified number of worker processes.

```bash
# Run server
./server.py --workers 4
```

--------------------------------

### Query Language Combination Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Illustrates how to combine multiple filters in a Loogle query using AND logic.

```text
List, "map", (α → β)  # All three must match
```

--------------------------------

### Minimal Loogle Setup

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/README.md

Run Loogle to search for a specific declaration, like 'List.map', against the default Mathlib index.

```bash
loogle "List.map"
```

--------------------------------

### Example Usage of renderFilters

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Shows how to use renderFilters with an array containing a Lean identifier for List.

```lean
let filters := #[⟨Lean.mkIdent `List⟩]
let str ← renderFilters filters
-- Result: "List"
```

--------------------------------

### CLI Search Examples

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Demonstrates various ways to search for declarations using the Loogle CLI. Supports direct string matching, keyword combination, and type pattern matching.

```bash
loogle "List.map"                    # Search for declarations mentioning List.map
```

```bash
loogle "List, map"                   # Combine filters with AND
```

```bash
loogle '"replicate"'                 # String search (substring match)
```

```bash
loogle '⊢ Nat'                       # Find all Nat-returning declarations
```

```bash
loogle '(List α) → Nat'              # Pattern matching
```

```bash
loogle --json "List.map"             # JSON output
```

```bash
loogle --interactive                 # Read queries from stdin
```

--------------------------------

### Example Usage of work Function

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

Demonstrates how to call the `work` function with specific `LoogleOptions` and a continuation that performs interactive search and prints JSON results. Ensure `LoogleOptions` are correctly configured before use.

```lean
let opts : LoogleOptions := {
  module := "Mathlib"
  json := true
  interactive := true
  indexMode := .useIndex
}
← work opts fun index => interactive index 200 printJson
```

--------------------------------

### Worker Management Examples

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Control the number of worker processes and their restart delay. Each worker manages its own Lean environment and index.

```bash
# Single worker (suitable for single-threaded access)
./server.py --workers 1
```

```bash
# 4 workers (handles 4 concurrent queries)
./server.py --workers 4 --host 0.0.0.0
```

```bash
# Many workers (on large server)
./server.py --workers 16
```

--------------------------------

### Handle GET Requests - MyHandler

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Handles GET requests for the main query interface. Supports various URL paths for web forms, JSON endpoints, and metrics. Parses queries, identifies client types, and returns results in JSON or HTML format. Implements load shedding and CORS headers.

```python
def do_GET(self)
```

--------------------------------

### Run Python HTTP Server for Loogle with Project and Loogle Arguments

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

Starts the Python HTTP server for Loogle, specifying the project directory and forwarding arguments to the loogle binary. The server automatically loads and caches the index, handles HTTP requests, and restarts workers if they fail.

```bash
./server.py --project-dir /path/to/mathlib -- --module Mathlib
```

--------------------------------

### Set Up Lake Option Handler

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Configures a Lake option handler, specifying short, long, and combined short-with-argument forms. This setup is used for consistent option parsing with Lake commands.

```lean
def lakeOption := 
  Lake.option {
    short := lakeShortOption
    long := lakeLongOption
    longShort := Lake.shortOptionWithArg lakeShortOption
  }
```

--------------------------------

### Zulip Query Extraction Examples

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Illustrates how the Zulip bot extracts search queries from messages using regex.

```text
"@**loogle**: List.map"        → query: "List.map"
"@**loogle** Real.sin"         → query: "Real.sin"
"@**loogle**? List.length"     → query: "List.length"
"@**loogle**: Real.sin, List"  → query: "Real.sin, List"
```

--------------------------------

### Take Command Line Argument

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Retrieves the next argument from the command line. Throws a 'missingArg' error if the argument is not found. Use this to get values for command-line options.

```lean
def takeArg (arg : String) : CliM String
```

```lean
let path ← takeArg "--path"  -- Gets next argument or errors
```

--------------------------------

### Index Rebuild Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Rebuild and cache the Loogle index for a specific module using the --index-mode write option.

```bash
loogle --index-mode write --module Mathlib
```

--------------------------------

### Specifying Custom Index File Path

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Provides an example of using the --index-file option to specify a custom path for the loogle cache file. This is useful when the default location is not writable.

```bash
loogle --index-file /tmp/mathlib-cache.loogle-index "List.map"
```

--------------------------------

### systemd Service Usage Commands

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Commands to manage the Loogle systemd service. Use these to start, check the status, and view logs of the Loogle service.

```bash
sudo systemctl start loogle
sudo systemctl status loogle
sudo journalctl -u loogle -f  # Stream logs
```

--------------------------------

### Interactive Query Loop

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

Starts an interactive query loop that reads queries from standard input until EOF. It prints a ready signal, then processes each non-empty line by calling the `single` function with the specified parameters.

```lean
def interactive (index : Find.Index) (maxResults : Nat) (print : Printer) : CoreM Unit
```

```lean
← interactive index 200 printJson
# Then at stdin, user types:
# List.map
# Real.sin
# (empty line to exit)
```

--------------------------------

### GET /metrics

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Exposes Prometheus metrics for monitoring the Loogle service. This endpoint is available only if the `prometheus_client` Python package is installed.

```APIDOC
## GET /metrics

### Description
Prometheus metrics endpoint that provides insights into the Loogle service's performance and status. This endpoint is optional and its availability depends on the installation of the `prometheus_client` package.

### Method
GET

### Endpoint
/metrics

### Response
#### Success Response (200)
- **Content-Type**: `text/plain; version=0.0.4`
- **Body**: Prometheus text format metrics.

### Response Example
```text
# HELP versions Lean and mathlib versions
# TYPE versions gauge
versions_info{loogle="abc1234",project="Mathlib",project_rev="def5678"} 1.0

# HELP queries Total number of queries
# TYPE queries counter
queries_total 42.0

# HELP errors_backend Queries failed because the backend crashed or timed out
# TYPE errors_backend counter
errors_backend_total 2.0

# ... (more metrics)

# HELP results Results per query
# TYPE results histogram
results_bucket{le="0"} 5.0
results_bucket{le="1"} 10.0
results_bucket{le="2"} 20.0
... results_bucket{le="+Inf"} 42.0
results_sum 150.0
results_count 42.0

# ... (more histogram buckets)
```

### Status Codes
- **200**: Success (prometheus_client installed)
- **500**: prometheus_client not installed

### Available Metrics
| Metric | Type | Description |
|--------|------|-------------|
| `versions` | Info | Versions of Loogle and served project |
| `queries` | Counter | Total query count |
| `errors_backend` | Counter | Worker crashes/timeouts/sandbox |
| `errors_loogle` | Counter | Loogle-level errors |
| `errors_denylist` | Counter | Blocked user agents |
| `load_shed` | Counter | Requests rejected (all workers busy) |
| `restarts` | Counter | Worker restarts by reason (sandbox/died/unresponsive) |
| `workers_lost` | Counter | Workers removed after failed restart |
| `results` | Histogram | Result counts per query (buckets: 0,1,2,5,10,50,100,200,500,1000) |
| `heartbeats` | Histogram | Solver iterations per query (buckets: 0,2e0,2e1,2e2,2e3,2e4) |
| `clients` | Counter | Clients by type (web/json/zulip/nvim/vscode-lean4/vscode-logue/LeanSearchClient/lean-lsp-mcp/meta-agent) |
| `workers_available` | Gauge | Current pool size |

### Installation (if missing)
```bash
pip install prometheus_client
# Then restart the server
```

### Example Request
```bash
curl 'http://localhost:8088/metrics'
```
```

--------------------------------

### Fetch Prometheus Metrics

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Access the Prometheus metrics endpoint by sending a GET request to /metrics. This endpoint is available only if the prometheus_client package is installed.

```bash
curl 'http://localhost:8088/metrics'
```

--------------------------------

### Running Loogle Locally

Source: https://github.com/nomeata/loogle/blob/master/README.md

Steps to set up and run the loogle binary locally. This involves cloning the repository, copying the target project's lean-toolchain, building with lake, and then executing loogle with a specified module and query.

```bash
cp /path/to/project/lean-toolchain .
lake build
lake env /path/to/loogle/.lake/build/bin/loogle \
  --module MyModule "<query>"
```

--------------------------------

### Initialize Loogle Worker

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Initializes and starts a new loogle worker subprocess. The caller should check `is_alive()` to ensure the worker started successfully.

```python
class Loogle:
    def __init__(self)
    def start(self) -> bool
    def is_alive(self) -> bool
    def do_query(self, query: str) -> dict
    def query(self, query: str) -> dict
```

```python
def __init__(self)
```

```python
worker = Loogle()
if not worker.is_alive():
    print("Worker failed to start")
```

--------------------------------

### work

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/loogle-core.md

The unsafe main entry point that sets up the Lean environment and search index. It resolves the search path, imports the root module, builds or loads the search index, and then calls a continuation with the initialized index.

```APIDOC
## Function: work

Unsafe main entry point that sets up the Lean environment and index.

```lean
unsafe def work (opts : LoogleOptions) (act : Find.Index → CoreM Unit) : IO Unit
```

### Parameters

| Parameter | Type | Description |
|-----------|------|-------------|
| `opts` | `LoogleOptions` | Configuration (module, search paths, cache mode, etc.) |
| `act` | `Find.Index → CoreM Unit` | Continuation to run with the initialized index |

### Behavior

1. Resolves search path (explicit `--path` → `LEAN_PATH` env var → compile-time default)
2. Sets `searchPathRef` for module loading
3. Enables initializers execution
4. Imports the specified root module (default: `Mathlib`)
5. Builds or loads the search index based on `opts.indexMode`:
   - `useIndex`: Load if fresh, rebuild if stale
   - `readIndex`: Load only if fresh, error otherwise
   - `writeIndex`: Always rebuild and cache
   - `noIndex`: In-memory only, no I/O
6. Validates index freshness via Lake `depHash` from `.trace` file
7. Warms caches to avoid lazy initialization during seccomp confinement
8. Enables seccomp sandbox (Linux)
9. Calls the continuation with the index

### Index File Location

- Default: next to root module's `.olean`, with `.loogle-index` extension
- Override: `--index-file PATH` in `LoogleOptions.indexFile`

### Error Handling

- Missing `.olean`: Normal Lean import error
- Stale index with `readIndex`: Throws error with message and suggestion to use `--index-mode use`
- Write failure: Suggests `--index-file` if default location is read-only
- Bad greeting from subprocess (in server.py): Worker not added to pool

### Example

```lean
let opts : LoogleOptions :=
  { module := "Mathlib"
    json := true
    interactive := true
    indexMode := .useIndex }
← work opts fun index => interactive index 200 printJson
```

**Source:** `Loogle.lean:173-276`
```

--------------------------------

### Loogle Server Metrics Endpoint

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

If the prometheus_client library is installed, metrics are collected and exposed at the /metrics endpoint in Prometheus text format. If not installed, /metrics returns HTTP 500.

```text
versions info
queries counter
errors_backend counter
errors_loogle counter
errors_denylist counter
load_shed counter
restarts counter
workers_lost counter
results histogram
heartbeats histogram
clients counter
workers_available gauge
```

--------------------------------

### Running the Loogle Web Service Locally

Source: https://github.com/nomeata/loogle/blob/master/README.md

Instructions to run the loogle web service locally. This requires building the project and then executing the server script, specifying the project directory and optionally forwarding arguments to the loogle binary.

```bash
lake build
./server.py --project-dir /path/to/project -- --module RootModule
```

--------------------------------

### GET /loogle-banner.png

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Retrieves the Loogle banner image. This endpoint is intended for social media previews.

```APIDOC
## GET /loogle-banner.png

### Description
Loogle banner image.

### Method
GET

### Endpoint
/loogle-banner.png

### Response
#### Success Response (200)
- **Content-Type** (string) - `image/png`
- **Body** (binary) - PNG image data
```

--------------------------------

### JSON Response (Success)

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Example of a successful JSON response from the Loogle API, indicating search results.

```json
{
  "header": "Found 2 declarations mentioning List.replicate.",
  "count": 2,
  "hits": [
    {
      "name": "List.replicate_add",
      "type": "∀ (n m : ℕ) (x : α), ...",
      "module": "Data.List.Basic",
      "doc": "docstring or null"
    }
  ],
  "heartbeats": 42
}
```

--------------------------------

### CLI Options Reference

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Lists available command-line options for configuring Loogle's search behavior and output.

```bash
--module MOD              # Root module (default: Mathlib)
```

```bash
--json                    # JSON output
```

```bash
--interactive, -i         # Interactive mode
```

```bash
--path PATH               # Add to search path
```

```bash
--index-mode MODE         # use|read|write|none
```

```bash
--index-file PATH         # Cache location
```

```bash
--max-results N           # Result limit (default: 200)
```

--------------------------------

### Custom Module Search Configuration

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Configure the server to search a specific project instead of the default Mathlib. Ensure the project directory and module name are correctly specified.

```bash
# Search a specific project instead of Mathlib
./server.py \
  --project-dir /my/project \
  -- --module MyProject --index-mode use
```

--------------------------------

### GET /loogle.png

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Retrieves the Loogle logo icon. This endpoint is suitable for browser favicons and UI elements.

```APIDOC
## GET /loogle.png

### Description
Loogle logo icon.

### Method
GET

### Endpoint
/loogle.png

### Response
#### Success Response (200)
- **Content-Type** (string) - `image/png`
- **Body** (binary) - PNG image data
```

--------------------------------

### Create Index from Cache - Lean

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Use `Index.mkFromCache` to initialize an index with pre-computed data. This is useful for loading persisted indexes or using pre-built mathlib indexes.

```lean
def Index.mkFromCache (init : NameRel × SuffixTrie) : IO Index
```

--------------------------------

### Server Options Reference

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Lists available options for configuring the Loogle HTTP server's network settings and worker processes.

```bash
--host ADDR              # Listen address (default: localhost)
```

```bash
--port PORT              # Listen port (default: 8088)
```

```bash
--workers N              # Worker processes (default: 1)
```

```bash
--project-dir PATH       # Lake project
```

```bash
--loogle-bin PATH        # Path to binary
```

```bash
-- LOOGLE_ARGS           # Forward to loogle
```

--------------------------------

### JSON Response (Error)

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Example of an error response from the Loogle API, providing details about the encountered issue and suggestions.

```json
{
  "error": "unknown identifier 'foo'",
  "heartbeats": 5,
  "suggestions": ["List.filter", "List.map"]
}
```

--------------------------------

### GET /json

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Provides search results in JSON format for a given query. This endpoint is suitable for programmatic access.

```APIDOC
## GET /json

### Description
Provides search results in JSON format for a given query. This endpoint is suitable for programmatic access.

### Method
GET

### Endpoint
/json

### Parameters
#### Query Parameters
- **q** (string) - Required - The search query.

### Request Example
GET /json?q=some+query

### Response
#### Success Response (200)
- JSON object containing search results.

#### Response Example
```json
{
  "results": [
    {
      "name": "Example.Function",
      "link": "https://example.com/docs/Example/Function"
    }
  ]
}
```

**CORS Headers:**
```
Access-Control-Allow-Origin: *
Access-Control-Allow-Headers: User-Agent, X-Loogle-Client
```
```

--------------------------------

### Dockerfile for Loogle Server

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Use this Dockerfile to build a containerized Loogle server. It sets up the Lean 4 environment, clones and builds mathlib, copies the Loogle server code, and configures the server to run on port 8088.

```dockerfile
FROM leanprover/lean4:v4.0.0

RUN git clone https://github.com/leanprover-community/mathlib4 /mathlib && \
    cd /mathlib && \
    lake build

COPY loogle /loogle
WORKDIR /loogle
RUN lake build

EXPOSE 8088
CMD ["./server.py", "--host", "0.0.0.0", "--port", "8088", "--workers", "2", \
     "--project-dir", "/mathlib", "--", "--module", "Mathlib"]
```

--------------------------------

### Setting LEAN_PATH with lake env

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Demonstrates how to set the LEAN_PATH environment variable using the `lake env` command, which automatically configures the path for Lean 4 projects. This is the recommended way to manage LEAN_PATH.

```bash
LEAN_PATH="/home/user/.elan/toolchains/leanprover--lean4---v4.0.0/lib/lean:/path/to/mathlib/.lake/build/lib" \
  loogle "List.map"
```

--------------------------------

### OPTIONS /json

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Handles CORS preflight requests for cross-origin access to the /json endpoint. It allows GET requests from any origin.

```APIDOC
## OPTIONS /json

### Description
CORS preflight request for cross-origin access.

### Method
OPTIONS

### Endpoint
/json

### Query Parameters
None

### Response Headers
- Access-Control-Allow-Origin: *
- Access-Control-Allow-Methods: GET
- Access-Control-Allow-Headers: User-Agent, X-Loogle-Client
- Content-Type: application/json

### Response Body
Empty

### Status Code
200

### Purpose
Browsers send this automatically before certain requests. Server responds to allow CORS GET requests to `/json`.

### Request Example
```bash
curl -X OPTIONS \
  -H 'Origin: https://example.com' \
  'http://localhost:8088/json'
```
```

--------------------------------

### CLI Entry Points

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/MANIFEST.txt

Main dispatcher and entry points for the command-line interface.

```APIDOC
## cliMain

### Description
Main CLI dispatcher function.

### Signature
cliMain() -> None

## main

### Description
Binary entry point for the CLI.

### Signature
main() -> None
```

--------------------------------

### Loogle Class Initialization

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Initializes and starts a new loogle worker subprocess. The caller should check `is_alive()` to confirm successful startup.

```APIDOC
## Method: __init__

### Description
Initialize and start a new worker subprocess.

### Behavior:
Calls `start()` to spawn the loogle process. Does not raise exceptions; caller should check `is_alive()`.

### Example:
```python
worker = Loogle()
if not worker.is_alive():
    print("Worker failed to start")
```
```

--------------------------------

### Loogle JSON API Error Response Schema

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

This is an example of an error response from the Loogle JSON API, indicating an unknown identifier.

```json
{
  "error": "unknown identifier 'List.foo'",
  "heartbeats": 5,
  "suggestions": ["List.filter", "List.find"]
}
```

--------------------------------

### Loogle JSON API Success Response Schema

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

This is an example of a successful response from the Loogle JSON API, detailing search results.

```json
{
  "header": "Found 3 declarations mentioning List.replicate.",
  "count": 3,
  "hits": [
    {
      "name": "List.replicate_add",
      "type": "∀ (n m : ℕ) (x : α), replicate (n + m) x = replicate n x ++ replicate m x",
      "module": "Data.List.Basic",
      "doc": "Optional docstring if available"
    }
  ],
  "heartbeats": 42,
  "suggestions": ["List.replicate (_ + _) _"]
}
```

--------------------------------

### Create Empty Index - Lean

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Use `Index.mk` to create a new, empty search index. The index caches are populated automatically when queries are executed.

```lean
let index ← Find.Index.mk
let result ← find index filters 200
```

--------------------------------

### Find Proofs of Equality

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/query-language.md

Searches for all proofs that demonstrate equality between two terms.

```bash
logue '⊢ _ = _'
```

--------------------------------

### JSON Schema Example

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/MANIFEST.txt

This snippet illustrates a JSON schema for representing query results. It defines the structure and types for fields like 'query', 'results', and 'error'.

```json
{
  "type": "object",
  "properties": {
    "query": {"type": "string"},
    "results": {
      "type": "array",
      "items": {"type": "string"}
    },
    "error": {"type": "string"}
  }
}
```

--------------------------------

### Loogle CLI Usage Help

Source: https://github.com/nomeata/loogle/blob/master/README.md

Displays the help message for the loogle command-line interface, outlining available options and their descriptions.

```bash
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)
```

--------------------------------

### Build and Run Loogle in a Lean Project (Standalone CLI)

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

Builds Loogle within a Lean project using `lake build` and then runs it via `lake env` with specified module and JSON output. This is for standalone CLI usage.

```bash
lake build                          # Build loogle
lake env loogle --module MyProject "pattern" --json
```

--------------------------------

### GET /

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

The main web interface provides an HTML form for searching and interacting with Loogle. It supports basic search queries and a 'lucky' option to redirect to the first result.

```APIDOC
## GET /

### Description
Main web interface with HTML form.

### Method
GET

### Endpoint
/

### Query Parameters
- `q` (string) - Optional - Search query (e.g., `List.map`)
- `lucky` (string) - Optional - If present, redirect to first result's documentation

### Response Headers
- `Content-Type`: `text/html`
- `Access-Control-Allow-Origin`: `*`
- `Access-Control-Allow-Headers`: `User-Agent, X-Loogle-Client`

### Response Body
HTML page with: Loogle branding and form, Search input field, #find and #lucky buttons, Results as bulleted list with links to Mathlib docs, Suggestions if query failed, Footer with Loogle and project revision info.

### Status Codes
- 200: Success (normal or with no results)
- 503: Service unavailable (all workers busy)

### Examples
```bash
# Basic search
curl 'http://localhost:8088/?q=List.map'

# With lucky redirect
curl 'http://localhost:8088/?q=List.length&lucky=yes'

# URL-encoded query
curl 'http://localhost:8088/?q=Real.sin%20%2B%20Real.cos'
```
```

--------------------------------

### Get Index Cache Data - Lean

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Use `Index.getCache` to extract cached index data for serialization. This function returns data only for imported declarations, excluding locally-defined ones.

```lean
def Index.getCache (i : Index) : CoreM (NameRel × SuffixTrie)
```

--------------------------------

### Short Options

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Handles short-form command-line options for interactive mode, JSON output, and help.

```APIDOC
## Short Options

### Description
Handles short-form command-line options.

### Method
`lakeShortOption`

### Parameters
- `opt` (Char) - The short option character.

### Supported Options:
- `-i` — Interactive mode
- `-j` — JSON output
- `-h` — Help

### Example
```lean
lakeShortOption 'i'
lakeShortOption 'j'
lakeShortOption 'h'
```
```

--------------------------------

### Using LEAN_PATH Environment Variable

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/configuration.md

Demonstrates how to set the LEAN_PATH environment variable to specify directories for .olean files when running loogle. This allows loogle to find compiled Lean modules.

```bash
# Use LEAN_PATH
LEAN_PATH="/path1:/path2" loogle "List.map"
```

--------------------------------

### Loogle CLI Dispatcher Logic

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

This snippet outlines the core logic within the `cliMain` function, determining how arguments are processed, help messages are displayed, and queries are executed or an interactive session is started.

```lean
if opts.wantsHelp ||
  queries.isEmpty && not opts.interactive && not workWithoutQuery
then IO.println usage
else work opts fun index => do
  queries.forM (single index opts.maxResults print)
  if opts.interactive
  then interactive index opts.maxResults print
```

--------------------------------

### Find Declarations Mentioning List, Nat, and 'add'

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/README.md

Search for declarations that mention 'List', 'Nat', and have 'add' in their name.

```bash
loogle 'List, Nat, "add"'
```

--------------------------------

### Parse Short Options

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/cli-entry.md

Handles short command-line options like -i, -j, and -h. Throws an error for unknown short options.

```lean
def lakeShortOption : (opt : Char) → CliM PUnit
  | 'i' => set interactive := true
  | 'j' => set json := true
  | 'h' => set wantsHelp := true
  | _ => throw unknownShortOption
```

--------------------------------

### Loogle Server Command-Line Arguments

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/server-http.md

Use these arguments to configure the Loogle server's host, port, worker count, project directory, and loogle binary path. Arguments after '--' are forwarded to loogle.

```bash
./server.py [OPTIONS] [-- LOOGLE_ARGS]
```

```bash
./server.py --host 0.0.0.0 --port 8080 --workers 4 \
  --project-dir /path/to/mathlib -- --module Mathlib --max-results 100
```

--------------------------------

### Run Python HTTP Server for Loogle

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/overview.md

Launches the Python HTTP server for Loogle, managing worker subprocesses and providing an HTTP frontend. Specify host, port, worker count, project directory, and loogle binary path. Additional arguments can be forwarded to the loogle binary.

```bash
./server.py [--host ADDR] [--port PORT] [--workers N] \
  [--project-dir PATH] [--loogle-bin PATH] \
  [-- LOOGLE_ARGS...]
```

--------------------------------

### Loogle JSON API Endpoint

Source: https://github.com/nomeata/loogle/blob/master/README.md

Example of accessing the loogle web service via a JSON API endpoint. The query is passed as a URL parameter 'q'. Note that the JSON format stability is not guaranteed.

```bash
/json?q=…
```

--------------------------------

### Web Search Workflow Steps

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/endpoints.md

Outlines the sequence of events for a typical web search request, from browser navigation to rendering results.

```workflow
1. Browser navigates to http://localhost:8088/?q=List.map
2. GET / handler is called
3. Query "List.map" is extracted
4. Worker is obtained from pool
5. Query is executed
6. Results are formatted as HTML
7. HTML page is returned (200 OK)
8. Browser renders page with results
9. User can click result links to Mathlib docs
```

--------------------------------

### Find Theorems About sin and Cosine

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/query-language.md

Searches for theorems related to the trigonometric functions 'sin' and 'cos' in the Real number domain.

```bash
logue 'Real.sin, Real.cos'
```

--------------------------------

### Optimize Loogle Queries with Constants and Name Patterns

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/query-language.md

Demonstrates how to optimize query performance by using constants and name patterns early. Narrowing the search space with constants and specific names like 'map' is faster than broad pattern matching.

```Loogle Query
# Slower: broad pattern
logue '(α → β)'
```

```Loogle Query
# Faster: narrow with constants first
logue 'List, (α → β)'
```

```Loogle Query
# Even faster: add name pattern
logue 'List, "map", (α → β)'
```

--------------------------------

### Configure LEAN_PATH Environment Variable

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/QUICKREF.md

Set the LEAN_PATH environment variable to specify directories for searching .olean files. Paths are separated by colons.

```bash
LEAN_PATH="/path1:/path2"
```

--------------------------------

### Index.mk

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Creates a fresh, empty search index. Caches are populated on demand when queries are executed.

```APIDOC
## Function: Index.mk

Create a fresh, empty index.

```lean
def Index.mk : IO Index
```

**Return:**
An `Index` with empty `NameRel` and suffix trie caches.

**Effect:**
When any query is executed, the caches are automatically populated by scanning all declarations in the environment.

**Example:**
```lean
let index ← Find.Index.mk
let result ← find index filters 200
```

**Source:** `Loogle/Find.lean:235-238`
```

--------------------------------

### Index.mkFromCache

Source: https://github.com/nomeata/loogle/blob/master/_autodocs/api-reference/find-search.md

Initializes a search index using previously cached data, suitable for loading persisted indices or pre-built mathlib indices.

```APIDOC
## Function: Index.mkFromCache

Create an index from previously cached data.

```lean
def Index.mkFromCache (init : NameRel × SuffixTrie) : IO Index
```

**Parameters:**
| Parameter | Type | Description |
|-----------|------|-------------|
| `init` | `NameRel × SuffixTrie` | Pre-computed index data (from `Index.getCache` or deserialized) |

**Return:**
An `Index` initialized with the cached data, plus empty caches for newly-added declarations.

**Use Cases:**
- Loading persisted index from disk (see `Loogle.lean:work`)
- Using pre-built mathlib indices

**Source:** `Loogle/Find.lean:248-251`
```