abella

abella is the prover. It runs a development either in batch mode, reading a .thm file, or interactively, reading commands from the terminal.

Synopsis

abella [OPTION]... [FILE]

FILE must end in .thm. If it is omitted, Abella starts in interactive mode.

$ abella examples/lambda-calculus/eval.thm
$ abella

Options

Option	Meaning
-a, --annotate	Emit annotations as JSON instead of the usual output.
-c FILE, --compile=FILE	Write the compiled development to FILE.
-f FLAGS, --flags=FLAGS	Set flags from a comma-separated list.
-i	Switch to interactive mode after processing the input file.
-N, --non-recursive	Do not recursively invoke Abella for imports.
-o FILE, --output=FILE	Write all normal output to FILE.
-M	Deprecated and does nothing. Use abella_dep.
--verbosity=NUM	Set the trace verbosity. The default is 0.
--version	Print version information.
--help[=FMT]	Show help in a given format.

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

Batch mode

In batch mode Abella reads the whole .thm file and exits. By default it also writes a compiled development to the matching .thc file:

$ abella foo.thm
$ ls foo.thc

The -c option overrides the compiled path. In interactive mode the compiled development is not written to disk.

Normal output is written to standard output. Use -o to redirect it:

$ abella -o foo.out foo.thm

The exit status is 0 when the development is processed successfully and 1 when an error occurs.

When Abella encounters Import with an out-of-date or missing .thc file, it recompiles the imported development first. The -N option disables this and requires the .thc files to be current.

Interactive mode

With no file argument, Abella starts a session:

$ abella
Welcome to Abella 2.0.8.3

Abella <

Commands are entered at the Abella < prompt. The prompt changes to the name of the current theorem while a proof is in progress:

Abella < Theorem eval_det : forall E V1 V2,
...        {eval E V1} -> {eval E V2} -> V1 = V2.

============================
 forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2

eval_det <

The interactive commands #back and #reset undo the previous command and reset the session. They are not accepted in batch mode, and no state is saved between sessions unless a compiled development is produced with -c.

Flags

The -f option applies run-time options before reading any commands. Each entry has the form key=value, and entries are separated by commas. For example:

$ abella -f subgoals=on,witnesses=on,search_depth=10 foo.thm

A quoted value may be written after the =:

$ abella -f 'load_path="lib"' foo.thm

Unknown flags are silently ignored. The keys and values are the same as for the Set command; see the command reference.

Annotation mode

The -a option changes the output to a stream of JSON records. This is the mode used by abella_doc to produce the proof traces shown in generated HTML pages. The JSON schema is experimental and may change between releases. It is not intended for interactive use.

Compiled developments

A compiled development records the specification signature, the specification clauses, the definitions, and the proved theorems. It is imported by other developments with the Import command. See File structure for the compatibility rules.

Compiled files record the version of Abella that produced them, together with a digest of the executable. If the digest differs, importing recompiles the development and prints a warning naming the version that produced the file. Do not edit .thc files by hand.

Related tools

• abella_doc generates HTML pages from a development.
• abella_dep generates a Makefile from the dependencies between developments.