Agate version 0.5.20060713

What is Agate

Agate is a translator that converts an Agda program into a Haskell program.  The generated program can be compiled with GHC (Glasgow Haskell Compiler) into executable code and then executed.  Agate provides a mechanism to access some built-in features of Haskell such as I/O using the 'native' or 'postulate' syntax of Agda.  Future releases of Agate will feature optimization based on type information in the program, although it is not available in this release.


You need Glasgow Haskell Compiler version 6.4.x to build and use Agate.
Note that the version 6.6 cannot build Agate and cannot be used as back-end of Agate currently.
You also need aclocal (automake) and autoconf to build Agate.


Click here to download the source tarball of the latest version of Agate.

How to Build

% aclocal-I macros 
% autoconf 
% ./configure --enable-newsyntax 
% make

How to Install

% make install

How to Use  

% agate [options] file.agda ...
% ghc [ghc-options...] a.hs

Command-line options

  --help, -h                  show this help
  --version, -v               show version
  --library-path DIR, -L DIR  set library path
  -o FILE                     specify output file