Подсветка синтаксиса для Agda-mode 2 в Doom Emacs

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 в.emacs.d и вместо этого поместив его в свой.init.el в.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)

Есть мысли, как это исправить? Я бы очень хотел использовать ту же конфигурацию doom.

Answer 1

подсветка синтаксиса происходит только после сохранения

Это задумано. Окрашивание происходит после того, как буфер был успешно набран. Вы пытаетесь решить проблему, которой предположительно не существует.

Поскольку проверка типов в буфере является важной частью разработки Agda, вам не составит труда привыкнуть к ее частому выполнению во время программирования.

Чтобы вручную вызвать проверку типов, используйте ярлык CTRL-C CTRL-L.