[Agda] Agda-mode problems in 2.3.2

Dominic Mulligan dominic.p.mulligan at googlemail.com
Fri Jan 25 18:28:24 CET 2013


I have just updated my version of Agda to 2.3.2.  However, apparently
something has gone wrong with agda-mode as half of the functionality
that was there prior to the update is missing.  In particular, I am
unable to use auto (C-c C-a), display a goal and its context (C-c C-,)
or give a term by hand to solve a goal (C-c C-space).  Issuing these
commands inside a hole results in ... nothing, and there appears to be
no Agda menu entry for them either (though the Agda menu has changed
between versions, with more entries than there were before --- for
instance I now have entries like `Information about character at point'
that were not there prior to the update).  I can still load a file fine
with C-c C-l, get syntax highlighting, etc.

Further, Agda no longer seems to be issuing type checking errors.  When
it encounters a type error it merely underlines the problem in red in
the source file, but no buffers (Agda information, Agda2, etc.) contain
an error message.

What's going on?

Installed Agda by:

cabal update
cabal install --global Agda
agda-mode setup

(ghc --version: 7.4.1, agda-mode
locate: /usr/local/share/Agda-2.3.2/emacs-mode/agda2.el, 
agda --version: Agda version 2.3.2, emacs --version: GNU Emacs 23.3.1, 
Ubuntu 12.04.1 LTS 32 bit.)


More information about the Agda mailing list