Мне нужна помощь в настройке режима agda для моей системы emacs. По сути, подсветка синтаксиса происходит только после сохранения, а не в реальном времени, как в других стандартных режимах. Я сделал урок по основам c. Я запускаю 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 и попытался использовать какой-то файл, который я нашел в inte rnet, чтобы узнать 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-конфиг.