CLI reference¶
Generated from the installed CLI at build time, this page contains each
command's complete --help output.
For what the values mean (model aliases, tuning knobs, precedence) see Configuration.
octo¶
Semantic search over Lean declarations: fetching and building search databases, and querying them. See Set up search on your repo for how to get started.
usage: octo [-h] {search} ...
Axiomatic Octo
positional arguments:
{search} octo domains
search Semantic search over Lean declarations (mathlib + local library)
octo search¶
usage: octo search [-h] [--folder FOLDER] [-c PATH] [--overrides KEY=VALUE]
{index,query,status,fetch,discover-build-targets} ...
Semantic search over Lean declarations (mathlib + local library)
positional arguments:
{index,query,status,fetch,discover-build-targets}
search verbs
index Update a search db (local project, or mathlib) via lean-
extract + the configured informalize LLM + embeddings
query Semantic search across attached search_dbs
status Show search_db paths, declaration counts, and remote update
info
fetch Download a pre-built search_db instead of building it locally.
Mathlib DBs come from published GitHub Releases; the local DB
comes from the ax search server or the project's own CI
workflow artifacts, per `search_lean.db_source`.
discover-build-targets
Read [[lean_lib]] entries from <folder>/lakefile.toml and
write them to <folder>/.axiomatic/search_lean/config.yaml. Run
once per project; `index` reads this file.
options:
--folder FOLDER Project root for the per-project local search_db (default:
cwd)
-c PATH, --config PATH
Extra YAML config file merged on top of the defaults (can be
used multiple times, merged in order). Must precede the verb.
--overrides KEY=VALUE
Dot-notation config override, e.g. --overrides
informalize_max_dependencies=5 (can be used multiple times).
Must precede the verb.
octo search index¶
usage: octo search index [-h] [--target TARGET [TARGET ...]] [--group GROUP]
[--package NAME] [--toolchain VERSION] [--source PATH]
[--from-search-db PATH] [--reuse-informalizations SPEC]
[--module-prefix PREFIX] [--all-modules] [--force]
[--concurrency N] [--yes] [--no-cache] [--dry-run] [--debug]
options:
--target TARGET [TARGET ...]
One or more search_dbs to update. 'local' (default): index the
current Lean project at ``--folder``. Corpus names (e.g.
`--target core batteries mathlib`) share one extraction and
build exactly the listed corpora in dependency order.
--group GROUP Build an entire corpus build group (e.g. 'mathlib-cluster') in
one sidecar Lake build and split the artifact into every
corpus it produces. Used by CI to publish
core/batteries/mathlib from one build. Mutually exclusive with
--target.
--package NAME [--target local] Lakefile-declared library name (also used as
the module-prefix filter). Overrides the build_targets list
from .axiomatic/search_lean/config.yaml. If omitted, the
config's build_targets are used; run `octo search discover-
build-targets` to generate that file.
--toolchain VERSION [--target mathlib] Lean version this build corresponds to
(e.g. v4.28.0). Defaults to the contents of <folder>/lean-
toolchain. Used to key the output search_db filename
(mathlib-<version>.db).
--source PATH Skip the Lake build and use this pre-built artifact: a lean-
extract .jsonl file, or a legacy doc-gen4 api-docs.db /
declaration-data*.bmp. Default: build and extract in-place
(--target local: against <folder>/.lake; --target mathlib:
against a per-version Lake workspace under the user cache).
Useful in CI where the workflow drives Lake itself for
explicit cache control.
--from-search-db PATH
Override the cache search_db (default: existing local.db for
--target local; manifest.current for --target mathlib).
Skipping the cache forces a full re-informalize + re-embed.
--reuse-informalizations SPEC
Reuse already-generated informalizations instead of
regenerating them with the LLM. SPEC is a FrenzyMath
HuggingFace dataset id (e.g. FrenzyMath/lsv2-mathlib-...), a
lean-explore build (lean-explore:<version> or lean-
explore:latest — auto-downloaded + cached), or a local
lean_explore.db path. Matched declarations skip the LLM (still
embedded). Repeatable; earlier sources win on name conflicts.
For our own search_dbs use --from-search-db instead (it also
reuses embeddings).
--module-prefix PREFIX
Restrict declarations to modules starting with PREFIX.
Repeatable. With multiple corpus targets, provide at least one
prefix in each target's namespace; for example Std.X,
Batteries.Y, and Mathlib.Z. Without overrides, each target
uses its registered corpus prefixes. Pass --all-modules to
disable filtering.
--all-modules [--target mathlib] Include every module the extraction covers
(Mathlib + stdlib + Batteries + ...). Overrides the default
Mathlib-only filter.
--force Ignore the existing local.db cache and re-build from scratch
(--target local only)
--concurrency N Concurrent Claude calls for informalization. Overrides
config.search_lean.informalize_concurrency (default: 32).
--yes Skip the interactive confirmation prompt before the first
(expensive) sidecar Lake build of a new mathlib version.
--no-cache Ignore any prior search_db and informalize every declaration
from scratch. Without this, the build falls back to the
manifest's `current` DB for the target; against a corpus with
pre-baked informalizations (e.g. FrenzyMath) that reuses them
by name and makes zero LLM calls — right for a cheap re-index,
wrong when the point of the build is to measure a specific
informalizer.
--dry-run Parse the source, classify declarations against the cache, and
print how many would need LLM calls + embed calls + the
estimated cost. Does not call any external APIs, write any
files, or update the manifest. For --target mathlib, the Lake
build still runs (it's incremental and cheap once the
workspace exists).
--debug Write every rendered informalization prompt and its resolved
dependency context to a sibling `<search_db>.prompts.jsonl`
file. Only prompts that actually make an LLM call are
recorded; combine with --no-cache to inspect every selected
declaration. These are real, paid LLM calls, so use narrow
module prefixes. Debug runs stop before embedding, writing a
search_db, or updating the manifest. In a multi-target run,
generated descriptions flow forward in memory between targets.
octo search query¶
usage: octo search query [-h] [-k N] [--scope SCOPE] [--frenzy DATASET] [--json] query
positional arguments:
query Natural-language search query
options:
-k N, --top-k N Max number of results to return (default: 20)
--scope SCOPE Which search_dbs to search (default: both). One of: both/auto (the
installed corpora this project depends on + local), all or
everything (every installed corpus + local, dependency or not),
local, a single corpus name (e.g. mathlib), or a comma-separated
list optionally including 'local' (e.g. mathlib,core,local).
Missing search_dbs are silently skipped.
--frenzy DATASET Pin a specific mathlib search_db by FrenzyMath dataset id
--json Emit hits as a JSON array (machine-readable) instead of plain text
octo search status¶
usage: octo search status [-h] [--json] [--source {hosted,workflow}]
options:
--json Emit a machine-readable JSON object instead of human-readable
text
--source {hosted,workflow}
[--target local] Where the project's own search_db comes from:
'hosted' (the ax search server) or 'workflow' (a search-lean-
db artifact from this repo's GitHub Actions). Overrides
`search_lean.db_source` in .axiomatic/config.yaml, which
defaults to hosted. There is no fallback between the two — the
selected source is the only one used.
octo search fetch¶
usage: octo search fetch [-h] [--source {hosted,workflow}] [--target TARGET]
[--toolchain VERSION] [--commit SHA] [--ref REF]
[--repo OWNER/REPO] [--force]
options:
--source {hosted,workflow}
[--target local] Where the project's own search_db comes from:
'hosted' (the ax search server) or 'workflow' (a search-lean-
db artifact from this repo's GitHub Actions). Overrides
`search_lean.db_source` in .axiomatic/config.yaml, which
defaults to hosted. There is no fallback between the two — the
selected source is the only one used.
--target TARGET Which search_db(s) to fetch (default: auto). One of: 'auto'
(corpora discovered from the project's lake-manifest.json +
always-fetch core, plus local), 'all'/'everything' (every
registered corpus + local), 'local', 'both' (mathlib + local),
a single corpus name (e.g. mathlib), or a comma-separated list
optionally including 'local' (e.g. mathlib,core).
--toolchain VERSION [--target mathlib] Lean version to fetch (e.g. v4.28.0).
Defaults to the contents of <folder>/lean-toolchain.
--commit SHA [--target local] Pin to a specific commit SHA. Default: walk
first-parent ancestors of HEAD until an artifact is found.
--ref REF [--target local] Resolve this ref (branch / tag) to a SHA and
walk its ancestors. Default: HEAD.
--repo OWNER/REPO [--target local] Override the owner/repo auto-detected from
`git remote get-url origin`.
--force Allow overwriting a newer existing local.db, and proceed even
when the worktree is dirty. For mathlib, re-download an
already-installed search_db.