[Agda] Agda beginner

[Guillaume Brunerie]

Hello,

Emacs does not find the executable agda.
Does the `agda' command works in a terminal?
If it does, you can type `type agda' in order to find out where agda
is installed and add it to your PATH in the .emacs
What is a bit strange is that agda is most likely installed in
/Users/mukeshtiwari/.cabal/bin which is included in your PATH…

Best,

Guillaume

2013/1/16 mukesh tiwari <mukeshtiwari.iiitm at gmail.com>:
> Hello all
> I started learning agda and installed gnu-emacs version 24.2 and I followed
> all the instructions given of wiki except aquamacs and library installation
> ( Currently I am not trying to import any library ). I have written this
> small code  Test.agda
>
> Module Test
>
> data Bool : Set where
>   true : Bool
>   false : Bool
>
> I am not getting any syntax highlights and when I am opening this file ( C-f
> C-x )  , getting errors
>
> File mode specification error: (file-error "Searching for program" "No such
> file or directory" "agda") [2 times]
> (No changes need to be saved)
> Starting agda process `agda'.
> apply: Searching for program: No such file or directory, agda
> progn: Another command is currently in progress
> (if a command has been aborted you may want to restart Agda)
>
> I am using ghc-7.6.1 , Agda-2.3.2 and mtl-2.1.2 ( After bit of searching I
> got this post https://lists.chalmers.se/pipermail/agda/2012/004675.html but
> the problem was mtl-2.1 which is not in my case ).  My .emacs file
> configuration is
>
> ; sane path
> (setq path
> "/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin:/Users/mukeshtiwari/.cabal/bin:/Users/mukeshtiwari/Erlang/bin:/Users/mukeshtiwari/Programming/Scala/scala-2.10.0/bin:/usr/local/smlnj-110.75/bin")
>  (setenv "PATH" path)
>
> (load-file (let ((coding-system-for-read 'utf-8))
>                 (shell-command-to-string "agda-mode locate")))
>
> (put 'downcase-region 'disabled nil)
>
>
> Kindly tell me how to resolve this issue.
>
> Regards
> Mukesh Tiwari
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>