Doom Emacs 中 Agda-mode 2 的语法高亮显示答案

【问题标题】：Syntax highlighting for Agda-mode 2 in Doom EmacsDoom Emacs 中 Agda-mode 2 的语法高亮显示
【发布时间】：2020-03-02 06:19:05
【问题描述】：

我需要帮助让我的 emacs 系统上运行 agda 模式。本质上，语法高亮只发生在我保存之后，而不是像其他标准模式那样实时。我做了基础教程。我在我的系统上运行 Manjaro，所以我使用 pacman 安装了 agda (2.6.0.1) 和 agda-stdlib (1.2-1)。之后，我做到了

agda-mode setup

这样做是添加

(load-file (let ((coding-system-for-read 'utf-8))
             (shell-command-to-string "agda-mode locate")))

到我的 .emacs.d 文件中的 .init.el。所以那时，我认为一切都很好。然而，当我启动 emacs 并尝试使用我在互联网上找到的一些文件来学习 agda (https://oxij.org/note/BrutalDepTypes.lagda)。但是，当我保存文件时似乎只有语法突出显示，并且任何新文本在保存之前都不会着色。我试图通过从 .emacs.d 中的 .init.el 中删除代码来解决此问题，而是将其放入 .doom.d 中的 .init.el 中。但我仍然得到相同的结果。我也做了sudo agda-mode compile，这给了我以下输出：

Loading quail/latin-ltx...

我使用 sudo，否则我会得到这个

>>Error occurred processing /usr/share/agda/emacs-mode/agda2-abbrevs.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda2-abbrevs.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda2-abbrevs.elc
>>Error occurred processing /usr/share/agda/emacs-mode/annotation.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/annotation.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/annotation.elc
>>Error occurred processing /usr/share/agda/emacs-mode/agda2-queue.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda2-queue.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda2-queue.elc
>>Error occurred processing /usr/share/agda/emacs-mode/eri.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/eri.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/eri.elc
>>Error occurred processing /usr/share/agda/emacs-mode/agda2.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda2.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda2.elc
>>Error occurred processing /usr/share/agda/emacs-mode/agda-input.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda-input.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda-input.elc
>>Error occurred processing /usr/share/agda/emacs-mode/agda2-highlight.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda2-highlight.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda2-highlight.elc
Loading quail/latin-ltx...


>>Error occurred processing /usr/share/agda/emacs-mode/agda2-mode.el: File error (("Opening output file" "Cannot overwrite file" "/usr/share/agda/emacs-mode/agda2-mode.elc"))
Removing old name: Permission denied, /usr/share/agda/emacs-mode/agda2-mode.elc
Unable to compile the following Emacs Lisp files:
  /usr/share/agda/emacs-mode/agda2-abbrevs.el
  /usr/share/agda/emacs-mode/annotation.el
  /usr/share/agda/emacs-mode/agda2-queue.el
  /usr/share/agda/emacs-mode/eri.el
  /usr/share/agda/emacs-mode/agda2.el
  /usr/share/agda/emacs-mode/agda-input.el
  /usr/share/agda/emacs-mode/agda2-highlight.el
  /usr/share/agda/emacs-mode/agda2-mode.el

但这也没有用。

我也尝试了不同的文件：

{- My Agda Tutorial-}

Module Tut where

open import Data.List

rev : {A : Set} -> List A -> List A

变化不大，但在我尝试对文件进行类型检查时也给了我这个错误

/usr/share/agda/lib/_build: createDirectory: permission denied
(Permission denied)

关于如何解决这个问题的任何想法？我真的很想使用我相同的厄运配置。

【问题讨论】：

标签： emacs syntax-highlighting manjaro agda-mode

【解决方案1】：

语法高亮只在我保存后才会出现

这是有意的。缓冲区已成功键入后发生着色。您正在尝试解决一个可能不存在的问题。

由于类型检查缓冲区是 Agda 开发中必不可少的部分，因此您应该不会很难习惯在编程时经常这样做。

为了手动调用类型检查器，快捷方式是CTRL-C CTRL-L。

【讨论】：