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: 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.

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 retired --retired-file retired.txt src/   # removed names that came back
isar check prose src/             # names cited in text blocks; raw _ that LaTeX rejects
isar check links site/index.html --browser-info browser_info   # links into HTML theories
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.

retired reports identifiers the project removed on purpose, listed in check.retired, in the file check.retired-file names (one per line, # comments), or with --retired NAME. Isabelle reads an unknown lowercase name in an assumption or a theorem statement as a free variable, so a locale whose assumption cites a deleted constant still builds and silently assumes less. Matching is whole-word outside (* *) comments, and foo_def, foo_def_raw, foo_axioms, and foo_axioms_def count as foo.

prose reads document text (text, section, ...). Isabelle checks \<^const>\<open>f\<close>, but not a plain nested cartouche such as \<open>f_def\<close>, which is how prose usually cites a lemma. A prose-reference is such a cartouche naming nothing the project or its -d directories declare (derived facts included) or use in their formal text; only names of at least four characters with an underscore are read, and --allow NAME accepts one. A prose-underscore is a raw _ in the outer prose, which reaches LaTeX unescaped and fails the document build.

links reads .html and .md files for links into Isabelle's HTML presentation, where each definition has an anchor such as Theory.loc.name|fact. With --browser-info DIR, a link into DIR (relative to the file, below a --link-base URL, or starting with a chapter directory of DIR) must name an existing page and anchor. Without a build, an anchor is compared with the declarations: it must start with its page's theory, and a name the theory declares once must carry its scope (Theory.loc.name, not Theory.name). project names --format json gives each declaration's anchor and its url below browser_info.

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

Session layers

isar project graph --layers                  # layer, session, and what it rests on
isar project graph --layers --format dot     # one rank per layer

A session rests on its parent, its sessions entries, and the sessions whose theories its theories import. Its layer is one above the highest of those (1 if it rests on no known session), so a drawing of the development as strata follows the ROOT files and imports. Sessions of -d directories that the project rests on are included; JSON adds layers and the imports edges.

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
isar project names "$ISABELLE_HOME/src/HOL/Orderings.thy"   # one theory file alone
isar project names --kind fact --statements --format json   # each lemma's statement

Names are qualified as Isabelle renders them: a lemma inside context loc is Theory.loc.name, and a datatype's constructors and selectors and a record's fields are named in their type (Theory.t.C). 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. JSON and CSV rows carry a constant's mixfix, its notation (the first string of the mixfix), and the syntax mode of abbreviation (input), for constants, record fields, constructors, and locale parameters, for clause included. The docstring is a text block directly before the declaration.

Quoting declarations

isar project extract combine_env locale_name.lemma_name
isar project extract --statement lemma_name     # without the proof
isar project extract "sign :: numeric_domain" sign_tf   # an instance, an interpretation
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, a class instance type :: class, or the qualifier of an interpretation (q for interpretation q: loc), and must identify one declaration. The project's declarations come first, then those of -d directories; a declaration hides the parameters, fields, and constructors that others have of the same name; its source is the command and, for a goal, its proof. With --statement it is the statement alone: no proof, and no begin of a locale, class, or instantiation. A manifest lists snippets as TOML tables, each written to KEY.thy, 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
proof = true                   # keep the proof, also with --statement
[snippets.succ_pos_short]
name = "B.succ_pos"            # what to extract, if not the key
[snippets.order]
file = "~~/src/HOL/Orderings.thy"   # Isabelle's own theories, below $ISABELLE_HOME

A ~~/ file is read below the ISABELLE_HOME environment variable and printed back as (* ~~/src/HOL/Orderings.thy *); without the variable, such entries are skipped with a note.

Notation

isar project notation notation.toml                                  # JSON to stdout
isar project notation notation.toml --out gen/notation.json --write
isar project notation notation.toml --out gen/notation.json --check  # diff; exit 1 on drift
isar project notation notation.toml --browser-info browser_info      # every anchor must exist

A document that explains a formalization shows its symbols, and a hand-typed table of them drifts from the theories. The manifest names the declarations and the argument names to show; the rest is read off each declaration:

[notation.widen]
args = ["a", "b"]                   # filled into the mixfix's _ slots, the rest applied after
reads = "a widened by b"            # anything else is ignored: keep your prose here
[notation.step]
name = "walk.step"                  # a NAME as extract takes it; default: the key
args = ["x", "y"]
[notation."walk.reach"]
file = "src/Walk.thy"               # choose between declarations of the same name

For fixes widen :: ... (infixl "\<nabla>" 65) in a class, the entry is

{
  "key": "widen",
  "name": "Lattice.widening_class.widen",
  "kind": "class_parameter",
  "command": "fixes",
  "scope": "global",
  "owner": "widening",
  "symbol": "a \\<nabla> b",
  "unicode": "a ∇ b",
  "printed": true,
  ...
}

with also theory, session, path, line, mixfix (as written), notation (its template, _ \<nabla> _ for an infix), args, mode (input or output of an abbreviation), expansion (an abbreviation's lhs and rhs), and the HTML anchors anchor, url, owner_anchor, and owner_url, as project names gives them. kind is the shape:

Isabelle never prints an abbreviation (input) back, so its printed is false. Any other declaration, such as a constant defined inside a locale (whose notation outside it takes the locale's parameters), a datatype constructor, or a binder or structure mixfix, fails with its location; so does a mixfix with more _ slots than args, and an abbreviation that is not one lhs \<equiv> rhs equation. Notation added later with the notation command is not read. Nothing is written while any entry fails.

With --browser-info, an anchor the sources cannot give is looked up in the build, as project anchors does: that of a theory no session owns, and that of an owner the project does not declare (context order begin gives HOL's order). --prefer chooses between rival definitions there.

Anchors in a build

isar project anchors --browser-info browser_info --format json      # every anchor
isar project anchors --browser-info browser_info lfp "order|locale" # by name
isar project anchors --browser-info browser_info --kind fact --kind thm sound \
  --prefer MyChapter/ --prefer HOL/HOL/

project names gives the anchors of the project from its sources. A build also holds those of HOL and of every library session it rendered. A NAME is any dotted suffix of an anchor (loc.name, name), or Theory.name for a member of a locale or type when no suffix matches, with |kind or --kind (tried in order) to choose the kind. The ids of one definition count once: a lemma's fact and thm, a class's locale and class, and T.c.x and T.c_class.x. A copy of another session's theory (Owner.Theory.html) is skipped. A name that matches several definitions, such as a constant two locales declare or a fact an interpretation copies, is an error that lists them; --prefer PREFIX (repeatable, first is best) keeps the definitions on pages below the first prefix that has any.

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
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
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