[Agda] Agda beginner

mukesh tiwari mukeshtiwari.iiitm at gmail.com
Wed Jan 16 23:02:48 CET 2013


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.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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130117/77450339/attachment.html


More information about the Agda mailing list