Preparation

Abella can be used in two modes: online and offline.

Online

  1. Go to http://abella-prover.org/tutorial/try with a modern Web Browser.
  2. Make sure JavaScript is enabled.
  3. There is nothing to install or configure! Abella will run completely inside your Browser.

Offline

You will need to have a working OCaml toolchain, preferably managed with the help of OPAM. Follow these steps to install Abella:

  1. Run the command opam install abella to install Abella in `opam config var bin` (which should be in your $PATH).
  2. Optional but recommended: If you want ProofGeneral support for Abella, then:
    1. Download and install ProofGeneral. Abella is only compatible with development versions with version numbers beginning with 4.3pre.
    2. Navigate to your ProofGeneral installation.
    3. Create a subdirectory abella from the topmost directory of the ProofGeneral installation.
    4. Copy the files `opam config var share`/abella/emacs/pg/*.el to that abella directory.
    5. Run M-x customize-variable proof-assistant-table from within Emacs and add the entry (abella "Abela" "thm") to the list.
      If this variable is not customizable, you need to make sure that ProofGeneral/generic is in your load-path and then eval (require 'proof-site).
    6. Restart Emacs.

Content

Links