遲來的 Agda 環境搭建

來自專欄千里冰封被吊打的日常13 人贊了文章

原文http://ice1000.org/2018/06/13/AgdaEnvConfig/

前面講了辣么多 Agda 的語言特性、寫證明的思路等，但是都沒有介紹 Agda 的具體編程方法，所以我先補上這個空缺。

首先，我們要搭建 Agda 開發環境。

1. 在 apt 里安裝合適版本的 ghc
2. 在 apt 里安裝合適版本的 cabal/stack (本文使用 cabal, 因為我們不需要用 Haskell 寫項目)
3. 在 apt 里安裝合適版本的 Emacs
4. 在 cabal 里安裝合適版本的 alex, happy, cpphs
5. 在 cabal 里安裝最新版本的 Agda
6. 通過 git 安裝最新版本的 Agda 標準庫
7. 學習 Agda 編程方法

如果你已經熟悉 cabal/stack 和 ghc 的安裝以及 Haskell 包的安裝，那麼你可以直接跳到 Emacs 的使用那一步。

安裝 Agda

我寫了一個用於初始化 Ubuntu 系統的腳本，用來安裝我需要的所有程序和進行所有配置：

其中，我們需要執行的代碼是：

## prerequisites$ sudo apt install cabal ghc git emacs$ export INSTALLATION_PATH=~/SDK # replace with your own## installing agda$ cabal update$ cabal install alex happy cpphs$ cabal install --allow-newer Agda$ agda-mode setup$ agda-mode compile$ mkdir -p $INSTALLATION_PATH$ git clone https://github.com/agda/agda-stdlib.git $INSTALLATION_PATH/agda-stdlib/$ rm $INSTALLATION_PATH/agda-stdlib/src/index.agda$ mkdir ~/.agda$ echo "$INSTALLATION_PATH/agda-stdlib/standard-library.agda-lib" >> ~/.agda/libraries$ echo "standard-library" >> ~/.agda/defaults

請先自行修改 INSTALLATION_PATH 為你希望的 Agda 標準庫的安裝目錄，以及把 cabal 和 ghc 改為你需要的版本。 推薦的 cabal 版本是 2.2，ghc 版本是 8.2.2。

安裝完成後，可以這樣測試：

$ agda --version

如果輸出了版本信息，說明安裝正常。

配置 Emacs

如果你真的非常不能接受 Emacs，你可以去官網找 Atom 環境搭建的教程。 由於我本身就習慣使用 Emacs 編程了，所以就只講 Emacs 了。

如果你是照著上一步來的，你執行了所有剛才給的 shell 腳本，那麼就不需要這一步。 否則，你需要執行：

$ agda-mode setup$ agda-mode compile

然後你可以使用 Emacs 打開一個 .agda 文件（更多關於 Emacs 的使用技巧，請參考我的這篇文章）：

emacs Hello.agda

打開之後先輸出以下代碼（module 名必須和文件名匹配）：

module Hello where

按下 Ctrl+C Ctrl+L，可以看到高亮出現了， 屏幕下方還出現了一個滴點兒大的 buffer，裡面什麼都沒有。

如果你不能理解這個很長很長的快捷鍵，你可以用我按這個快捷鍵的方法去按：

1. 按住 Ctrl
2. 按下 C
3. 鬆開 C
4. 按下 L
5. 鬆開 L
6. 鬆開 Ctrl

高亮出現代表 Parsing 和基本的檢查通過了，每次刷新高亮都需要按這個快捷鍵，剛輸入的字元的顏色是錯誤的。

如果你的代碼有詞法上的錯誤，那麼出錯的地方會有紅色高亮，其他地方是黑色的。

這兩種情況下，下面那個滴點兒大的 buffer 會有錯誤信息。

寫點代碼吧

我們可以試著寫點代碼。比如，定義一個 GADT:

data List (A : Set) : Set where [] : Set A _::_ : A -> List A -> List A

按 Ctrl+C Ctrl+L 出現高亮。 然後我們編寫一個函數，並不寫實現：

emptyList : {A : Set} -> List AemptyList = ?

對，你沒有看錯，我們需要在代碼里寫下這個問號，表示我們暫時不確定這個地方可以寫什麼。 Agda 強大的類型系統擁有輔助程序員填寫問號內的內容的功能，有時還可以直接自己填寫實現。

按 Ctrl+C Ctrl+L 再次出現高亮，你會發現代碼變成了這樣：

emptyList : {A : Set} -> List A

emptyList = { }0

這個綠色背景的 { }0 就是 Agda 的 『洞』，表示一個還沒想好怎麼寫的表達式，在下面的滴點兒大的 buffer 里註明了它的類型。 把游標放在那個『洞』裡面，按 Ctrl+C Ctrl+A ，你會發現 Agda 給這個洞填入了一個值。

emptyList : {A : Set} -> List A

emptyList = []

Idris, Coq 都具有這樣的功能。

我說完啦。

為什麼要寫這篇文章

最近被 @16 拉著寫的 Agda 代碼比你們想像的要多， 又產生了寫博客的慾望。

我的計劃是，先使用 Literate Agda 重寫之前的幾篇博客，擺脫傻逼 LaTeX 代碼，然後繼續更新這個系列。

更新會發布到 zju lambda 的網站（如果龍神給這個網站續命了的話），我的博客，和知乎。

廣告

給大家推薦一個國內的GitHub同類產品叫coding，網址是