Agda: A dependently typed functional programming language and proof assistant

[ dependent-types, mit, program ] [ Propose Tags ] [ Report a vulnerability ]

Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code).

Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL.

This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running agda-mode setup (see the README).

Note that the Agda library does not follow the package versioning policy, because it is not intended to be used by third-party packages.


[Skip to Readme]

Modules

[Index]

Flags

Manual Flags

NameDescriptionDefault
cpphs

Use cpphs instead of cpp.

Enabled
uhc

Enable the UHC backend. For details, consult the Agda User Manual.

Disabled
debug

Enable debugging features that may slow Agda down.

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Versions [RSS] 2.2.0, 2.2.2, 2.2.4, 2.2.6, 2.2.8, 2.2.10, 2.3.0, 2.3.0.1, 2.3.2, 2.3.2.1, 2.3.2.2, 2.4.0, 2.4.0.1, 2.4.0.2, 2.4.2, 2.4.2.1, 2.4.2.2, 2.4.2.3, 2.4.2.4, 2.4.2.5, 2.5.1, 2.5.1.1, 2.5.1.2, 2.5.2, 2.5.3, 2.5.4, 2.5.4.1, 2.5.4.2, 2.6.0, 2.6.0.1, 2.6.1, 2.6.1.1, 2.6.1.2, 2.6.1.3, 2.6.2, 2.6.2.1, 2.6.2.2, 2.6.3, 2.6.4, 2.6.4.1, 2.6.4.2, 2.6.4.3, 2.7.0, 2.7.0.1 (info)
Change log CHANGELOG.md
Dependencies Agda (==2.5.2), array (>=0.4.0.1 && <0.6), base (>=4.6.0.1 && <4.10), base-orphans (>=0.3.1 && <0.5), binary (>=0.7.2.1 && <0.9), boxes (>=0.1.3 && <0.2), bytestring (>=0.10.0.2 && <0.11), containers (>=0.5.0.0 && <0.6), data-hash (>=0.2.0.0 && <0.3), deepseq (>=1.3.0.1 && <1.5), directory (>=1.2.0.1 && <1.4), EdisonCore (>=1.3.1.1 && <1.3.2), edit-distance (>=0.2.1.2 && <0.3), equivalence (>=0.2.5 && <0.4), fail (>=4.9 && <4.10), filepath (>=1.3.0.1 && <1.5), geniplate-mirror (>=0.6.0.6 && <0.8), gitrev (>=1.2 && <2.0), hashable (>=1.2.1.0 && <1.3), hashtables (>=1.0.1.8 && <1.2 || >=1.2.0.2 && <1.3), haskeline (>=0.7.1.3 && <0.8), ieee754 (>=0.7.8 && <0.9), monadplus (>=1.4 && <1.5), mtl (>=2.1.1 && <=2.1.3.1 || >=2.2.1 && <2.3), murmur-hash (>=0.1 && <0.2), parallel (>=3.2.0.4 && <3.3), pretty (>=1.1.1.0 && <1.1.1.2 || >=1.1.2 && <1.2), process (>=1.1.0.2 && <1.5), regex-tdfa (>=1.2.2 && <1.3), semigroups (>=0.18 && <0.19), strict (>=0.3.2 && <0.4), template-haskell (>=2.8.0.0 && <2.12), text (>=0.11.3.1 && <1.3), time (>=1.4.0.1 && <1.7), transformers (>=0.3 && <0.4 || >=0.4.1.0 && <0.6), transformers-compat (>=0.3.3.3 && <0.6), unordered-containers (>=0.2.5.0 && <0.3), void (>=0.5.4 && <0.9), Win32 (>=2.2 && <2.4), xhtml (>=3000.2.1 && <3000.3), zlib (>=0.4.0.1 && <0.7) [details]
Tested with ghc ==7.6.3, ghc ==7.8.4, ghc ==7.10.3, ghc ==8.0.1
License LicenseRef-OtherLicense
Author Ulf Norell, Andreas Abel, Nils Anders Danielsson, Makoto Takeyama, Catarina Coquand, with contributions by Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, James Chapman, Jesper Cockx, Dominique Devriese, Peter Divanski, Fredrik Nordvall Forsberg, Olle Fredriksson, Daniel Gustafsson, Philipp Hausmann, Patrik Jansson, Alan Jeffrey, Wolfram Kahl, Fredrik Lindblad, Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin, Nicolas Pouillard, Andrés Sicard-Ramírez, Andrea Vezzosi and many more.
Maintainer Ulf Norell <ulfn@chalmers.se>
Revised Revision 3 made by AndresSicardRamirez at 2017-08-02T00:46:51Z
Category Dependent types
Home page http://wiki.portal.chalmers.se/agda/
Bug tracker https://github.com/agda/agda/issues
Source repo head: git clone https://github.com/agda/agda.git
this: git clone https://github.com/agda/agda.git(tag v2.5.2)
Uploaded by AndresSicardRamirez at 2016-12-22T12:39:35Z
Distributions Arch:2.6.4.1, Debian:2.6.1, Fedora:2.6.4.1, FreeBSD:2.4.2.3, LTSHaskell:2.6.4.3, NixOS:2.7.0.1, Stackage:2.7.0.1
Reverse Dependencies 8 direct, 1 indirect [details]
Executables agda-mode, agda
Downloads 63815 total (522 in the last 30 days)
Rating 2.75 (votes: 10) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-12-22 [all 1 reports]

Readme for Agda-2.5.2

[back to package description]

Agda 2

Hackage version Stackage version Build Status

Table of contents:

Note that this README only discusses installation of Agda, not its standard library. See the Agda Wiki for information about the library.

Documentation

Prerequisites

You need recent versions of the following programs/libraries:

You should also make sure that programs installed by cabal-install are on your shell's search path.

For instructions on installing a suitable version of Emacs under Windows, see [below]((#installing-emacs-under-windows).

Non-Windows users need to ensure that the development files for the C libraries zlib and ncurses are installed (see http://zlib.net and http://www.gnu.org/software/ncurses/). Your package manager may be able to install these files for you. For instance, on Debian or Ubuntu it should suffice to run

apt-get install zlib1g-dev libncurses5-dev

as root to get the correct files installed.

Note on GHC's CPP language extension

Recent versions of Clang's preprocessor don't work well with Haskell. In order to get some dependencies to build, you may need to set up Cabal to have GHC use cpphs by default. You can do this by adding

program-default-options
  ghc-options: -pgmPcpphs -optP--cpp

to your .cabal/config file. (You must be using cabal >= 1.18. Note that some packages may not compile with this option set.)

You don't need to set this option to install Agda from the current development source; Agda.cabal now uses cpphs.

Installing Agda

There are several ways to install Agda:

Using a binary package prepared for your platform

Recommended if such a package exists. See the Agda Wiki.

Using a released source package from Hackage

Install the prerequisites mentioned below, then run the following commands:

cabal update
cabal install Agda
agda-mode setup

The last command tries to set up Emacs for use with Agda. As an alternative you can copy the following text to your .emacs file:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

It is also possible (but not necessary) to compile the Emacs mode's files:

agda-mode compile

This can, in some cases, give a noticeable speedup.

WARNING: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files.

Using the development version of the code

You can obtain tarballs of the development version from the Agda Wiki, or clone the repository.

Install the prerequisites discussed in Prerequisites.

Then, either:

(1a) Run the following commands in the top-level directory of the Agda source tree to install Agda:

cabal update
cabal install

(1b) Run agda-mode setup to set up Emacs for use with Agda. Alternatively, add the following text to your .emacs file:

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

It is also possible (but not necessary) to compile the Emacs mode's files:

agda-mode compile

This can, in some cases, give a noticeable speedup.

WARNING: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old compiled files.

(2) Or, you can try to install Agda (including a compiled Emacs mode) by running the following command:

make install

Configuring the Emacs mode

If you want to you can customise the Emacs mode. Just start Emacs and type the following:

M-x load-library RET agda2-mode RET
M-x customize-group RET agda2 RET

This is useful if you want to change the Agda search path, in which case you should change the agda2-include-dirs variable.

If you want some specific settings for the Emacs mode you can add them to agda2-mode-hook. For instance, if you do not want to use the Agda input method (for writing various symbols like ∀≥ℕ→π⟦⟧) you can add the following to your .emacs:

(add-hook 'agda2-mode-hook
          '(lambda ()
            ; If you do not want to use any input method:
            (deactivate-input-method)
            ; (In some versions of Emacs you should use
            ; inactivate-input-method instead of
            ; deactivate-input-method.)

            ; If you want to use the X input method:
            (set-input-method "X")))

Note that, on some systems, the Emacs mode changes the default font of the current frame in order to enable many Unicode symbols to be displayed. This only works if the right fonts are available, though. If you want to turn off this feature, then you should customise the agda2-fontset-name variable.


Installing Emacs under Windows

A precompiled version of Emacs 24.3, with the necessary mathematical fonts, is available at http://homepage.cs.uiowa.edu/~astump/agda/

Hacking on Agda

Head to HACKING