Skip to content

Instantly share code, notes, and snippets.

@banacorn

banacorn/macosx.md

Last active Jul 7, 2016
Embed
What would you like to do?
FLOLAC'16 / OS X 安裝指南

有哪些東西要安裝?

  1. Haskell
  • ghcghci ,GHC 提供的 Haskell 編譯器與交互式直譯器
  • 建議版本為 **GHC 7.8 (較舊版本例如 **7.6 也可以接受,而更新的版本 prelude 所提供的函數型別會與教學使用的有些落差)
  1. Agda
    • agda
    • 建議版本為 Agda 2.5(較舊版本例如 2.4 也可以接受)
    • 另外需要在 Emacs 或 Atom 上安裝 agda-mode

安裝 Haskell


建議安裝 2014.2.0.0 版的 Haskell Platform

安裝 Agda


http://hackage.haskel.org/package/Agda-2.5.1/readme Haskell platform 會附帶 ghcghcicabal 這些工具

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

$ cabal
-bash: cabal: command not found

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

  1. ~/Library/Haskell/bin/cabal
  2. ~/.cabal/bin/cabal
  3. /Library/Haskell/..? (目錄下面某處 XD)

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 裝好後,開啟選單 Preferences... > Install 安裝套件

  • 搜尋並且安裝 langauge-agda
  • 再安裝 agda-mode

[註] 第一次載入檔案時,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 ,再連按 cl

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

(在 Emacs 如果碰到字形問題符號跑不出來,請換 Atom 試試看)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment