FLOLAC'16 / Linux 安裝指南

linux.md

有哪些東西要安裝？

1. Haskell

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

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

安裝 Haskell

---

建議用 distro 提供的 package manager 安裝，選擇 2014.2.0.0 版的 Haskell Platform。 或是自己從 source 編 😁

安裝 Agda

---

在 terminal 中試試看找不找得到 cabal

$ cabal
-bash: cabal: command not found

如果找不到的話， cabal 可能躲在這兩個地方

1. ~/Library/Haskell/bin/cabal
2. ~/.cabal/bin/cabal

看 cabal 與他的好朋友躲在哪邊，請把

export PATH=$HOME/Library/Haskell/bin:$PATH

或者

export PATH=$HOME/.cabal/bin:$PATH

這其中一行字，加到 ~/.bash_profile 檔案裡（接在後面就可以了）

接著用 cabal 安裝 Agda：

$ cabal update
$ cabal install happy alex
$ cabal install agda 

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

$ agda -V
Agda version 2.5.1

安裝 agda-mode

---

可以選擇在 Atom 或 Emacs 安裝使用

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 會與 Agda 溝通，所以他需要知道 Agda 住在哪裡。 第一次載入檔案時，agda-mode 會嘗試用 which agda 去搜尋 agda 路徑，但如果失敗的話 agda-mode 會主動要你填入路徑名稱。

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

Emacs

Emacs 裝好後，先在 terminal 中執行下列指令

$ agda-mode compile
$ agda-mode setup

如何使用 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 試試看）