I need help getting agda mode to work on my emacs system. Essentially, syntax highlighting only occurs after I save and not in real time like other standard modes. I did the basic tutorial. I run Manjaro on my system so I used pacman to install agda (2.6.0.1) and agda-stdlib (1.2-1). After that, I did
agda-mode setup
What this did was add
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
to my .init.el in my .emacs.d file. So then, I thought everything was well. However, when I did boot up emacs and I tried using some file I found on the internet to learn agda ( https://oxij.org/note/BrutalDepTypes.lagda). However, there only seems to be syntax highlighting when I save the file and any new text is not colored until saved. I tried to solve this by instead removing the code from .init.el in .emacs.d and instead putting it in my .init.el in .doom.d instead. But still I get the same results. I also did sudo agda-mode compile as well which gives me the following output:
Loading quail/latin-ltx...
I use sudo because otherwise I get this
>>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
But this failed to work too.
I tried a different file too:
{- My Agda Tutorial-}
Module Tut where
open import Data.List
rev : {A : Set} -> List A -> List A
which didn't change much, but also gave me this error when I tried to typecheck the file
/usr/share/agda/lib/_build: createDirectory: permission denied
(Permission denied)
Any thoughts on how to fix this? I would really like to use my same doom config.
syntax highlighting only occurs after I save
This is intended. The coloration occurs after the buffer has successfully been typecked. You are trying to solve an issue that presumably does not exist.
Since type checking the buffer is an essential part in an Agda development you should not have a hard time getting used to doing it often while programming.
In order to manually call the type checker, the shortcut is CTRL-C CTRL-L.