Download

Installation

There are several ways to obtain Adelfa. We recommend using opam, the OCaml package manager, to install Adelfa. However, you can also clone the code from GitHub or download the source code directly from this website.

The recommended way for installing Adelfa is through OPAM.

opam install adelfa

The code for Adelfa is hosted on Github. You can clone the repository and install the code using Dune.

git clone https://github.com/adelfa-prover/adelfa.git
cd adelfa
dune install

You may also obtain the source code by downloading the latest release from Github.

VSCode Support

We provide a VSCode extension for developing proofs in Adelfa. The extension is in active development so it may have issues. If you encounter any issues, please report them. For a more robust experience, we recommend using the Emacs/Proof General setup.

Emacs / Proof General Support

The distribution of Adelfa provides a Proof General mode and syntax highlighting for developing proofs in its PG/ directory which has the following structure:

adelfa-syntax.el

adelfa.el

README.md

Install Proof General

Install Proof General as instructed by its documentation at https://proofgeneral.github.io/download/.

Add Adelfa to Proof General Source

Copy the entirety of the adelfa directory into the folder where Proof General was installed. The folder structure should now resemble:

adelfa-syntax.el

adelfa.el

proof-general.el

Setup Adelfa in Proof General

In the file PG/generic/proof-site.el, add an entry for Adelfa in PG's proof-assistant-table-default resembling (adelfa "Adelfa" "ath"). The proof-assistant-table-default should resemble something similar to:

(defconst proof-assistant-table-default
    '(
      ;; Main instances of PG.

      (adelfa "Adelfa" "ath")
      (coq "Coq" "v" nil (".vo" ".glob"))
      ; ...
     ))

Complete Proof General Setup

In your Emacs configuration, commonly located at ~/.emacs or ~/.emacs.d/init.el, add the following lines:

(defconst proof-site-file
  (expand-file-name "path-to-pg/PG/generic/proof-site.el"))

(when (file-exists-p proof-site-file)
  (setq proof-splash-enable nil
        proof-output-tooltips nil
        proof-three-window-mode-policy 'horizontal)

  (load-file proof-site-file)

  (add-hook 'adelfa-mode-hook
            #'(lambda ()
                (setq indent-line-function 'indent-relative)))

  (setq auto-mode-alist
        (append
         '(("\\.ath\\'" . adelfa-mode))
         auto-mode-alist)))

Where path-to-pg should be changed to the file path of your proof general installation.