Abella can be used in two modes: online and offline.
with a modern Web Browser.
- There is nothing to install or configure! Abella will
run completely inside your Browser.
You will need to have a
working OCaml toolchain,
preferably managed with the help
of OPAM. Follow these
steps to install Abella:
- Run the command
opam install abella to
install Abella in
`opam config var bin`
(which should be in your
- Optional but recommended: If you
support for Abella, then:
and install ProofGeneral. Abella is only
compatible with development versions with version
numbers beginning with
- Navigate to your
- Create a subdirectory
abella from the
topmost directory of the ProofGeneral installation.
- Copy the files
`opam config var
proof-assistant-table from within Emacs and
add the entry
(abella "Abela" "thm") to
If this variable is not customizable, you need to make
ProofGeneral/generic is in
load-path and then eval
- Restart Emacs.
- Slides (PDF) from the presentation