Doom Emacs中Agda-模式2的语法突出显示

Question

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

agda-mode setup

它所做的是添加

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

到我.emacs.d文件中的.emacs.d。所以我觉得一切都很好。然而，当我启动emacs时，我尝试使用我在网上找到的一些文件来学习agda ( https://oxij.org/note/BrutalDepTypes.lagda)。但是，只有在保存文件时才会出现语法突出显示，而且任何新文本在保存之前都不会着色。我试图解决这个问题，方法是从.init.el中删除.emacs.d中的代码，然后将其放在.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)

对如何解决这个问题有什么想法吗？我真的很想使用我的相同的厄运配置。

Answer 1

语法高亮显示仅在我保存

这是故意的。该颜色发生在缓冲区已成功键入之后。你在试图解决一个大概不存在的问题。

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

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