Agda: A dependently typed functional programming language and proof assistant

[ dependent-types, mit, program ] [ Propose Tags ]

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
epic

Install the Epic compiler.

Disabled

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

Downloads

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 (info)
Dependencies Agda (==2.3.2.2), array (>=0.1 && <0.5), base (>=4.2 && <4.7), binary (>=0.4.4 && <0.6), bytestring (>=0.9.0.1 && <0.11), containers (>=0.1 && <0.6), deepseq (>=1.3 && <1.4), directory (>=1.0 && <1.3), filepath (>=1.1 && <1.4), geniplate (>=0.6.0.3 && <0.7), hashable (>=1.1.2.3 && <1.2 || >=1.2.1.0 && <1.3), hashtables (>=1.0 && <1.2), haskeline (>=0.6.3.2 && <0.8), haskell-src-exts (>=1.9.6 && <1.15), mtl (>=2.0 && <2.1 || >=2.1.1 && <2.2), old-time (>=1.0 && <1.2), parallel (<3.3), pretty (>=1.0 && <1.2), process (>=1.0.1.0 && <1.2), QuickCheck (>=2.3 && <2.7), text (>=0.11 && <0.12), time (>=1.4 && <1.5), unordered-containers (>=0.2 && <0.3), Win32 (>=2.2 && <2.4), xhtml (>=3000.2 && <3000.3), zlib (>=0.4.0.1 && <0.6) [details]
License LicenseRef-OtherLicense
Author Ulf Norell, Nils Anders Danielsson, Andreas Abel, Makoto Takeyama, Catarina Coquand, with contributions by Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, James Chapman, Dominique Devriese, Peter Divanski, Fredrik Nordvall Forsberg, Olle Frediksson, Daniel Gustafsson, Alan Jeffrey, Fredrik Lindblad, Guilhem Moulin, Nicolas Pouillard, Andrés Sicard-Ramírez and many more.
Maintainer Ulf Norell <ulfn@chalmers.se>
Category Dependent types
Home page http://wiki.portal.chalmers.se/agda/
Bug tracker http://code.google.com/p/agda/issues/list
Source repo head: darcs get http://code.haskell.org/Agda/
this: darcs get http://code.haskell.org/Agda/ --tag 2.3.2.2
Uploaded by NilsAndersDanielsson at 2013-10-30T16:33:25Z
Distributions Arch:2.6.4, Debian:2.6.1, Fedora:2.6.3, FreeBSD:2.4.2.3, LTSHaskell:2.6.4.3, NixOS:2.6.4.1, Stackage:2.6.4.3
Reverse Dependencies 8 direct, 1 indirect [details]
Executables agda-mode, agda
Downloads 59794 total (593 in the last 30 days)
Rating 2.75 (votes: 9) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Successful builds reported [all 1 reports]

Readme for Agda-2.3.2.2

[back to package description]
========================================================================
Agda 2
========================================================================

Table of contents:

* Installing Agda
* Configuring the Emacs mode
* Prerequisites
* Installing the Epic backend's dependencies
* Installing a suitable version of Emacs under Windows

------------------------------------------------------------------------
Installing Agda
------------------------------------------------------------------------

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

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, available from Hackage.

  (Note that if you want to install the development version of Agda,
  then you should use the next method.)

  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 source tar balls available from the Agda Wiki, or the
  development version of the code available from our darcs repository.

  1)  Install the prerequisites mentioned below.

  2a) Run the following commands in the top-level directory of the
      Agda source tree:

        cabal update
        cabal install
        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")))

      If you want to have more control over where files are installed
      then you can give various flags to cabal install, see
      cabal install --help.

      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.

  2b) Instead of following 2a 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:
             (inactivate-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.

------------------------------------------------------------------------
Prerequisites
------------------------------------------------------------------------

You need recent versions of the following programs/libraries:

   GHC:           http://www.haskell.org/ghc/
   cabal-install: http://www.haskell.org/cabal/
   Alex:          http://www.haskell.org/alex/
   Happy:         http://www.haskell.org/happy/
   GNU Emacs:     http://www.gnu.org/software/emacs/

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.

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.

------------------------------------------------------------------------
Installing the Epic backend's dependencies
------------------------------------------------------------------------

The Epic backend is experimental and requires that the Epic program is
installed. You can install this program by giving the epic flag to
cabal (but note that, at the time of writing, the Epic program does
not build with certain recent versions of GHC):

* When installing from Hackage:

    cabal update
    cabal install Agda -fepic
    agda-mode setup

* When installing using a source tar ball, following the instructions
  in 2a) above:

    cabal update
    cabal install -fepic
    agda-mode setup

* When installing using a source tar ball, following the instructions
  in 2b) above:

    make CABAL_OPTIONS=-fepic install

You can also install Epic directly:

  cabal install epic

Note that Epic depends on other software:

  The Boehm garbage collector:
    http://www.hpl.hp.com/personal/Hans_Boehm/gc/
  The GNU Multiple Precision Arithmetic Library:
    http://gmplib.org/
  GCC, the GNU Compiler Collection:
    http://gcc.gnu.org/

For more information about Epic:

  http://www.cs.st-andrews.ac.uk/~eb/epic.php

------------------------------------------------------------------------
Installing a suitable version of Emacs under Windows
------------------------------------------------------------------------

Note that Agda code often uses mathematical and other symbols
available from the Unicode character set. In order to be able to
display these characters you may want to follow the procedure below
when installing Emacs under Windows. (Note: These instructions are
possibly outdated.)

1. Install NTEmacs 22.

   Download from
       http://ntemacs.sourceforge.net/
   the self-extracting executable
       ntemacs22-bin-20070819.exe

   When executed, it asks where to extract itself.  This can be
   anywhere you like, but here we write the top directory for ntemacs as
       c:/pkg/ntemacs
   in the following.

   What follows is tested only on this version.  Other versions may
   work but you have to figure out yourself how to use Unicode fonts
   on your version.

2. Install ucs-fonts and mule-fonts for emacs.

   Download from
       http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html
   the tar file
       http://www.cl.cam.ac.uk/~mgk25/download/ucs-fonts.tar.gz
   Let us write the top directory of extracted files as
       c:/pkg/ucs-fonts
   Next we create some derived fonts.
       cd c:/pkg/ucs-fonts/submission
       make all-bdfs
   This gives an error message about missing fonts, but ignore it.

   Download from
       http://www.meadowy.org/
   the tar file
       http://www.meadowy.org/meadow/dists/3.00/packages/mule-fonts-1.0-4-pkg.tar.bz2
   The untarred top directory is named "packages", but we are only
   interested in the subdirectory "packages/fonts".  Let us assume
   we moved this subdirectory to
       c:/pkg/mule-fonts

   Add the following to your .emacs

;;;;;;;;; start of quoted elisp code

(setq bdf-directory-list
      '(
        "c:/pkg/ucs-fonts/submission"
        "c:/pkg/mule-fonts/intlfonts"
        "c:/pkg/mule-fonts/efonts"
        "c:/pkg/mule-fonts/bitmap"
        "c:/pkg/mule-fonts/CDAC"
        "c:/pkg/mule-fonts/AkrutiFreeFonts"
        ))

(setq w32-bdf-filename-alist
      (w32-find-bdf-fonts bdf-directory-list))

(create-fontset-from-fontset-spec
    "-*-fixed-Medium-r-Normal-*-15-*-*-*-c-*-fontset-bdf,
    ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1,
    latin-iso8859-2:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-2,
    latin-iso8859-3:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-3,
    latin-iso8859-4:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-4,
    cyrillic-iso8859-5:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-5,
    greek-iso8859-7:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-7,
    latin-iso8859-9:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-9,
    mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1,
    mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1,
    mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1,
    japanese-jisx0208:-JIS-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0208.1983-0,
    japanese-jisx0208-1978:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISC6226.1978-0,
    japanese-jisx0212:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0212.1990-0,
    latin-jisx0201:-*-*-medium-r-normal-*-16-*-*-*-c-*-jisx0201*-*,
    katakana-jisx0201:-Sony-Fixed-Medium-R-Normal--16-120-100-100-C-80-JISX0201.1976-0,
    thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1,
    lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1,
    tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0,
    tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1,
    korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0,
    chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0,
    chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0,
    chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0,
    chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0
    " t)

(setq font-encoding-alist
      (append '(
                ("JISX0208" (japanese-jisx0208 . 0))
                ("JISX0212" (japanese-jisx0212 . 0))
                ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0))
                ("GB2312" (chinese-gb2312 . 0))
                ("KSC5601" (korean-ksc5601 . 0))
                ("VISCII" (vietnamese-viscii-lower . 0))
                ("MuleArabic-0" (arabic-digit . 0))
                ("MuleArabic-1" (arabic-1-column . 0))
                ("MuleArabic-2" (arabic-2-column . 0))
                ("muleindian-1" (indian-1-column . 0))
                ("muleindian-2" (indian-2-column . 0))
                ("MuleTibetan-0" (tibetan . 0))
                ("MuleTibetan-1" (tibetan-1-column . 0))
                ) font-encoding-alist))

;;;;;;; end of quoted elisp code

   To test the fonts, try

       M-x eval-expression RET
       (set-default-font "fontset-bdf") RET
       M-x view-hello-file

   You should see all the characters without white-boxes.