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
Install Agda
$ stack install Agda
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.
However, if you already have extra-deps:, add:
extra-deps:
- hogehoge
- hugahuga
(Omitted)
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
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
It's over. Yay! (^○^)
Top comments (0)