[Agda] help with math symbols

[Serge D. Mechveliani]

On Thu, Aug 02, 2012 at 10:38:28AM +0200, Dominique Devriese wrote:
> Serge,
> 
> 2012/8/2 Serge D. Mechveliani <mechvel at botik.ru>:
> >> > 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?
> >>
> >> Yes, that's what it should evaluate to and your solution works around
> >> the problem but will not work well after Agda updates. The question is
> >> why (shell-command-to-string "agda-mode locate") doesn't evaluate to
> >> "/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el".  The
> >> emacs function shell-command-to-string is supposed to return a string
> >> containing the output of the shell command you pass it. But you say
> >> that the "agda-mode locate" command yields the correct result in the
> >> shell but not when run using shell-command-to-string.
> >
> > Yes. I am in  tcshell:
> >
> >   > agda-mode locate
> >   /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
> >
> > -- without Newline in the end,
> >
> >   > bash -c "agda-mode locate"
> >   /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
> >
> > -- without Newline in the end.
> >
> > And         (shell-command-to-string "agda-mode locate")
> > evaluates to
> >             "/home/mechvel/stdin"
> > instead.
> 
> Are you sure?  The debug output in your first mail suggests it evaluates to
> 
> "/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"
> 
> (with the newline in the middle).

As I wrote earlier, I initially confused citing the message
(because I copied it by mouse and formatted it by hand, and made an
error).
  

> What output do you see if you do
>    bash -c "agda-mode locate" | less
> That might reproduce the problem as bash's output is then also not
> attached to a tty.

-- citation -----------
> bash -c "agda-mode locate" | less
/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
(END) 
-----------------------

-- these 3 lines in the middle of citation is what I see on the screen.
And the above expression
                        (shell-command-to-string "agda-mode locate")
evaluates to  "/home/mechvel/stdin"

And what is the idea?

Thanks,

------
Sergei