Installation of Agda from Binaries under Linux (Unofficial)

• Download the binaries: emacsagda to anywhere. Make it executable (by using from a shell in the directory where emacsagda is located the linux command chmod u+x emacsagda )
• Installation of the elisp files for XEmacs/Emacs (we assume that XEmacs or Emacs is already installed on your machine).
  • If using emacs
    • Download
      • agda-additions-to-dotemacsfile.el
      • agda-mode.el
      • agda-additions-by-setzer-for-emacs.el
      • haskell-indent.el
      • haskell-mode.el
    • Then add the content of the file agda-additions-to-dotemacsfile.el you have downloaded to your ~/.emacs file. However you need to adapt the path mentioned in that file.
      • Comments in this file start with ';'
      • Follow the comments which explain you how to adapt the paths.
  • If using XEmacs
    • Download
      • agda-additions-to-dotxemacsinit.el
      • agda-startup.el
      • agda-mode-modified-for-xemacs-vers4.el
      • agda-additions-by-setzer.el
      • haskell-indent.el
      • haskell-mode.el
    • Then add the content of the file agda-additions-to-dotxemacsinit.el you have downloaded to your ~/.xemacs/init.el file. However you need to adapt the path mentioned in that file.
      • Comments in this file start with ';'
      • Follow the comments which explain you how to adapt the paths.
• Compile your files ~/.emacs (Emacs) or ~/.xemacs/init.el (XEmacs) and all the files you have downloaded by using from emacs M-x byte-compile-file (M-x stands for Escape x; it asks for the file name to be compiled).
• To test it, start a new Emacs and open a file called test.agda, (.agda tells Emacs to switch to agda-mode), and type in the following line
  A :: Type = Set
  Then type check it using the menu "Agda" on the emacs, or alternatively using C-c C-x C-b. If no error occurs, the installation should be okay.