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

Question

我需要帮助让 agda 模式在我的 emacs 系统上工作。本质上，语法高亮仅在我保存后出现，而不是像其他标准模式那样实时出现。我做了基础教程。我在我的系统上运行 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")))

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

syntax highlighting only occurs after I save

这是故意的。成功输入缓冲区后会出现着色。您正在尝试解决一个可能不存在的问题。

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

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

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

Syntax highlighting for Agda-mode 2 in Doom Emacs

emacs

syntax-highlighting

manjaro

agda-mode