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
- this Agda library is included in the agda2hs repository; see agda2hs.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/libaries

Optionally, the agda2hs prelude can also be added as a default global import:

echo agda2hs >> ~/.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 agda2hs Agda library
echo $(pwd)/agda2hs.agda-lib >> ~/.agda/libraries
# register the agda2hs Agda library as a default
echo agda2hs >> ~/.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