Metadata-Version: 2.5
Name: isabelle-block
Version: 0.1.4
Summary: Mechanical block surgery on Isabelle theory sources: move, copy, delete, rewrite and substitute inside regions named by line span or by entry name.
Project-URL: Homepage, https://github.com/ott2/isabelle-block
Project-URL: Source, https://github.com/ott2/isabelle-block
Author-email: András Salamon <Andras.Salamon@st-andrews.ac.uk>
License: MIT
License-File: LICENSE
Keywords: afp,formal-verification,isabelle,isar,refactoring,theorem-proving
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development
Requires-Python: >=3.9
Requires-Dist: isabelle-layout>=0.2.2
Requires-Dist: isabelle-query>=1.1.1
Provides-Extra: test
Requires-Dist: pytest>=7; extra == 'test'
Description-Content-Type: text/markdown

# 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.**

```sh
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`](https://github.com/ott2/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

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

| verb | does |
|---|---|
| `move SRC:REGION before DEST` | relocate a block, within a file or between files |
| `copy SRC:REGION before DEST` | place a copy and keep the source |
| `delete FILE:REGION` | excise a block |
| `emit FILE:REGION` | print a block verbatim |
| `replace FILE:REGION NEWFILE` | swap a block for a file's contents |
| `sub OLD NEW FILE[:REGION]...` | literal substring substitution; OLD may span lines, and either side may be `@FILE` |
| `resub PAT NEW FILE[:REGION]...` | regex substitution; a match may span lines |
| `reargs 'F $1 $2' TMPL FILE[:REGION]...` | rewrite `F`'s applications by their (bracket-aware) arguments; skips prose |
| `split SRC 'NAME\|IMPORTS\|RANGES'... [--cut]` | cut a theory into several |
| `merge BASE.thy SRC.thy...` | splice theory bodies into one |

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](https://comby.dev) 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

```sh
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](LICENSE).
