Download

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

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 folder where Proof General was installed. The folder structure should now resemble:

  • 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.

HomeWalkthrough