abella

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

Synopsis

abella [OPTION]... [FILE]

FILE must end in .thm or .thmod. 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	Deprecated; the argument is ignored.
-f FLAGS, --flags=FLAGS	Set flags from a comma-separated list.
-i	Deprecated; does nothing.
-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.
--strict-stratification	Treat stratification failures as errors.
--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.

The -i option is deprecated in favor of a frontend such as Abella Web. The -c option is ignored: the compiled artifact always goes to its default location.

Batch mode

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

$ abella foo.thm
$ ls foo.thc
$ abella foo.thmod
$ ls foo.thmodc

The compiled artifact is always written to its default location. The -c option is deprecated and its argument is ignored. 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 or Import Module with an out-of-date or missing compiled file, it recompiles the imported development first. The -N option disables this and requires the .thc and .thmodc files to be current.

Interactive mode

With no file argument, Abella starts a session:

$ abella
Welcome to Abella 2.1.0-dev

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. The -i option is deprecated and does nothing.

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. A .thmod artifact also records the module declarations. Compiled developments are imported with Import or Import Module. 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 or .thmodc files by hand.

Related tools

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