Metadata-Version: 2.4
Name: axiomatic-octo
Version: 0.2.8
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

<p align="center">
  <img src="extensions/octo/images/octo_search.svg" alt="Axiomatic Octo logo" width="180">
</p>

<h1 align="center">Axiomatic Octo</h1>

<p align="center">
  <a href="https://github.com/AxiomaticX/ax-assistant-public-staging/actions/workflows/unit_tests.yml"><img src="https://github.com/AxiomaticX/ax-assistant-public-staging/actions/workflows/unit_tests.yml/badge.svg" alt="Unit tests"></a>
  <a href="pyproject.toml"><img src="https://img.shields.io/badge/python-3.11%2B-3776AB" alt="Python 3.11+"></a>
  <a href="LICENSE"><img src="https://img.shields.io/badge/License-AGPL--3.0-2563A6" alt="License: AGPL-3.0"></a>
  <a href="https://pypi.org/project/axiomatic-octo/"><img src="https://img.shields.io/pypi/v/axiomatic-octo" alt="PyPI version"></a>
</p>

Axiomatic Octo is a swiss army knife for Lean (auto)formalization workflows.
Today, it provides semantic search over your own projects and common dependencies
such as Mathlib, Batteries, CSLib, and Physlib through a VS Code extension and
Python CLI. The roadmap includes broader theorem-proving and knowledge-management
tools.

## Install

**VS Code (recommended):** install Axiomatic Octo from the Marketplace and open
a Lean project. The extension completes setup on first activation.

Hosted project indexing requires a GitHub repository. The extension identifies
it from the Git `origin` remote and supports SSH host aliases when the remote
path uses the standard `owner/repository` form.

**CLI only:**

```bash
uv tool install axiomatic-octo
```

To build your own search index, install the optional dependencies:

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

## Quickstart

Set `OPENROUTER_API_KEY` in your environment or a project-root `.env.secrets`
file, then run:

```bash
cd my-lean-project
octo search fetch
octo search query "self-adjoint operator is symmetric"
```

Use `octo search status` to check installed databases and updates. Local index
creation is available through `octo search index` when the optional dependencies
are installed.

Axiomatic hosts project databases by default. Repositories that already build a
`search-lean-db` workflow artifact can set `search_lean.db_source` to
`workflow`. Octo uses only the selected source and does not fall back.

## Agents

Octo includes a workspace-scoped Claude Code skill that lets agents search Lean
declarations through the CLI. After the VS Code extension starts successfully,
enable terminal and agent access when prompted. You can also run
**Octo: Enable terminal / agent access** from the Command Palette. The extension
installs the skill under `.claude/skills/`, offers to add
`.claude/skills/octo*` to `.gitignore`, and keeps the skill synchronized when
Octo updates.

## Development

```bash
uv sync
pnpm install

uv run pytest
uv run ruff check .
pnpm --filter axiomatic-octo run test
```

To run the extension from source, open the repository in VS Code and launch
**Run Search Extension (isolated)**. After changing
`src/axiomatic_octo/protocol.py`, regenerate the TypeScript bindings with:

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

## License

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