[Agda] Re: Agda beginner

[mukesh tiwari]

Hello everyone
I managed to solve this. Seems like

(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)

is not good way to set paths in emacs.  I removed this line and added path
using the following.

(setenv "PATH" (concat "/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin:"
(getenv "PATH")))
(setq exec-path (cons "/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin"
exec-path))

(setenv "PATH" (concat "/Users/mukeshtiwari/.cabal/bin:" (getenv "PATH")))
(setq exec-path (cons "/Users/mukeshtiwari/.cabal/bin" exec-path))

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

Now its working fine.

Regards
Mukesh Tiwari



On Thu, Jan 17, 2013 at 3:32 AM, mukesh tiwari <mukeshtiwari.iiitm at gmail.com
> wrote:

> Hello all
> I started learning agda and installed gnu-emacs
> <http://emacsformacosx.com/>version 24.2 and I followed all the
> instructions given of wiki<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX>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.htmlbut 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130117/66afa22a/attachment.html