Metadata-Version: 2.5
Name: isabelle-query
Version: 0.7.0
Summary: Query the live theory index of an Isabelle/Isar project — entries, call graph, dependencies, and dead code — by parsing .thy files on every invocation.
Project-URL: Homepage, https://github.com/ott2/isabelle-query
Project-URL: Source, https://github.com/ott2/isabelle-query
Author-email: András Salamon <Andras.Salamon@st-andrews.ac.uk>
License: MIT
License-File: LICENSE
Keywords: afp,formal-verification,isabelle,isar,proof-engineering,theorem-proving
Classifier: Development Status :: 4 - Beta
Classifier: Environment :: Console
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Programming Language :: Python :: 3.14
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Quality Assurance
Requires-Python: >=3.9
Requires-Dist: isabelle-layout>=0.2.2
Description-Content-Type: text/markdown

# isabelle-query

`query` is a command-line tool for **querying an Isabelle/Isar project** — its
entries (definitions, lemmas, theorems, datatypes), call graph, theory
dependencies, outstanding `sorry`s, dead code, and the shape of its proofs.

It parses the project's `.thy` sources on every invocation, so results always
match the current tree: **no Isabelle build, no proof replay**. A large project
parses in a fraction of a second, and the whole AFP in a couple of minutes. It is
aimed at projects big enough that grep-and-examine has stopped working — AFP
entries, the AFP itself, or industrial verification.

Pure Python. One runtime dependency,
[isabelle-layout](https://pypi.org/project/isabelle-layout/) — the ROOT and
theory-header parser, split out so that reading an Isabelle project's structure
does not require installing a CLI. `pip` fetches it for you.

## Commands

```sh
query summary              # theory overview table (-S: corpus/session aggregate)
query theory MyTheory      # entries in a theory (-n for terse names)
query find <regex>         # search entry names (--statement: search statements; --and: all patterns)
query show <name>          # a named entry's declaration + body
query enclosing FILE:LINE  # which entry + proof block owns a line; inverse of outline
query callers <name> [-r]  # who references a name  (reverse; -r = transitive)
query callees <name> [-r]  # what a name references (forward)
query deps <theory> [-r]   # what a theory imports  (forward; reverse: uses)
query refs <theory>        # what a theory cites, by owning theory (citation-level)
query graph [citation|imports]  # the whole graph as JSON (-f dot for Graphviz)
query sorry                # outstanding sorry's
query unused               # dead-code / unused-entry analysis
query shape <view>         # proof-shape metrics (summary|steps|lemma|widest|census)
```

Every subcommand takes `-h`; `query -h` lists all 20.

## Examples

Point `query` at any session directory with `-R` (or `--root`):

```sh
query -R AFP/thys largest                          # the biggest entries, by line count
query -R AFP/thys callers metric_domain_tfin_def   # every proof step that cites a fact
query -R AFP/thys find --statement tfin            # lemmas *stated about* tfin, whatever their name
query -R AFP/thys find --statement --and length tfin  # ...and mentioning length too (--and intersects)
query -R AFP/thys enclosing Tfin.thy:412           # the lemma and nearest proof block a build error sits in
query -R AFP/thys enclosing Tfin:88..140           # every entry a diff hunk touches
query -R AFP/thys grep simp Tfin.thy:88..140       # search just a hunk
```

Locations and spans share one grammar (`theory:line`, `theory:A..B`), so the
tool's output is valid input: a locus from `callers` / `sorry` pastes into
`enclosing`, and a span from `outline` / `largest` — or a proof block from
`enclosing`'s own drill-down (`▸ have key 11..14`) — pastes into `lines`.

## What it reads

Only **live Isar text**. A name in a comment, a `\<comment>` note, a `text`
block or an `ML` body is not a citation, so it never invents a caller or hides a
dead lemma — and a `definition` left behind in a comment is not an entry.
Regions are found by a character-level scan, not by line, so
`by (simp add: foo) (* not bar *)` keeps `foo` and drops `bar`.

Layout carries no meaning: Isar is whitespace-insensitive, so a declaration is
recognised wherever a *command* can start, at any indentation and any block
depth. Discovery loads what `isabelle build` compiles — each session's declared
theories plus the closure of their in-entry imports.

See **[SCANNING.md](SCANNING.md)** for the details: locale scope, method names
that collide with fact names, corpus aggregation, and the prose view.

## Proof-shape metrics

`query shape` measures the shape of individual proof steps — how big a step is,
how deeply nested, how many facts it holds at once, how much is re-said, and how
it is discharged. All source-level, no build.

```sh
query shape summary                  # per-theory aggregate table
query shape lemma <name>             # one proof: every step
query -R AFP/thys shape census       # per-proof JSONL over a whole corpus
```

See **[METRICS.md](METRICS.md)** for the command reference, the metric table, and
the JSONL record schema.

## Exit status

`0` the command ran; `1` the request could not be resolved (unknown theory or
path, no subcommand); `2` bad usage — an argparse error, or **a root that could
not be read**; `141` a downstream reader closed the pipe (`query shape census |
head`), as a shell reports for SIGPIPE.

A root that yields no theories is reported on stderr and never as an empty
success, so a script can tell a broken run from an honestly empty one:

```
$ query -R /typo/path shape census
query: /typo/path: no such directory (given to -R/--root)
$ echo $?
2
```

## Installation

Requires Python 3.9 or greater. Installs the command on your `PATH` under two
names — **`query`**, the short form used throughout these docs, and
**`isabelle-query`**, matching the distribution — and pulls `isabelle-layout`
from PyPI. They are the same program, and it reports whichever you typed, so
`isabelle-query -h` documents `isabelle-query`.

```sh
pip install isabelle-query     # from PyPI
pip install .                  # from a checkout
```

An editable install, for working on the tool itself:

```sh
git clone https://github.com/ott2/isabelle-query
cd isabelle-query
python -m venv .venv && source .venv/bin/activate   # optional but recommended
pip install -e .
```

## Documentation

| file | what |
|---|---|
| [SCANNING.md](SCANNING.md) | how `query` reads a project — what counts as a declaration, a citation, and a session |
| [METRICS.md](METRICS.md) | `query shape` command reference and metric definitions |
| [CONTRIBUTING.md](CONTRIBUTING.md) | the CLI contract and where design decisions are recorded |

## Authors & license

By András Salamon, with Claude Opus 4.6, 4.7, 4.8, and 5. [MIT](LICENSE).
