agda-mode not installing onto any version of emacs

Question

Agda Mode, the tool used to aid in the discovery of proofs alongside the program initialised by the agda-setup command is not working. I have tried this through sudo usage and have the same error.

The error I get, is below:

lukemccartney@Lukes-MacBook-Pro ~ % sudo agda-mode setup
Password:
FAILED: emacs --batch --user '' --eval '(with-temp-file "/tmp/askEmacs2284-0" (insert (expand-file-name user-init-file)))'
Exception: emacs: rawSystem: posix_spawnp: permission denied (Permission denied)
Executable emacs at: (not found)
PATH:
  - /opt/local/bin
  - /opt/local/sbin
  - /Users/lukemccartney/.cargo/bin
  - /Library/Frameworks/Python.framework/Versions/3.8/bin
  - /usr/local/bin
  - /usr/bin
  - /bin
  - /usr/sbin
  - /sbin
  - /usr/local/Cellar/llvm@12
  - /var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/local/bin
  - /var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/bin
  - /var/run/com.apple.security.cryptexd/codex.system/bootstrap/usr/appleinternal/bin
  - /opt/X11/bin
  - /Library/Apple/usr/bin
  - /Library/TeX/texbin
  - /Applications/Wireshark.app/Contents/MacOS
  - /Applications/VMware Fusion.app/Contents/Public
  - /usr/local/share/dotnet
  - ~/.dotnet/tools
  - /usr/local/go/bin
  - /Library/Frameworks/Mono.framework/Versions/Current/Commands
  - /Users/lukemccartney/.cabal/bin
  - /Users/lukemccartney/.ghcup/bin

I have tried installing via sudo I have also tried to move a version of emacs to the locations listed in the error but keep getting the same error.

Answer 1

agda-mode that you're attempting to setup is an Emacs mode for Agda, meaning you need to have Emacs installed to be able to use the mode, which you don't have according to

emacs --version zsh: command not found: emacs

So make sure to install Emacs and put it on your $PATH.

Note that some other editors like Atom and Vim also have an Agda mode.

You can find information about the Emacs Agda mode as well as references to the other modes here.