Metadata-Version: 2.4
Name: ax-assistant-release-staging
Version: 0.1.3
Summary: Semantic search over Lean 4 declarations — Mathlib and local corpora — as a CLI, a JSON-RPC sidecar, and a VS Code extension
Author-email: Austin Letson <austin@axiomatic-ai.com>
License-Expression: AGPL-3.0-only
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: ax-prover>=0.1
Requires-Dist: pydantic>=2.7
Requires-Dist: omegaconf>=2.3.0
Requires-Dist: python-dotenv>=1.2.1
Requires-Dist: platformdirs>=4.0
Requires-Dist: httpx>=0.27
Requires-Dist: sqlite-vec>=0.1.6
Requires-Dist: mistralai<2,>=1.9.11
Requires-Dist: langchain-core>=0.3
Requires-Dist: langchain-deepseek>=1.1.0
Requires-Dist: jinja2>=3.1
Requires-Dist: datasets>=3.0
Requires-Dist: python-lsp-jsonrpc>=1.1.2
Dynamic: license-file

# Axiomatic Lean Search

Semantic search over Lean 4 declarations — Mathlib, core, Batteries, and your
own Lean projects. Ask in plain English and get matching declarations, ranked
by meaning rather than name. Ships a Python CLI and JSON-RPC sidecar plus a
VS Code extension.

## Install

**VS Code (recommended):** install the extension from the Marketplace and open
a Lean project. On first activation it sets up everything it needs — including
its own Python — with no manual steps.

**CLI only:**

```bash
uv tool install ax-assistant-release-staging
```

## Quickstart

Queries embed your text with qwen3-embedding-8b via OpenRouter, so an API key
is required. Export `OPENROUTER_API_KEY`, or put it in a `.env.secrets` file
in your project root (the current directory, the `--folder` target, and a
user-global config file are checked in that order; shell environment always
wins). Results are reranked with Qwen3-Reranker-8B when `SILICONFLOW_API_KEY`
is also set; without it, queries fall back to vector-ranked results.

```bash
cd my-lean-project
ax-search-lean fetch                                  # download prebuilt search databases
ax-search-lean status                                 # what's installed, and any updates
ax-search-lean query "self-adjoint operator is symmetric"
```

Search databases are SQLite files with [`sqlite-vec`](https://github.com/asg017/sqlite-vec)
vector indexes, either downloaded prebuilt or built locally from a Lean project
(`ax-search-lean index`).

## Layout

| Path | What |
|---|---|
| `src/ax_assistant_public/` | Python package: CLI (`ax-search-lean`), JSON-RPC sidecar (`ax-search-lean-sidecar`), indexing and query engine |
| `extensions/ax-search-lean/` | VS Code extension — search sidebar, backed by the sidecar |

## Names

The PyPI distribution is `ax-assistant-release-staging` (provisional; see
`TODO-packaging.md`), the module is `ax_assistant_public`, the commands are
`ax-search-lean` and `ax-search-lean-sidecar`, and the extension settings are
`axSearchLean.*`. The module, command, and setting names are stable surface —
renaming them would break imports, configs, and keybindings.

## Development

```bash
uv sync                                # Python deps + editable install
pnpm install                           # extension deps

uv run pytest                          # Python tests
uv run ruff check .                    # lint
pnpm --filter ax-assistant-release-staging run test  # extension tests
```

To run the extension from source, open this repo in VS Code and launch
**"Run Search Extension (isolated)"** (F5). It loads only this extension and
resolves the sidecar from the repo `.venv`, so an installed release can't
shadow your working copy.

Regenerate the TypeScript protocol bindings after changing
`src/ax_assistant_public/protocol.py`:

```bash
pnpm --filter ax-assistant-release-staging run protocol:codegen
```

CI asserts the generated file is up to date.

## License

AGPL-3.0-only. See [LICENSE](LICENSE).
