isabelle-block

Mechanical edits to regions of Isabelle theory files, where a region is named by a line span or by the name of a lemma.

block move Foo.thy:helper_lemma before first_user     # hoist a helper
block delete Foo.thy:dead_lemma
block move Foo.thy:1669..2657 before Bar.thy:46       # between theories
block reargs 'cost $1 $2' 'Suc (len $1)' Foo.thy --expect 14

Name addressing is the reason to use it. Foo.thy:helper_lemma resolves, through isabelle-query's parser, to the lemma's span, from its doc block through the last line of its proof. So an edit needs no line arithmetic, and it cannot go stale between looking a lemma up and editing it.

Install

python3 -m pip install isabelle-block

This puts block on your PATH. Needs Python 3.9 or later; depends on isabelle-query and isabelle-layout, which pip fetches from PyPI. It needs no Isabelle process.

Verbs

A REGION is A..B (or A-B), a single line N, an entry NAME, or all, which is also what a bare FILE means. A DEST is LINE, NAME, FILE:LINE or FILE:NAME; the block lands immediately before it, preamble included.

Modifiers:

• --dry-run reports the edit and writes nothing.
• --expect N makes sub, resub and reargs refuse unless exactly N substitutions are made.
• --except NAME leaves an entry out of every region.
• --no-preamble starts a resolved span at the entry, not its doc block.
• --with-preamble keeps the doc block even when it sits directly under a section heading. Such a text may introduce the section rather than document the entry, and the source cannot say which. So there, delete, move and replace refuse until you choose one of these two flags.
• --keep-heading / --with-heading: deleting the only entry under a heading refuses until you say whether the heading stays (bare) or the whole section goes with the entry.
• --land-above-text / --land-below-text: a block moved or copied before NAME, landing under a heading, refuses when NAME's doc block sits directly under that heading, since the text may introduce the section. Say whether the block lands above the text or between it and NAME.
• --root DIR names the session root whose keyword table name resolution uses. By default it is discovered as query discovers it: an environment variable, a .isabelle-query marker, or the nearest ROOT. The table matters because a theory may use a command that another theory in its session declares.
• --no-trailing-blank cuts verbatim, without blank-line healing.

A refusal for want of a choice lists every open choice at once, so one rerun with a flag from each pair goes through.

A block moved before NAME that starts with its own heading, of the same or higher rank as the heading above NAME, lands above that heading. So it becomes a section beside NAME's, and does not swallow NAME.

block --help gives the full grammar, and block VERB --help gives one verb's.

Every run ends with an explicit PASS: or FAIL: line, and the exit status agrees. emit prints its PASS: on stderr, so block emit … > FILE is a clean copy. A refusal writes nothing.

Related tools

Editing by line span and plain substitution are what ed, sed, sd and fastmod already do. comby does bracket-aware rewriting much as reargs does. block is worth installing if your edits need what those tools cannot see:

• lemma names as addresses;
• the difference between Isar code and prose (text, headings, \<comment>);
• edits at theory level.

docs/related-tools.md compares them in detail.

Status

This is alpha, extracted from the NDTHT formalisation's bin/block.py, where it did the project's mechanical theory surgery. The planned verbs (rename, a caller-checked delete and an import-checked move) are in tasks.md.

Development

python3 -m venv .venv
.venv/bin/pip install -e '.[test]'
.venv/bin/pytest

Authors & license

By András Salamon, with Claude Opus 4.7, 4.8, 5, and 5.5. MIT.