abella_doc

abella_doc generates HTML pages from Abella sources. The pages show a development beside a browsable proof trace, with syntax highlighting.

Synopsis

abella_doc [--abella=CMD] [-r] [--verbose] [OPTION]... [SOURCE]...

Each SOURCE is a .thm file or a directory. Directories are processed only with -r.

$ abella_doc eval.thm
$ abella_doc -r examples

Options

Option	Meaning
-a CMD, --abella=CMD	Run CMD instead of abella.
-r	Process directories recursively.
--verbose	Print the files that are read and written.
--help[=FMT]	Show help in a given format.

The FMT of --help is one of auto, pager, groff, or plain.

-a overrides the ABELLA environment variable. When neither is given, abella_doc looks for an executable named abella, abella.exe, or abella.bc in the directory containing abella_doc.

Outputs

For each source type abella_doc produces the following files.

Source	Outputs
file.thm	file.html, file.json
file.sig	file.sig.json
file.mod	file.mod.json, file.lp.html

file.html embeds the text of file.thm and the annotation JSON, and renders the proof trace interactively. file.lp.html shows the signature and module of a specification side by side.

The annotation JSON is produced by running Abella in annotation mode:

abella --non-recursive --annotate --output=file.json file.thm

The .sig.json and .mod.json files are produced by parsing the source directly. They record the source ranges of declarations and clauses.

Dependencies

Before processing a .thm file, abella_doc reads its Specification and Import commands and recursively processes the files it depends on. The output order is topological, so a specification is documented before any development that uses it.

A .mod file requires a matching .sig file in the same directory. A relative path is expected; absolute paths are rejected for specifications.

When processing a directory, abella_doc ignores the directories node_modules, build, dist, css, and js. Other files are processed only if they have a recognized suffix.

Clause names

A clause may carry a %:name: annotation on the line before it. The generated pages use the name to label the clause and to improve error messages.

%:abs-typing:
of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).

The annotation is optional. It has no effect on proof checking.

Self-contained output

Each generated page embeds its stylesheet and scripts, so it can be published as a static file without serving extra assets. The pages do not depend on the scripts or fonts of the surrounding documentation site.

Examples

Document a single development:

$ abella_doc examples/lambda-calculus/eval.thm

Document every development under a tree:

$ abella_doc -r examples

Use a specific Abella executable and show progress:

$ abella_doc --abella=/usr/local/bin/abella --verbose eval.thm

Related tools

• abella runs the proofs.
• abella_dep generates a Makefile for incremental builds.