acorn-search

Search tool for the Acorn theorem prover's standard library. Given a theorem to prove, find relevant definitions, lemmas, types, and typeclasses.

Provides three interfaces: CLI, Python API, and MCP server (for Claude Code / LLM agents).

Quick Start

# 1. Clone and install
git clone git@github.com:AIxMath/acorn-search.git
cd acorn-search
pip install -e .

# 2. Export your Acorn standard library
cd /path/to/your/acornlib
acorn export --proof-deps
# This creates export/*.jsonl (one file per module)

# 3. Build the search database
acorn-search-build --export /path/to/your/acornlib/export --db /path/to/acorn.db

# 4. Verify it works
acorn-search --db /path/to/acorn.db --stats

MCP Server (Claude Code Integration)

Setup

After completing the Quick Start above, add this to ~/.claude/settings.json:

{
  "mcpServers": {
    "acorn-search": {
      "command": "acorn-search-server",
      "args": ["--db", "/path/to/acorn.db"]
    }
  }
}

Replace /path/to/acorn.db with the actual path from step 3.

Restart Claude Code. The 15 search tools will be available automatically.

Available Tools

Search:

Tool	Description	Example input
search	Full-text search (FTS5)	"add_comm", "prime AND nat"
search_by_name	Name substring match	"add_comm"
search_by_type	Type signature match	"Nat -> Nat -> Nat"
search_similar_type	Structurally similar types	"(Nat, Nat) -> Nat"
search_by_statement	Statement substring match	"a + b = b + a"
search_similar_statement	Structurally similar statements	"a + b = b + a"

Browse & Inspect:

Tool	Description	Example input
get_item	Full item details (source, deps)	"nat.nat_base.add_comm"
get_source	Source code of an item	"nat.nat_base.Nat"
get_dependencies	What an item uses	"nat.nat_base.add_comm"
get_dependents	What uses an item	"add.Add.add"
list_modules	List all modules	—
browse_module	List items in a module	"nat.nat_base"
stats	Database statistics	—

Feedback:

Tool	Description
feedback	Rate search quality, submit comments
bug_report	Report bugs or unexpected behavior

Feedback is appended to feedback.jsonl in the repo directory.

Rebuilding After Library Changes

When your Acorn standard library is updated:

cd /path/to/your/acornlib && acorn export --proof-deps
acorn-search-build --export /path/to/your/acornlib/export --db /path/to/acorn.db

No need to restart Claude Code — the server picks up the new DB on next query.

CLI

# Full-text search (FTS5 — supports AND/OR/NOT, "phrases", prefix*)
acorn-search "add_comm"
acorn-search "prime AND nat"

# Search by name (substring match)
acorn-search --name add_comm

# Search by type signature
acorn-search --type "Nat -> Nat -> Nat"

# Find structurally similar types (tree edit distance)
acorn-search --similar-type "(Nat, Nat) -> Nat"

# Search theorem statements
acorn-search --statement "a + b = b + a"

# Find structurally similar statements (tree edit distance)
acorn-search --similar-statement "a + b = b + a"

# Item details
acorn-search --item nat.nat_base.add_comm

# Dependencies
acorn-search --deps nat.nat_base.add_comm    # what it uses
acorn-search --rdeps "add.Add.add"            # what uses it

# Browse
acorn-search --module nat.nat_base
acorn-search --stats

# Options
acorn-search "add" --kind theorem,definition --limit 50 --json
acorn-search --db /path/to/acorn.db "query"   # custom DB path

Python API

from acorn_search.db import AcornDB
from acorn_search.search import SearchEngine

db = AcornDB("/path/to/acorn.db")
engine = SearchEngine(db)

# Full-text search
results = engine.search("add_comm", kinds=["theorem"], limit=10)

# Name search
results = engine.search_by_name("add_comm")

# Type signature search
results = engine.search_by_type("Nat -> Nat -> Nat")

# Structurally similar types (tree edit distance)
results = engine.search_similar_type("(Nat, Nat) -> Nat", min_similarity=0.5)

# Structurally similar statements
results = engine.search_similar_statement("a + b = b + a", min_similarity=0.4)

# Statement substring search
results = engine.search_by_statement("a + b = b + a")

# Dependency graph
results = engine.dependencies_of("nat.nat_base.add_comm")   # forward
results = engine.dependents_of("add.Add.add")                # reverse

# Module browsing
modules = engine.list_modules()
items = engine.browse_module("nat.nat_base")

# Full item detail
detail = engine.get_item_detail("nat.nat_base.add_comm")

Subset database

Generate a minimal database containing only specific items and their transitive dependencies:

from acorn_search.subset import generate_subset_db

subset = generate_subset_db(db, {"nat.nat_base.add_comm"}, "subset.db")

Architecture

acorn_search/
├── db.py            — SQLite schema + builder (from export JSONL)
├── search.py        — Search engine (FTS5, type matching, deps)
├── tree_distance.py — Type/statement parsing + Zhang-Shasha tree edit distance
├── subset.py        — Subset database generation
├── mcp_server.py    — MCP server (15 tools)
└── cli.py           — CLI interface

Database schema

• modules — module metadata (name, imports, numerals)
• items — all exported items with source_block, type_signature, statement, etc.
• deps — dependency edges (item_id → dep_qname, dep_kind)
• items_fts — FTS5 full-text index (auto-synced via triggers)

Tests

python -m pytest tests/ -q