FLOLAC'16 / Windows 安裝指南

windows.md

有哪些東西要安裝？

Windows 64-bit 一鍵安裝包：http://www.cs.uiowa.edu/~astump/agda/ （備用連結（比較快）） 本安裝檔包含 GHC 7.8、Agda 2.4 以及 Emacs

1. Haskell

• ghc 與 ghci ，GHC 提供的 Haskell 編譯器與交互式直譯器
• 建議版本為 **GHC 7.8 （較舊版本例如 **7.6 也可以接受，而更新的版本 prelude 所提供的函數型別會與教學使用的有些落差）

2. Agda

• agda
• 建議版本為 Agda 2.5（較舊版本例如 2.4 也可以接受）
• 另外需要在 Emacs 或 Atom 上安裝 agda-mode

3. 文字編輯器 Emacs 或 Atom

• Emacs 直接從官方網站下載 binary distribution，解壓縮即可使用：https://www.gnu.org/software/emacs/download.html
• 建議將執行檔路徑加入 PATH 環境變數中（一般是 解壓縮路徑\bin ）

---

安裝 Haskell

建議安裝 2014.2.0.0 版的 Haskell Platform

• 32-bit: https://www.haskell.org/platform/download/2014.2.0.0/HaskellPlatform-2014.2.0.0-i386-setup.exe
• 64-bit: https://www.haskell.org/platform/download/2014.2.0.0/HaskellPlatform-2014.2.0.0-x86_64-setup.exe

照下載好的安裝檔指示 安裝成功後，在 cmd 裡嘗試 ghc -V 應該可以看到下列訊息

$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 7.8.3

---

安裝 Agda

http://hackage.haskell.org/package/Agda-2.5.1/readme

Windows 使用者在安裝 Agda 前，需要先將電腦的 locale 改為 en-us。修改方法如下:

1. 控制台 > 時鐘語言及和區域 > 變更日期、時間或數字格式
2. 在 系統管理 > 變更系統地區設定 中將目前的系統地區設定改為「英文(美國)」
3. 重新開機

使用 cabal 安裝 Agda：

somewhere> cabal update
somewhere> cabal unpack agda-2.5.1.1

接著打開 Agda-2.5.1.1 資料夾，以純文字編輯器開啟 Agda.cabal 檔案並刪除以下這行文字：

    , EdisonAPI == 1.3

繼續以下指令安裝 Agda：

somewhere> cd Agda-2.5.1.1
somewhere\Agda-2.5.1.1> cabal configure
somewhere\Agda-2.5.1.1> cabal install

安裝成功以後，在 terminal 中應該能看到 agda

$ agda -V
  Agda version 2.5.1.1

---

安裝 agda-mode

如果是使用一鍵安裝的話，直接開啟附帶的 Emacs 應該就可以直接使用 但如果不習慣 Emacs 的話還可以選擇用 Atom 編輯

Atom

總共有兩個 Atom 的 package 要裝：

1. langauge-agda：幫 Agda 的語法上顏色（e.g. 幫 Haskell 上色用 language-haskell）
2. agda-mode：讓我們可以藉由 Atom 與 Agda 溝通

有兩種安裝方式：

1. 開啟選單 Preferences... > Install，搜尋這兩個 package 並且安裝
2. 或是直接在 terminal 打 $ apm install langauge-agda agda-mode

第一次載入檔案時，agda-mode 會嘗試用 which agda 去搜尋 agda 路徑，但如果失敗的話 agda-mode 會主動要你填入路徑名稱。

路徑通常在 Program Files > Haskell > bin 或 Program Files (x86) > Haskell > bin 下面

Emacs

安裝 agda-mode 之前，請先確認 Emacs 的執行檔資料夾路徑已經設定於 PATH 環境變數當中。可以在 terminal 中啟動 Emacs 來檢驗：

$ runemacs

若能啟動 Emacs 則代表路徑設定成功。若否，請從**電腦 > 右鍵選單「內容(R)」> 進階系統設定 > 環境變數(N)… > **雙擊「PATH」變數設定，將 Emacs 執行檔資料夾路徑加入。

接下來安裝 agda-mode：

$ agda-mode compile
$ agda-mode setup

其中 agda-mode setup 指令即為往 Emacs 設定檔中添加以下的程式碼：（若不執行此指令，亦可手動加入）

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

（可能需要先安裝 git ） （Atom 版的 agda-mode 裝好載好後，使用時碰到 bug 請來回報 issue ，助教會努力把它修好 😂😂😂）

如何使用 agda-mode

agda-mode 提供一些指令，讓你可以和 Agda 溝通： 詳細的指令列表請看這裡或這裡

例如載入檔案的指令是 C-c C-l，有兩種方式可以按出來：

1. 先按 Ctrl-c 再按 Ctrl-l
2. 或者壓住 Ctrl ，再連按 c 與 l

寫 Agda 通常要用到許多 unicode symbol 例如 ∀。但 agda-mode 有附帶輸入法，打出 \all 就會變成 ∀。 常用的一些符號該怎麼打可以到這裡查

（在 Emacs 如果碰到字形問題符號跑不出來，請換 Atom 試試看）