Library search

Use Search in the toolbar, or Ctrl/⌘ Shift F, to search bundled Cumulus and .g17 libraries loaded through Open .g17 or Open folder. Results include qualified names, source declarations, section assumptions, documentation, and source navigation. Copy name copies the qualified identifier. Escape closes; Arrow Down enters the results, and Tab moves through result actions.

Search is local and works offline after the workbench has been cached. It does not send source text to a search service. Imported files must be available in the bundle or loaded into the workspace; it does not crawl arbitrary disks or remote repositories. Workspace modules override bundled modules of the same name. Reopening Search synchronizes edits and removals.

Queries#

Criteria are conjoined. Quotes preserve whitespace. Prefix a criterion with - to exclude it. Matching is case-insensitive.

A value may follow its field after whitespace. After conclusion: or pattern: such a value runs to the next filter or the end of the query, so conclusion: ∈ ω is the conclusion criterion ∈ ω and conclusion: _ = 0 ∨ _ = 0 -module:Core is one conclusion pattern and an exclusion; after the other fields it is the next word. symbol: matches a complete source identifier or its qualified suffix, not a substring. module: and conclusion: use substring matching; name: matches the whole value as a substring, or its pieces split at _ in order, so name:mul_eq_zero finds mul.eq_zero_iff and integerMulValue.eq_zero while name:complexPolynomial.continuous stays a substring. A conclusion: value with a wildcard is matched as a pattern. pattern: uses token sequences with nonempty balanced spans for _ and named wildcards such as ?x. Repeated named wildcards must bind identical token sequences. Wildcards are local to each pattern criterion. Matching is syntactic, over the source text. It does not resolve overloads, identify alpha-equivalent expressions, unfold definitions, or infer carriers. Patterns are limited to 128 tokens, wildcard spans to 64 tokens, and query work to a fixed matching budget. When the budget runs out, search asks for another filter instead of returning a partial result set.

Results are source declarations. They say nothing about proof status: broken or admitted workspace declarations can appear. Autogenerated theorems without explicit source declarations are not indexed yet. Use proof checking and Axiom Audit for validity/dependencies. Existing exact?, apply?, and rw? perform checked goal-directed discovery inside proofs.

Design#

A dedicated worker keeps discovery independent of long-running kernel checks. The index uses trigram postings, intersects the rarest postings first, and verifies each surviving candidate against all criteria. Changed files replace their records and postings; unchanged files retain them. Query caches are bounded and invalidated on changes. Results are ranked deterministically: an exact short-name match first for a name or text criterion, and for a conclusion or pattern criterion the conclusion whose token shape is the value itself (parentheses around the whole aside), then shorter conclusions containing it before longer ones. The UI debounces typing, ignores stale replies, limits rendered results, and reports malformed or over-budget queries.

Limits#

Search matches source text. There is no elaborated structural index that resolves notation, alpha-equivalence, or carriers, and no natural-language retrieval. For goal-directed search over the elaborated environment, use exact?, apply?, and rw? inside a proof.