Edited at

StackでAgdaをインストールする

最近LinuxマシンにAgdaを導入したので,やったことをメモします.


alexhappyのインストール

alexはレキシカルアナライザを生成するツール,happyはパーサジェネレータです.(それぞれlexyaccに相当します.)

$ stack install alex happy


Agdaのインストール

$ stack install Agda

私は,エラーメッセージが出てコンパイルに失敗しました.


stack.yamlに追記して,もう一度Agdaをインストール

エラーメッセージの

Some different approaches to resolving this:

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

- ほげほげ
- ふがふが
(略)

Plan construction failed.

の部分を参照して,~/.stack/global-project/stack.yamlに以下を追記します.ただし,extra-deps:が既にあるなら,そこに追記します.

extra-deps:

- ほげほげ
- ふがふが
(略)

もう一度Agdaのインストールを行い,失敗したら同じことを繰り返し,成功したら次に進みます.


Emacs上で使えるようにagda-modeを設定

$ agda-mode setup && agda-mode compile


Standard Libraryをインストール (追記)

v1.1をインストールしました.

$ mkdir -p ~/.agda/lib

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

導入できたか確認します.

$ agda -I -l standard-library


おしまい.

おしまい.やったー(^○^)