Windows 環境 Agda 安裝教學

參考連結：https://agda.readthedocs.io/en/latest/getting-started/installation.html

安裝 WSL

參考連結：https://learn.microsoft.com/zh-tw/windows/wsl/install

1. 打開 Power Shell 下指令
   ​​​​wsl --install
   

2. 等待安裝完後需重新開機
3. 重新開機後會跳出視窗要求設置 Username 及 Password
   
   
4. 有看到 [username]@[systemname]: $ 就代表設置成功！

安裝 home-brew

參考連結：https://brew.sh/

1. 複製 brew 官網的安裝指令
   
   
2. 打開 Power Shell 下指令 ubuntu
3. 在 $ 字號後貼上 brew 安裝指令
4. 等候安裝程序跑完後，視窗會出現下面兩行指令（[username] 會代換為剛剛 WSL 安裝時設定的 username），複製後在 $ 字號後貼上
   ​​​​(echo; echo 'eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"') >> /home/[username]/.bashrc
   ​​​​eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
   

5. 以上兩行有正確貼上後，再下指令 brew，若有出現下方畫面代表安裝成功
   
   

安裝 Agda

1. 同樣在 utuntu 指令區下以下指令，這裡安裝會跑比較久
   ​​​​brew install agda
   

2. 安裝成功後下以下指令，即可設置好 Agda
   ​​​​agda-mode setup
   

VS Code 環境設置

1. 安裝 Extension: Remote Development
   
   
2. 按 Ctrl + Shift + P，選擇 WSL: Connect to WSL
   
   
3. 確認 VS Code 視窗左下角有 WSL: Ubuntu
   
   
4. 安裝 Extension: Agda-mode
   
   
5. 開啟一個新檔案寫入下面程式碼
   ​​​​data Greeting : Set where
   ​​​​  hello : Greeting
   
   ​​​​greet : Greeting
   ​​​​greet = hello
   

6. 儲存檔案為 hello.agda（檔名必須一致），並且注意儲存路徑會在 /home/[username]... 底下，並非 Windows 的 C:\ 路徑
7. 儲存後在剛剛的檔案視窗按 Ctrl + C 後再按 Ctrl + L
   
   
8. 若安裝成功會看到程式碼成功套色並出現 All Done
   
   

Windows 與 WSL 檔案傳輸

開啟 Power Shell 或 WSL 指令區下指令：

explorer.exe .

或直接開啟檔案總管視窗，從 Windows 搬移檔案到 WSL

WSL 系統路徑：\\wsl.localhost\Ubuntu\home\[username]

只可搬移檔案到 /home/[username]/..，不可直接寫入 /home/