Introduction

Getting Started

Requirements

Haskell programming language
Haskell Cabal
Agda programming language
- version >= 2.6.4 && < 2.6.5
Agda standard library
Agda library agda2hs-base
- this Agda library is included in the agda2hs repository; see base.agda-lib
- you can navigate the library in HTML format, along with a comprehensive test suite

Installation with Cabal

agda2hs is released on Hackage, and can be installed with Cabal:

cabal install agda2hs

Once installed, the agda2hs prelude bundled with agda2hs can be registered in the Agda config using the agda2hs locate command:

agda2hs locate >> ~/.agda/libraries

Optionally, the base.agda-lib library can also be added as a default global import:

echo agda2hs-base >> ~/.agda/defaults

Manual installation

Let DIR be the directory in which you start running these shell commands.

# clone the repository locally
git clone git@github.com:agda/agda2hs.git

# build agda2hs with cabal
cd agda2hs
cabal install

# register the base Agda library
echo $(pwd)/lib/base/base.agda-lib >> ~/.agda/libraries
# register the base Agda library as a default
echo agda2hs-base >> ~/.agda/defaults

Running `agda2hs`

To run agda2hs, run

agda2hs <path>/<name>.agda [-o <outputDir>]

which, for all dependencies of that Agda file, compiles and writes

[<outputDir>/]<modulePath>.hs

Using agda2hs with Stack

You can use agda2hs with the Haskell Stack tool.

TODO: integrate agda2hs as a preprocessor for stack

Creating an Agda2Hs project

All agda2hs projects should have a dependency on the agda2hs-base library provided by Agda, and can also optionally depend on the agda2hs-containers library. Using Agda’s standard library with agda2hs is not supported.

All agda2hs projects should enable the --erasure option of Agda. It is also recommended to enable the --no-projection-like flag since otherwise functions might get inlined inadvertently.