时间戳

首页 > 解决方案 > Doom Emacs 中 Agda-mode 2 的语法高亮显示

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

问题描述

我需要帮助让 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")))

到我的 .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)

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

标签： emacssyntax-highlightingmanjaroagda-mode

解决方案

语法高亮仅在我保存后发生

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

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

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

推荐阅读