Fucking install guide: How to install Adga in Win10

噢,我的上帝啊,世界上怎么会有这么多劝退新人的教程呢!

我在配置 Haskell 环境的时候,遇到了超多的问题(对我这种萌新来说,是绝对的折磨)。在配置 Agda 的时候获得了极大的帮助,得以简单的安装完成,但配置方法与官方文档上的教程存在不少出入(官方教程老麻烦了),所以为了帮助和我一样一头雾水的萌新,把这些东西记录下来帮助更多人入门。

我尽量写的详细,以避免实际操作和教程的出入。

P.S. 本教程仅适用于 Win10。不需要配置 Haskell。

Agda 本体

  1. 下载 Agda

    链接:https://github.com/agda/agda/releases/download/nightly/Agda-nightly-win64.zip

    (此处下载的是每晚编译的版本)

  2. 解压 Agda-nightly-win64.zip

  3. 移动解压后的文件夹 Agda-nightly-win64 到你想长期保存的位置【不移的话,这个文件夹得永久留在这里了,所以慎重啊(我这个文件夹在 Downloads 里,想哭的心都有了)】

    得到文件目录如图:

    image-20210303112707034

  4. 点击 Agda-nightly 文件夹,有以下文件

    image-20210303112800226

  5. 点击 install_agda_user.dat,等待安装完成,窗口自动关闭

标准库

  1. 下载 标准库

    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)

  2. 解压 agda-stdlib-1.5.zip

  3. 移动解压后的文件夹 agda-stdlib-1.5 到你想保存标准库的位置

  4. 接下来需要让 Agda 知道标准库在哪里

    1
    cd C:\Users\%USERNAME%\AppData\Roaming\agda

    在这个目录下创建两个文件,分别名为 defaults 和 libraries(别拼错了,我拼错了3次,哭哭)

    1
    2
    touch defaults
    touch libraries

    defaults 的内容为:

    image-20210303114544146

    libraries 的内容为:

    你刚刚放置标准库的路径\standard-library.agda-lib,比如我的是:

    image-20210303114700425

还需要设置文本编辑器,这里有两个选择,VS code 和 Emacs。

P.S. 用 VS code 写 Agda 的时候,会遇到各种各样稀奇古怪的 bug,,,

选择1:VS code 的设置

  1. 找到名为 agda-mode 的 extension

    image-20210303115106971

  2. 安装并重启 VS code

  3. 现在可以创建一个以 .agda 为后缀的文件,使用 C-c C-l 测试。(第一次运行时间会比较长)(C 是 Ctrl)

  4. image-20210303115332604

    底部正常输出了~

选择2:Emacs 的设置

  1. 回到安装 Agda 的文件夹:

    image-20210303115640116

  2. 点击 install_emacs_mode.bat,等待安装完成,自动退出

  3. 要让 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")))
  4. 打开 Emacs,创建一个以 .agda 为后缀的文件,使用 C-c C-l 测试。

    image-20210303120143007

    All Done~

本文作者:Alendia

本文链接: https://alendia.dev/2021/03/03/agda-install-guide/

文章默认使用 CC BY-NC-SA 4.0 协议进行许可,使用时请注意遵守协议。

评论

您所在的地区可能无法访问 Disqus 评论系统,请切换网络环境再尝试。