[Agda] help with math symbols

[Dominique Devriese]

Oh, and while you're at it: what output do you get if you run the command

  bash -c "agda-mode locate"

?

Thanks
Dominique

2012/7/30 Dominique Devriese <dominique.devriese at gmail.com>:
> Serge,
>
> What output do you get if you run the command "agda-mode locate" in a
> shell (outside of emacs)?
>
> Thanks
> Dominique
>
> 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"
>> "/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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda