Skip to main content
Version: 2.0.8

Installation

Abella is distributed as an OCaml package and is installed with opam. Installing the package provides the abella, abella_doc, and abella_dep executables.

Requirements​

  • opam 2.1 or later.
  • An OCaml switch supported by the 2.0.8 package: OCaml 4.12.0 up to, but not including, OCaml 5.5.
  • Dune 3.11 or later, installed automatically by opam.

If your current switch uses a different OCaml version, create a dedicated switch. For example:

$ opam switch create abella-2.0.8 5.4.0
$ eval $(opam env --switch=abella-2.0.8)

Install from OPAM​

The 2.0.8 series is available from the default OPAM repository:

$ opam install abella

This installs the latest packaged release in the series, currently 2.0.8. Check the installation:

$ abella --version

Run opam show abella to inspect the package metadata and the exact dependency constraints for your repository snapshot.

Install the 2.0.8.3 patch release​

These pages document the 2.0.8.3 patch release. To install exactly that revision, pin the tagged sources from the Abella repository:

$ opam pin add abella \
    https://github.com/abella-prover/abella.git#v2.0.8.3

Alternatively, clone the tag and pin the local checkout:

$ git clone --branch v2.0.8.3 --depth 1 \
    https://github.com/abella-prover/abella.git
$ cd abella
$ opam pin add abella .

The 2.0.8.3 sources require the same OCaml range as the 2.0.8 package.

Remove the package​

$ opam remove abella

If you installed a pinned revision, remove the pin as well:

$ opam pin remove abella

Next steps​

Continue with the walkthrough for an introduction to Abella, or read File structure for the layout of a development.