← Command reference · CLI overview

lean-pkg search

prior-art search over claims, the index and public sources.

Usage

lean-pkg search [--package PACKAGE] [--offline] [--loogle] [--loogle-query PATTERN]
                [--require-complete] [--cache-dir DIR] [--sources a,b,c] [--index INDEX]
                [--record] [--repo DIR] [--agent AGENT] [common flags] TERM

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Prior-art search. Packages without synced claims are searched by declaration (fully qualified names; accents folded). A source that skipped, failed in part, listed fewer matches than it found or could not read everything makes the search incomplete (complete: false): a zero there is not an absence.

Arguments and flags

Argument or flag	Description
TERM	what to look for (quote a phrase)
--package PACKAGE	the registered package this search is for (it labels the output; every package’s claims are still searched)
--offline	skip every network source
--loogle	send the term to Loogle even when it reads as natural language (by default only declaration/type patterns go to Loogle)
--loogle-query PATTERN	send PATTERN to Loogle instead of the term (a Lean name, term or pattern such as ‘Real.exp’ or ‘?a * ?b = ?b * ?a’); the other sources still get the term
--require-complete	exit 1 when the search is incomplete (a source skipped, failed in part, capped, or read only part of what it should); the output is printed in full first
--cache-dir DIR	use DIR as the lean-pkg cache for this search (Palomar snapshots, Reservoir index) instead of $XDG_CACHE_HOME/lean-pkg or ~/.cache/lean-pkg
--sources a,b,c	subset of: registry,index,loogle,leansearch,reservoir,palomar,github (order is fixed)
--index INDEX	index root (default: $LEAN_PKG_INDEX, else ./index)
--record	write docs/prior-art/<date>-<slug>.md in the package checkout (or –repo-dir) and a prior-art-searched event
--repo DIR	research repository for –record (old spelling –repo-dir, kept working)
--agent AGENT	with –record: the agent acting (recorded as the event’s actor); another agent’s live lease on –package then refuses

Details

Form	What it does	Key flags
search TERM	prior-art search in the fixed order registry, index, loogle, leansearch, reservoir, palomar, github; each source ok or skipped: <reason>; the registry source scores each package’s name (exact name 3), notes, owner_project and repo as well as its cached claims, and every local hit carries hit_kind (package or claim) and repo; a package without synced claims (no cached claim: claims coverage empty, unsynced or none) is searched by declaration instead: git grep over the tracked *.lean files of its checkout at HEAD, every query word (case- and accent-insensitive on both sides: ito finds Itô; file names with non-ASCII characters are searched) in a theorem|lemma|def|structure|class|instance|abbrev|inductive|axiom|opaque|irreducible_def name or its /-- -/ docstring (a scanner that skips block comments, line comments and strings and reads attributes, modifiers, instance (priority := n), class inductive and «» names), decl the fully qualified name (namespace/section/end tracked; a dotted query such as DemoA.heatFlowMass_le is matched against it, a plain query against the name as written), at most 10 listed per package (the rest counted as declaration_hits_omitted), reading at most 2000 candidate files per package; a package past that file cap, or with candidate files that could not be read, is listed in coverage.declaration_files_capped[] {package, candidates, inspected, unreadable}, named on the coverage line, and makes the search incomplete (the registry block’s incomplete says why, truncated_sources: ["registry"], complete: false); an index entry that cannot be read (invalid YAML, not UTF-8) is counted in the index block’s reason and incomplete and makes the search incomplete too (truncated_sources: ["index"]); the --record page then marks such a source incomplete: in its Sources table, never words it Not found in, and names it in a Not fully searched sentence; hit_kind: declaration (unclaimed), trust none, file as PATH:LINE, pin the HEAD commit, ranked after the claim and package hits; a registered package whose checkout lies inside another’s is scanned only as itself (the outer package’s scan excludes it); a package without a git checkout is not searched; when any source was skipped, the line just before consulted: reads incomplete: searched N of M sources; skipped: A, B; a zero here is not a negative result, and --json always carries complete (no source skipped or truncated), searched and skipped_sources[]; a source that answered with a part failed (GitHub’s code or repository search) stays ok but lists the part in its block’s partial[], is added to truncated_sources and makes the search incomplete (incomplete: github: code search failed; ...); a part that returned exactly its result limit (GitHub’s --limit 30, no paging) lists the part in the block’s capped[] with cap_limit (distinct from partial[], which means failed), is added to truncated_sources too (incomplete: github: code search returned its 30-result limit; ..., consulted: ... github (capped, 30 hits)); a source that found more matches than it lists (Palomar and Reservoir list 30, Loogle 20) reports capped: ["results"] with cap_limit (the number listed) and total (the number found) and is truncated the same way (incomplete: palomar: 50 matches found, first 30 listed), and the --record page marks it capped: ... in its Sources table with an Incomplete: ... more matches may exist than the ones listed. sentence; the registry coverage line before that names the blind sources (registry coverage: 26 of 31 packages have no synced claims: 24 searched by declaration only, 2 not searched (no checkout: ...)), grouped by reason when several apply (no path: A; no checkout: B; no git HEAD: C; scan error: D), and --json carries coverage (claims, declaration_only, not_searched[] (names, as before), not_searched_reasons[] {package, code: no-path	no-checkout	no-git-head	scan-error, remedy} whose remedy names only read-only commands keyed by the package name, never a host path, declaration_hits_omitted; null when the registry was skipped); exit 0 even with zero hits; the term is routed by shape: a Lean declaration or type pattern (signature) goes to Loogle, natural language (natural-language) skips Loogle with the reason natural-language query; Loogle takes declaration patterns — try e.g. ... and still runs every other source; --loogle forces Loogle; --json carries route at the top and on every source; after --record writes the page in a repository with an mkdocs.yml (or mkdocs.yaml) it prints note: <path> is new; a strict MkDocs build needs a nav entry (or a literate-nav glob) for it and --json carries nav_hint (path, reason); without one there is no note, nav_hint is null and record.mkdocs is false; mkdocs.yml is never edited; --loogle-query PATTERN sends PATTERN (a Lean name, term or pattern) to Loogle instead of the term, whatever the route, and every other source still gets the term (--json loogle_query); a Loogle parse error (“Unknown identifier …”) is skipped with a reason that says to pass the Lean part that way; --require-complete exits 1 when complete is false, after printing the full output (--json ok: false and error); a scan-error entry carries detail (git grep exit 128: <fixed cause> or git grep killed by signal N, never git’s stderr), also shown on the coverage line; an online search refreshes the Palomar snapshot and Reservoir index cache under $XDG_CACHE_HOME/lean-pkg even without --record (never the registry): each block’s cache_writes[], --json cache {root, writes[]} and a cache: wrote ... line say so, and --cache-dir DIR keeps that search’s cache in DIR; see Prior-art search	[--package NAME] [--offline] [--sources a,b,c] [--loogle] [--loogle-query PATTERN] [--require-complete] [--cache-dir DIR] [--record] [--repo-dir PATH] [--index PATH]

Exit codes

0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.