公式ドキュメントが微妙に不親切だったので，自分でまとめる．

1. Agda本体

a. Homebrew経由

Homebrewがある場合は，

brew install agda

楽ちん．

b. apt経由

aptでも入れられる．あんまり信頼できないバージョンが入ることもあると思うが，さっき手元で試した感じ最新バージョンが入ったしこれでも大丈夫そう．

sudo apt-get install zlib1g-dev libncurses5-dev agda

楽ちん．

c. Cabal経由

Cabalから落とすのが一番安心できるが，大変だし時間もかかる．

ドキュメント参照．

Haskellの環境からインストールする．Haskellの環境構築には一悶着あるが，こだわりがない場合はGHCup経由でCabalをinstallして，Cabalからagdaをinstallしてもらう．（2024年現在はghcupからstackもcabalも全部入れるのが主流っぽい）

curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh

続いて，各種ツールのセットアップを行う：

ghcup tui

でrecommendedを選ぶ．すると，ghcup，HLS(HaskellのLanguage Server)，Stack(ghcのインストール，プロジェクトのビルド，ライブラリ管理ができる)，Cabal(プロジェクトのビルド，ライブラリ管理ができる)，GHC(Glasgow Haskell Compiler )がinstallできる．

完了したら，念のためインストールできているか確認する．

cabal --version

続いてAgdaのインストールに入る．あとはドキュメントと同じ．

apt-get install zlib1g-dev libncurses5-dev

cabal update
cabal install alex happy

cabal update
cabal install Agda

けっこう時間がかかる．終わったらagdaが叩けるか試す．

agda --version

2. Agda Standard Libraries

これも入れないとろくな証明を書けない．が，ドキュメントにはあんまり親切に書いていない．

実はagdaをインストールした時点で既に入ってはいるが，そのままでは呼び出せないのでなんとかする必要がある．

  • aptで入れたらusr/share/lockとかのどこかにstandard-library.agda-libがある．

  • Homebrewで入れたら/opt/homebrew/Cellar/agda/2.6.4.3_1/lib/agda とかにstandard-library.agda-libがある．

これらを認識するためのファイルがある$AGDA_DIRを設定する．なんでも良いが，.agdaなるディレクトリを用意する．

cd
mkdir .agda
echo export AGDA_DIR="~/.agda" >> ~/.bash_profile
source .bash_profile

続いて，.agdaの中身を作る．こんな感じの構成を用意していく．

.
├── defaults
└── libraries

cd .agda
touch defaults
touch libraries

defaultsの中身は，

standard-library

librariesの中身は，

/PATH-TO-AGDA-STDLIB/standard-library.agda-lib

PATH-TO-AGDA-STDLIBは，standard-library.agda-libがあるパスを入れる．

どうしても見つからない場合は，.agda内に落としてしまうのでもよい．（正直こっちの方が保守しやすいしおすすめ）

.
├── defaults
├── lib
│   └── agda-stdlib
│        └── ...
└── libraries

lib内に agda-stdlibを落とす．

cd lib
git clone https://github.com/agda/agda-stdlib.git
cd ..

この場合のlibrariesの中身は，

~/.agda/lib/agda-stdlib/standard-library.agda-lib

になる．

これでok．

3. Editor Setup

ここからは，実際にサンプルコードを用意して動作確認する．

VSCode

agda-modeを入れる．

入ったら，以下のようなhello.agdaファイルを用意して，

data Greeting : Set where
  hello : Greeting

greet : Greeting
greet = hello

C-c-C-lを押す．(C-nはControl-n)

なんか下にAll Done.と出てきたらok．ここで，agdaのインストールに失敗している場合は，agdaが無いぞと怒られる．

続いて，以下のdata.agdaファイルを用意し，同様にC-c-C-lを押す：

module type where
open import Data.Nat
a : ?
a = 1

なんか下に

*All Goals*
?0 : Set

と出てくればok．ここで，agda-stdlibの読み込みに失敗している場合は，Data.Setが無いぞと怒られる．

emacs

準備中．agda-modeを使う．

neovim

準備中．agda-nvimかcornelisを使う．