Skip to main content
Version: 2.1.0-dev

Tools

Abella ships with three command-line programs.

  • abella runs developments in batch mode or starts an interactive session.
  • abella_doc generates HTML pages from Abella sources.
  • abella_dep generates a Makefile from the dependencies between developments.

All three are distributed together and use the same version number. They share the ABELLA environment variable, which names the Abella executable to invoke.

A typical build​

Compile the examples and generate their documentation:

$ abella_dep -o Makefile -r examples
$ make -j
$ abella_doc -r examples

abella_dep records which .thm and .thmod files depend on which specifications, developments, and modules. make then recompiles only what changed. abella_doc produces the HTML traces next to the sources. Neither tool edits the sources.

Exit status​

abella exits with status 0 when a development is processed successfully and 1 when an error occurs. abella_doc stops at the first failing Abella invocation and reports the command that failed. abella_dep reports malformed inputs and circular dependencies.

Editors​

A fork of ProofGeneral with Abella support is maintained in the PG repository. Check out its abella branch and load it from your Emacs configuration.

The fork provides proof navigation for .thm files and a major mode for .sig and .mod files. The important commands are:

  • C-c C-RET processes the script up to the cursor;
  • C-c C-n processes the next command;
  • C-c C-u undoes the last command.

ProofGeneral for Abella requires a graphical Emacs; the C-RET key binding is not available in most terminal emulators.

Abella Web​

The Abella source distribution includes Abella Web, a browser-based frontend. A public instance is available at abella-prover.org/web. See web/README.md in the distribution for instructions on running a local server. The -i option of abella is deprecated; Abella Web is the recommended interactive frontend.

Getting the tools​

The tools are built from the Abella source repository with Dune. See the upstream README for build instructions and platform requirements. The documentation on this site describes the behavior of the programs, not how to install them.

See also​