Skip to main content
Version: 2.1.0-dev

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.

The development version 2.1.0-dev is not released on OPAM. Install it by pinning a local checkout of the repository.

Requirements​

  • opam 2.1 or later.
  • An OCaml switch using OCaml 5.3.0 or later.
  • Dune 3.20 or later, installed automatically by opam.

Create a dedicated switch if your current one uses an older OCaml:

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

Install from a local checkout​

Clone the repository and pin the checkout:

$ git clone https://github.com/abella-prover/abella.git
$ cd abella
$ opam pin add abella .

The pin resolves the dependencies from abella.opam and installs the three executables. Check the result:

$ abella --version

The version should be 2.1.0-dev. The documentation on this site is pinned at commit 6b5bc46; check out that commit if you need the exact sources the pages describe:

$ git checkout 6b5bc46
$ opam pin add abella .

Updating a pinned checkout​

After pulling new changes, reinstall the pinned package:

$ git pull
$ opam install abella

Remove the package​

$ opam remove abella
$ opam pin remove abella

Next steps​

Continue with the walkthrough for an introduction to Abella, or read Reasoning-level modules for the main addition in this version.