isar-tools

Linting, formatting, and project analysis for Isabelle/Isar. Pure Python: it reads .thy and ROOT files the way isabelle build finds them, without running Isabelle, and answers in seconds.

Why

Isabelle checks that every proof goes through. It has nothing to say about a lemma no proof cites, an import another import already brings in, a constant written out next to the notation the project gave it, a locale assumption no proof uses, or a sorry left in a theory nobody builds. In a development of a few hundred theories these pile up, the build slows down, and reviewers check style by eye. Other languages have formatters, linters, and dead-code finders for this. Large Isabelle projects mostly have conventions in a README.

isar-tools is that missing tooling: a formatter that only touches layout, about fifty checks, statistics, and views of a project's sessions, theories, and declarations. It fits a pre-commit hook or a CI job next to the build.

Status: alpha. Published on PyPI and conda-forge and used by a real project; minor versions may still add commands and JSON columns. 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.

Checks

isar check                           # groups project, proofs, and syntax
isar check notation unused src/      # name more groups to run them
isar check --ignore oops --format json

A tour, from docs/showcase/Tour.thy:

theory Tour
  imports Base
begin

text \<open>A few findings of \<^verbatim>\<open>isar check\<close>.\<close>

lemma join_comm: "a \<squnion>\<^sub>m b = b \<squnion>\<^sub>m a"
  by (simp add: join_def)

lemma join_comm_again: "x \<squnion>\<^sub>m y = y \<squnion>\<^sub>m x"
  by (simp add:)

lemma join_idem: "join a a = a"
  apply (simp add: join_def)
  done

lemma join_bound: "a \<le> a \<squnion>\<^sub>m b"
  sorry

end

$ isar check proofs notation methods redundant Tour.thy
Tour.thy:10:7: duplicate-lemma: join_comm_again states join_comm (Tour.thy:7) again
Tour.thy:11:12: empty-modifier: add: lists nothing
Tour.thy:13:19: spelled-out-notation: join is written out; its notation is _ \<squnion>\<^sub>m _
Tour.thy:14:3: single-apply: one apply and done: write by
Tour.thy:18:3: unfinished-proof: sorry leaves the goal unproved

docs/CHECKS.md explains every group and shows an example of every code, generated from the showcase project. A comment (* isar-ignore: CODE *) silences a finding on its line, or on the next line when it stands alone.

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

Project views

isar project graph --layers          # sessions as strata
isar project names --format markdown > NAMES.md
isar project extract --manifest snippets.toml --out generated/ --check
isar project notation notation.toml --out gen/notation.json --check

docs/PROJECT.md describes session layers, names, quoting declarations, notation tables, anchors of a build, and commands of other sessions (-d).

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, leaf-sessions
retired-file = "retired_identifiers.txt"      # also: retired = ["name", ...]

[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
pixi run checks-doc          # regenerate docs/CHECKS.md and the README's check sections
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