[Agda] Emacs Agda mode is not working

Álvaro García Pérez agarcia at babel.ls.fi.upm.es
Wed Dec 3 16:21:08 CET 2008


Hi to everybody,

I'm having problems to run Agda mode on Emacs. I recently upgraded my system
to Ubuntu8.10 and Emacs22, and installed Agda2 (following Anton Setzer's
guide). I've also generetad the Agda batch tool and runned "make test". The
Agda installation seems to be Ok. Then I've installed haskell-mode-2.4 in
/usr/share/emacs22/site-lisp/haskell-mode-1.4 and coppied the files from
Agda/src/full/Agda/Interact/emacs-mode/*.el to
/usr/share/emacs22site-lisp/agda-mode. Finally, I've created the file
agdainstall.el in /usr/share/emacs22/site-lisp/agda-mode and modified
.emacs.

I run Emacs and it is not able to load any .agda file (it freezes and the
status bar says "no changes need to be saved").

These are the contents of the files .emacs and agdainstall.el:
.emacs:
(load "/usr/share/emacs22/site-lisp/haskell-mode-2.4/haskell-site-file")
(add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
(add-hook 'haskell-mode-hook 'turn-on-haskell-indent)
;;(add-hook 'haskell-mode-hook 'turn-on-haskell-simple-indent)
(load "/usr/share/emacs22/site-lisp/agda-mode/agdainstall.el")

agdainstall.el:
(setq load-path (cons "/usr/share/emacs22/site-lisp/agda-mode/" load-path))
(setq load-path (cons "/usr/share/emacs22/site-lisp/haskell-mode-2.4/"
load-path))
(autoload 'agda2-mode "agda2-mode" "Agda2 mode." t)
(add-to-list 'auto-mode-alist '("\\.l?agda$" . agda2-mode))
(modify-coding-system-alist 'file "\\.l?agda$" 'utf-8)
(add-hook 'agda2-mode-hook
           '(lambda nil
              (require 'quail)
              (set-input-method 'Agda)
              ))

I've also tried to modify agdainstall.el following the README file in the
Agda directory

(add-to-list 'load-path "/usr/share/emacs22/site-lisp/haskell-mode-2.4/")
(add-to-list 'load-path "/usr/share/emacs22/site-lisp/agda-mode/")
(require 'agda2)
(add-hook 'agda2-mode-hook
      '(lambda ()
         (inactive-input-method)
         (set-input-method 'Agda)
         ))

but the same thing happens.

Does anybody have a clue?

Thanks,

Alvaro.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081203/4953ddd4/attachment.html


More information about the Agda mailing list