Windows 課前安裝指南

1. 安裝 Agda

這裡下載Agda2.6.0.1.v1.msi打開一直下一步即可


2. 安裝 Agda standard library 

  1. 下載並解壓縮到某個資料夾(假設路徑為 $SOMEWHERE
  1. 解壓縮出來的資料夾中應該有個檔案名稱為 standard-library.agda-lib ,他的路徑應為$SOMEWHERE/agda-stdlib-1.2/standard-library.agda-lib
  1. C:\Users\$USERNAME\AppData\Roaming\ (假設用戶名為 $USERNAME)底下創建名為 agda 的資料夾,他的路徑應為 C:\Users\$USERNAME\AppData\Roaming\agda
  • (AppData 是隱藏資料夾,若看不到請到 Windows 資料夾上方的選項將「檢視>隱藏的項目」打開)
  1. 在剛創建的 agda 資料夾底下新增一個名為 libraries 的空白檔案,他的路徑應為 C:\Users\$USERNAME\AppData\Roaming\agda\libraries
  1. 在剛創建的 libraries 空白檔案裡加入前述 $SOMEWHERE/agda-stdlib-1.2/standard-library.agda-lib 路徑
  1. 在同個資料夾創建另一個檔案 defaults 內容寫入 standard-library


3. 安裝 VS Code & 擴充功能 agda-mode


按下快捷鍵 Ctrl+C Ctrl+L 若出現以下畫面代表安裝完成





// 不成功可參考以下方法

安裝 Haskell


若有自己安裝過 Haskell 與 Agda 請先刪除再重新安裝,刪除方式:1. 去控制台>解除安裝程式,將 Haskell 相關程式都解除安裝 2. 去 C:\Program Files 與 C:\Program Files(x86) 檢查有沒有 Haskell 與 Haskell Platform 資料夾,若有請刪除

  1. 請照著這些步驟
  1. 簡化版:
  1. 開始功能表 > PowerShell,按右鍵「以系統管理員身分執行」
  1. 安裝 chocolatey
  1. 在 PowerShell 輸入Set-ExecutionPolicy Bypass -Scope Process允許安裝程式
  1. 複製貼上下面指令:
Set-ExecutionPolicy Bypass -Scope Process -Force; [System.Net.ServicePointManager]::SecurityProtocol = [System.Net.ServicePointManager]::SecurityProtocol -bor 3072; iex ((New-Object System.Net.WebClient).DownloadString('https://chocolatey.org/install.ps1'))
  1. 輸入choco確定有安裝成功
  1. 使用 chocolatey 安裝 haskell 相關程式 choco install haskell-dev
  1. 完成後應該會在你的電腦裡安裝 ghc , ghcicabal 這些程式
  • 要檢查是否有裝好,可以在 PowerShell 輸入 ghc --version 看看有沒有顯示版本資訊

安裝 Agda


  1. PowerShell 中輸入

cabal update
cabal install Agda