[Agda] Install Agda on Mac OS

Mac OS 10.5 の上にAgdaをインストールしました。基本的にはAgda Wikiを参考にしたのだけど、そのままではうまく動きませんでした。

• Xcodeをインストール。DVDからなり、ADCのサイトなりから。最新版は10.6用なので古いのをインストール。
  
• Mac Portsのインストール。/opt/local/binにPATHを通す。Mac Portsの準備が済んでいる人もsudo port -v selfupdateする。
  
• GHCはportsからインストールすると古くて駄目なので、GHC download pageよりバイナリパッケージを導入。
  
• sudo port install hs-cabalして、sudo cabal updateして、~/.cabal/binにPATHを通す。
  
• sudo port install darcs
  
• sudo cabal install happyして、sudo cabal install alex
  
• sudo cabal install Agda-executable
  
• cd ~/.cabal/binして、./agda-mode setup
  
• emacsは薦められるままにAquamacsを導入する。
  
• 下記を~/.emacsに追加。
  
(setq load-path (cons "~/.cabal/share/Agda-2.2.4/emacs-mode/" load-path))
(autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t)
(unless (assoc "\\.agda" auto-mode-alist)
(setq auto-mode-alist
(nconc '(("\\.agda" . agda2-mode)
("\\.alfa" . agda2-mode)) auto-mode-alist)))

  
• Aquamacsを起動し、~/test.agdaというファイルを作成して、
  
module test where

data Bool : Set where
  true : Bool
  false : Bool

  と書く（true, falseの前のインデント必須。単語や:の前後に空白があるのも確認。）
  C-c C-lで入力内容が処理され、文字が色分けされたら、agda2-modeが動いている。
  

---
追記: ~/.emacsについて念のため全部掲載。haskell-modeの設定も重要らしいので。

(setq load-path (cons "‾/.cabal/share/Agda-2.2.4/emacs-mode/" load-path))
(autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t)
(unless (assoc "¥¥.agda" auto-mode-alist)
(setq auto-mode-alist
(nconc '(("¥¥.agda" . agda2-mode)
("¥¥.alfa" . agda2-mode)) auto-mode-alist)))
(setq load-path (cons "‾/lib/elisp/haskell" load-path))
(setq auto-mode-alist
(append auto-mode-alist
'(("促促.[hg]s$" . haskell-mode)
("促促.hi$" . haskell-mode)
("促促.l[hg]s$" . literate-haskell-mode))))
(autoload 'haskell-mode "haskell-mode"
"Major mode for editing Haskell scripts." t)
(autoload 'literate-haskell-mode "haskell-mode"
"Major mode for editing literate Haskell scripts." t)
(add-hook 'haskell-mode-hook 'turn-on-haskell-decl-scan)
(add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
(add-hook 'haskell-mode-hook 'turn-on-haskell-indent)
(add-hook 'haskell-mode-hook 'turn-on-haskell-ghci)

(setq haskell-literate-default 'latex)
(setq haskell-doc-idle-delay 0)


(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))