[Agda] help with math symbols

[Serge D. Mechveliani]

People,
I need help in customizing  emacs  for math symbols in Agda.

The situation is as follows.
I have installed  Agda-2.3.0.1  and  lib-0.6  from source under
(Lenny) Debian Linux.


(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" 
"/home/mechvel/haskell/agda/lib-0.6/src/Data/stdin:  is not a tty
/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el")
  load("/home/mechvel/haskell/agda/lib-0.6/src/Data/stdin: is not a tty
\n/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el" nil nil t)
  load-file("stdin: is not a tty
\n/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el")
  eval-buffer(#<buffer  *load*> nil "/home/mechvel/.emacs" nil t)  ; 
Reading at buffer position 114
 load-with-code-conversion("/home/mechvel/.emacs" "/home/mechvel/.emacs" t t)
 load("~/.emacs" t t)
 #[nil "
---------------------------------------------------------------------

a) The directory  ~/haskell/agda/lib-0.6/src/Data/
                                                   (~ = /home/mechvel)
   contains many files but does not contain  stdin.

b) ~/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el    does exist.
c) The  putStrLn "Hello!"  program complies and runs correctly.

d) With this,  emacs  still shows correctly specific math symbols 
   in the  .adga  files,
but I cannot correctly _input_ these math symbols. For example,
my program 
          open import Nat
          ...
          f : \bn
          f = zero
does not compile, the compiler takes  \bn  as lambda.

Please, how to fix the setting?


(3) http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput
writes
--------------------------------------------------
How can I write Unicode characters using Emacs?
The Agda Emacs mode turns on a special input method [..]
This input method is highly customisable 

(via   M-x customize-group agda-input  ).
 
By default you can insert a number of symbols by typing their 
TeX/LaTeX names. For instance, if you type \forall then Б┬─ gets inserted
Some characters have key bindings which have not been taken from LaTeX 
(typing \bn results in Б└∙ being inserted, for instance)
[..]
--------------------------------------------------

The error of (1) still keeps emacs working, with many respects.
So, I tried in  emacs,  in the menu dialogue:  

  >  Alt-x
  e> M-x
  >  customize group
  e> Customize group (default emacs): 
  >  agda-input
  e> Customize group (default emacs): agda-input  no match

-- it somehow fails to customize. 

Thank you in advance for advice, 

------
Sergei
mechvel at botik.ru