isar-tools

Source tooling for Isabelle/Isar projects: a formatter, project and source checks, and statistics. Pure Python. Works on .thy and ROOT files without running Isabelle.

Status: pre-alpha. See CHANGELOG.md and docs/PLAN.md.

Install

pip install isar-tools          # or: uv tool install isar-tools, pipx install isar-tools
isar --help

Python 3.11 or newer; no runtime dependencies. A conda-forge package (pixi global install isar-tools) follows the first PyPI release.

Commands

A path is a project directory, read like isabelle build -D (its ROOT, and ROOTS recursively), or a .thy file. Commands that read a project default to the current directory.

Exit status: 0 success, 1 findings or differences, 2 invalid invocation or unreadable input. Data goes to stdout, diagnostics to stderr. JSON and CSV output use stable snake_case keys and are never coloured.

Formatting

isar fmt                          # format every .thy below the current directory
isar fmt --check                  # list files that would change; exit 1 if any
isar fmt --diff Foo.thy           # show the change without writing
isar fmt --max-line-length 100    # also wrap long lines
isar fmt -                        # stdin to stdout, for editors

The formatter only changes layout. It never changes a token, never touches the space between two tokens on a line, and never rewrites strings, cartouches, comments, or ML. By default it only indents lines that are too shallow for their proof structure; --normalize sets indentation exactly. See docs/FORMATTER.md.

As a git hook with lefthook:

pre-commit:
  jobs:
    - name: isar-fmt
      glob: "*.thy"
      run: isar fmt {staged_files}
      stage_fixed: true

Checks

isar check                        # groups project, proofs, and syntax
isar check symbols src/           # non-ASCII characters outside comments
isar check docs src/              # theories, headings, locales, classes without a text block
isar check locales -d ~/afp/thys  # free variables in locale headers
isar check --ignore oops --format json

Project checks run for directory arguments only. isar check --help describes every code.

locales is heuristic. Inside the terms of a locale or context header, Isabelle reads an unknown identifier as a free variable and generalizes over it, so an assumption citing a deleted or misspelt constant still builds. The check reports identifiers that are no parameter of the header (its fixes, for clause, defines, or those of the locales it extends, resolved through imports), not bound in the term, and not used anywhere else in the project or in the -d theories it imports. Only names of at least four characters with an underscore (or \<^sub>) are reported; --allow NAME (repeatable) accepts a name. Inner syntax is approximated lexically: see isar_tools/checks/locales.py.

Commands of other sessions

Whether a word is an Isar command depends on the theories a file imports. The built-in table covers Pure and HOL, and commands declared in the theory headers of the project are found automatically. For commands of other projects, such as AFP entries, pass their directory with -d, as with isabelle build -d:

isar check -d ~/afp/thys .
isar project hierarchy --root numeric_domain -d ~/afp/thys --format json

Names

isar project names --kind locale                  # every locale, as Theory.locale
isar project names --format markdown > NAMES.md   # an index with docstrings
isar project names --name Foo.loc.bar_lemma       # exit 1 if no such declaration

Names are qualified as Isabelle renders them: a lemma inside context loc is Theory.loc.name. With --name, a qualifier naming the wrong scope does not match, and the error suggests the names that exist, so links into rendered theories can be checked without building them. The docstring is a text block directly before the declaration.

Quoting declarations

isar project extract combine_env locale_name.lemma_name
isar project extract --manifest snippets.toml --out generated/ --write   # regenerate
isar project extract --manifest snippets.toml --out generated/ --check   # diff; exit 1 on drift

A name is name, locale.name, Theory.name, or Theory.locale.name, and must identify one declaration; its source is the command and, for a goal, its proof. A manifest lists names as TOML tables, so a document that quotes a definition fails its check when the definition changes or is renamed:

[snippets.combine_env]
why = "shown in chapter 3"     # free text, ignored
[snippets.succ_pos]
file = "src/B.thy"             # choose between declarations of the same name

Statistics

isar stats                               # sessions, then the largest theories
isar stats proofs --top 10               # the longest proofs
isar stats style --max-line-length 100   # long theories, long lines, sorry, watched methods
isar stats build build.log --budget HOL-Library=0

Limits

• Nothing runs Isabelle, so nothing is type-checked or proved. A formatted file is guaranteed to contain the same tokens; building it is the project's CI's job.
• The built-in command table is hand-written. A command of a session that is neither built in nor passed with -d is read as part of the previous command.
• project extract finds names that commands declare; derived names (foo_def, foo.simps) and names made by interpretations are not found.
• project hierarchy follows declared parents, not sublocale, subclass, or interpretation.
• stats build reads one log line format, observed in Isabelle2025 logs.

Development

Requires pixi.

pixi run pre-commit-install  # git hooks
pixi run test
pixi run coverage            # 100% line and branch coverage required
pixi run typecheck           # pyright, strict
pixi run lint
pixi run isar --help
pixi run demo                # re-record docs/demo/demo.gif with VHS
pixi run demo-check          # run the demo commands without recording
ISAR_CORPUS=~/afp/thys pixi run corpus   # integration tests over real projects

Expected output lives in golden files under tests/golden/ and tests/formatter/. UPDATE_GOLDEN=1 pixi run test rewrites them, so a change in output shows up as a diff in review.

The demo GIF is generated by VHS from docs/demo/demo.tape, which runs the real commands on the small project in docs/demo/project. The demo task uses its own pixi environment, so VHS, ttyd, and ffmpeg stay out of the default one.

License

MIT