噢,我的上帝啊,世界上怎么会有这么多劝退新人的教程呢!
我在配置 Haskell 环境的时候,遇到了超多的问题(对我这种萌新来说,是绝对的折磨)。在配置 Agda 的时候获得了极大的帮助,得以简单的安装完成,但配置方法与官方文档上的教程存在不少出入(官方教程老麻烦了),所以为了帮助和我一样一头雾水的萌新,把这些东西记录下来帮助更多人入门。
我尽量写的详细,以避免实际操作和教程的出入。
P.S. 本教程仅适用于 Win10。不需要配置 Haskell。
Agda 本体
下载 Agda
链接:https://github.com/agda/agda/releases/download/nightly/Agda-nightly-win64.zip
(此处下载的是每晚编译的版本)
解压 Agda-nightly-win64.zip
移动解压后的文件夹 Agda-nightly-win64 到你想长期保存的位置【不移的话,这个文件夹得永久留在这里了,所以慎重啊(我这个文件夹在 Downloads 里,想哭的心都有了)】
得到文件目录如图:
点击 Agda-nightly 文件夹,有以下文件
点击 install_agda_user.dat,等待安装完成,窗口自动关闭
标准库
下载 标准库
1
git clone https://github.com/agda/agda-stdlib.git --depth=1
或者戳链接:https://github.com/agda/agda-stdlib/archive/v1.5.zip
(此处下载的是 v1.5,教程写作时间的 latest release)
解压 agda-stdlib-1.5.zip
移动解压后的文件夹 agda-stdlib-1.5 到你想保存标准库的位置
接下来需要让 Agda 知道标准库在哪里
1
cd C:\Users\%USERNAME%\AppData\Roaming\agda
在这个目录下创建两个文件,分别名为 defaults 和 libraries(别拼错了,我拼错了3次,哭哭)
1
2touch defaults
touch librariesdefaults 的内容为:
libraries 的内容为:
你刚刚放置标准库的路径\standard-library.agda-lib,比如我的是:
还需要设置文本编辑器,这里有两个选择,VS code 和 Emacs。
P.S. 用 VS code 写 Agda 的时候,会遇到各种各样稀奇古怪的 bug,,,
选择1:VS code 的设置
找到名为 agda-mode 的 extension
安装并重启 VS code
现在可以创建一个以 .agda 为后缀的文件,使用
C-c C-l
测试。(第一次运行时间会比较长)(C 是 Ctrl)-
底部正常输出了~
选择2:Emacs 的设置
回到安装 Agda 的文件夹:
点击 install_emacs_mode.bat,等待安装完成,自动退出
要让 Emacs 能找到 agda_mode 的库,需要这样做:
找到 Emacs 的配置文件,默认在这里:
1
cd C:\Users\%USERNAME%\AppData\Roaming
在这个文件夹内找到 .emacs ,在这个文件中加入以下内容
1
2(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))打开 Emacs,创建一个以 .agda 为后缀的文件,使用
C-c C-l
测试。All Done~
Author: Alendia
Permalink: https://alendia.dev/2021/03/03/agda-install-guide/
文章默认使用 CC BY-NC-SA 4.0 协议进行许可,使用时请注意遵守协议。
Comments