Metadata-Version: 2.4
Name: axiomatic-octo
Version: 0.2.0
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: 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: python-lsp-jsonrpc>=1.1.2
Provides-Extra: build-search-index
Requires-Dist: ax-prover>=0.1; extra == "build-search-index"
Requires-Dist: langchain-core>=0.3; extra == "build-search-index"
Requires-Dist: langchain-deepseek>=1.1.0; extra == "build-search-index"
Requires-Dist: langchain-openai>=0.2; extra == "build-search-index"
Requires-Dist: mistralai<2,>=1.9.11; extra == "build-search-index"
Requires-Dist: jinja2>=3.1; extra == "build-search-index"
Requires-Dist: datasets>=3.0; extra == "build-search-index"
Dynamic: license-file

# Axiomatic Octo

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 axiomatic-octo
```

That installs what you need to search and to download prebuilt databases (~12 MB).
Building your own index additionally needs the informalization LLM stack, which
is an opt-in extra because it is 25× the size:

```bash
uv tool install 'axiomatic-octo[build-search-index]'   # adds `octo search index`
```

## 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 over the same
`OPENROUTER_API_KEY` the embedder uses; without it, queries fall back to
vector-ranked results.

```bash
cd my-lean-project
octo search fetch                                  # download prebuilt search databases
octo search status                                 # what's installed, and any updates
octo search 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
(`octo search index`, which needs the `build-search-index` extra above).

## Layout

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

## Names

The PyPI distribution and the marketplace extension are both `axiomatic-octo`,
the module is `axiomatic_octo`, the commands are `octo` and `octo-sidecar`, and
the extension settings are `octo.*`.

CLI verbs sit under a domain, so it is `octo search query "..."` rather than
`octo query "..."`. The domain level is there so later domains can be added
under the one binary without disturbing these verbs.

These are stable surface now — renaming them again would break imports,
configs, and keybindings. Everything was last renamed from `ax-search-lean` /
`axSearchLean.*`; the extension migrates settings, the stored API key, and the
search-database cache on first activation.

## Development

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

uv run pytest                          # Python tests
uv run ruff check .                    # lint
pnpm --filter axiomatic-octo run test  # extension tests
```

`uv sync` includes the `build-search-index` extra (the dev group self-references
it), so the whole test suite runs. To reproduce what an extension user gets —
the wheel with no extras — build and install it into a scratch venv; the
`bare-install` CI job does exactly this and asserts the query path still
imports, since the dev environment can never catch a stray module-scope import
of the index stack.

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/axiomatic_octo/protocol.py`:

```bash
pnpm --filter axiomatic-octo run protocol:codegen
```

CI asserts the generated file is up to date.

## License

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