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

pixi global install isar-tools  # or: conda install -c conda-forge isar-tools
pip install isar-tools          # or: uv tool install isar-tools, pipx install isar-tools
isar --help

Python 3.11 or newer; no runtime dependencies. In a pixi project: pixi add isar-tools.

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 leftovers hygiene src/ # sledgehammer, thm, nitpick without expect; tabs, CRs
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, commands declared in the theory headers of the project are found automatically, and a generated table covers the commands of AFP entries (such as derive from Deriving), so no AFP checkout is needed. For commands of other projects, or of an AFP newer than the table, 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
isar project names --derived                      # also f_def, f.simps, L.intro, q.fact

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 commands --by theory --format json   # command counts per theory
isar stats build build.log --budget HOL-Library=0
isar stats build build.log --budget TD=8 --default-budget 0 --project .  # every other library: 0

Configuration

Options a project always wants go in [tool.isar] in pyproject.toml, or in an isar.toml (same keys, at the top level). The file is found by searching upward from the working directory.

[tool.isar]
include = ["$AFP", "vendor/td-verification"]  # like -d; skipped with a note if absent
exclude = ["src/**/generated/**"]             # like --exclude

[tool.isar.fmt]
max-line-length = 100    # also: indent, max-blank-lines, normalize

[tool.isar.check]
groups = ["project", "proofs", "syntax"]      # also: ignore, allow

[tool.isar.stats]
max-line-length = 100    # also: watch

Paths and globs are relative to the file. Command-line options win; -d and --exclude add to the lists, and --max-line-length 0 turns configured wrapping off. A glob excludes matching files and everything below matching directories, also when a file is named on the command line (as a git hook does).

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, and the AFP table is generated from one AFP revision (scripts/gen_afp_commands.py). A command of a session that is in neither and not passed with -d is read as part of the previous command.
• project names --derived adds the usual derived facts (f_def, f.simps, P.intros, t.inject, L.intro, ...) and the facts of qualified theory-level interpretations (q.fact), from the interpreted locale's own facts only; facts a locale inherits, and names made by other packages, are not listed.
• 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.

Releasing

1. Check that formatting cannot break a build: format a real project with the release candidate and build it with Isabelle (for Voblint, its isar fmt round trip workflow or the same steps locally).
2. In CHANGELOG.md, rename ## Unreleased to ## X.Y.Z (YYYY-MM-DD) and merge.
3. Tag the merge commit and push the tag (git tag -a vX.Y.Z -m "isar-tools X.Y.Z", git push origin vX.Y.Z). The Build workflow takes the version from the tag and publishes to PyPI; the conda-forge feedstock's bot opens the update.

License

MIT