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 [OPTION]... [SOURCE]...

Each SOURCE is a .thm or .thmod 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.
--strict-stratification	Treat stratification failures as errors.
--verbose	Set verbosity to at least 2.
--verbosity=NUM	Set verbosity to NUM.
--web=URL	Link theorem pages to Abella Web at URL.
--share=URL	Upload the project to the ZIP Worker at URL.
--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.

--web defaults to https://abella-prover.org/web/, and --share defaults to https://zips.abella-prover.org/. Passing an empty value removes the corresponding button from the generated pages.

Outputs

For each source type abella_doc produces the following files.

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

file.html embeds the source text and the annotation JSON, and renders the proof trace interactively. For a .thmod file it also highlights the module commands. 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 or .thmod file, abella_doc reads its Specification, Import, and Import Module commands and recursively processes the files it depends on. The output order is topological, so a specification or module 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 follow the operating system color scheme by default and remember an explicit light or dark choice in local storage. They do not depend on the scripts or fonts of the surrounding documentation site.

The --web option adds a link from each theorem page to Abella Web, and --share adds an Edit button that uploads the project to a ZIP Worker.

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

Document a module, enforcing strict stratification:

$ abella_doc --strict-stratification List.thmod

Related tools

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