[Agda] help with math symbols

[Serge D. Mechveliani]

On Mon, Jul 30, 2012 at 01:56:30PM +0200, Dominique Devriese wrote:
> Oh, and while you're at it: what output do you get if you run the command
> 
>   bash -c "agda-mode locate"
> 
> ?

It yields
   /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el

Thanks to people for help.
Now, from the start 
(sorry, initially I confused the  emacs  report a bit): 
~/.emacs  contains 

 (load-file (let ((coding-system-for-read 'utf-8))
                 (shell-command-to-string "agda-mode locate")))

Thanks to my colleage, he noticed that the expression
                          (shell-command-to-string "agda-mode locate")

evaluates to  "/home/mechvel/stdin".
And it is natural to suppose that in my installation case this value
rather should be
       "/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el".
Right?
So, I reset  ~/.emacs  as

  (load-file
    (let ((coding-system-for-read 'utf-8))
         "/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el" ))
,
and now, emacs is improved, shows `Agda' in the menu when editing an
.agda file, and inputs the  \bn  symbol correctly.

The installation is almost all right now, and I see the two remaining 
points.
1. It is desirable to make
                      (shell-command-to-string "agda-mode locate")
   to evaluate to the needed string
   -- or to change respectively this point in the Agda README
   (?)
2. As \bn works now, and  emacs  displayes math symbols as needed,
   do I need further to issue the commands to 
   _customize_ emacs to Agda, to set an _input method_ ?

------
Sergei



> > 2012/7/30 Serge D. Mechveliani <mechvel at botik.ru>:
> >> (1) With empty  ~/.emacs,  emacs  loads without error.
> >>
> >> But according to README of Agda-2.3.0.1, I set  ~/.emacs  as
> >>
> >> (load-file (let ((coding-system-for-read 'utf-8))
> >>                 (shell-command-to-string "agda-mode locate")))
> >>
> >> And now, emacs loads with a certain error:
> >>                                            > emacs --debug-init
> >> reports
> >> ---------------------------------------------------------------------
> >> Debugger entered--Lisp error: (file-error "Cannot open load file"
> >> [..]