[Agda] Agda-mode problems in 2.3.2

[Dominic Mulligan]

(Mistakenly replied in private to Peter before without CCing to the
list).

Thanks Peter for the suggestion, however agda-mode compile did not fix
the problem, nor did updating my version of emacs to 24.30.5.1.  I'm at
a loss here: Agda 2.3.2 is not usable on my machine.

Thanks,
Dominic

On Sat, 2013-01-26 at 19:22 +0100, Peter Divianszky wrote:
> I'm not sure but maybe 'agda-mode compile' is needed too?
> 
> Peter
> 
> On 01/25/2013 06:28 PM, Dominic Mulligan wrote:
> > Hi,
> >
> > 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.)
> >
> > Thanks,
> > Dominic
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>