DEV Community

Masaki Haga
Masaki Haga

Posted on • Edited on

Installing Agda using Stack

#agda #stack #emacs #haskell

I recently installed Agda on my Linux machine, so I'll take note of what I did.

Install alex, happy

alex is a tool to generate a lexical analyzer and happy is a parser generator. (They correspond to lex and yacc respectively.)

$ stack install alex happy
Enter fullscreen mode Exit fullscreen mode

Install Agda 

$ stack install Agda
Enter fullscreen mode Exit fullscreen mode

I failed to compile with an error message.

Add to stack.yaml and install Agda again

Refer to the following part of the error message and add the following to ~/.stack/global-project/stack.yaml:

Some different approaches to resolving this:

* Recommended action: try adding the following to your extra-deps in/home/(Username)/.stack/global-project/stack.yaml:

- hogehoge
- hugahuga
(Omitted)

Plan construction failed.
Enter fullscreen mode Exit fullscreen mode

However, if you already have extra-deps:, add:

extra-deps:
- hogehoge
- hugahuga
(Omitted)
Enter fullscreen mode Exit fullscreen mode

Install Agda again, repeat if it fails, and proceed if it succeeds.

Set agda-mode to work with Emacs 

$ agda-mode setup && agda-mode compile
Enter fullscreen mode Exit fullscreen mode

InstallStandard Library

Version 1.1 has been installed.

$ mkdir -p ~/.agda/lib
$ cd ~/.agda/lib
$ wget https://github.com/agda/agda-stdlib/archive/v1.1.tar.gz
$ tar xvzf v 1.1 .tar.gz
$ echo "$HOME/.agda/lib/agda-stdlib -1.1/standard-library.agda-lib" > ~/.agda/libraries

$ agda-I-l standard-library
Enter fullscreen mode Exit fullscreen mode

It's over. Yay! (^○^)

Top comments (0)