[Agda] Agda beginner
mukesh tiwari
mukeshtiwari.iiitm at gmail.com
Wed Jan 16 23:29:59 CET 2013
Hi Guillaume
Thank you for reply. It's already in path as suspected by you. Below is all
the output
Mukeshs-MacBook-Pro:~ mukeshtiwari$ agda -V
Agda version 2.3.2
Mukeshs-MacBook-Pro:~ mukeshtiwari$ agda
Agda
Usage: agda [OPTIONS...] [FILE]
-V --version show version number
-? --help show this help
-I --interactive start in interactive
mode
--interaction for use with the
Emacs mode
-c --compile compile program using
the MAlonzo backend (experimental)
--epic compile program using
the Epic backend
--js compile program using
the JS backend
--compile-dir=DIR directory for
compiler output (default: the project root)
--ghc-flag=GHC-FLAG give the flag
GHC-FLAG to GHC when compiling using MAlonzo
--epic-flag=EPIC-FLAG give the flag
EPIC-FLAG to Epic when compiling using Epic
--test run internal test
suite
--vim generate Vim
highlighting files
--latex generate LaTeX with
highlighted source code
--latex-dir=DIR directory in which
LaTeX files are placed (default: latex)
--html generate HTML files
with highlighted source code
--dependency-graph=FILE generate a Dot file
with a module dependency graph
--html-dir=DIR directory in which
HTML files are placed (default: html)
--css=URL the CSS file used by
the HTML files (can be relative)
--ignore-interfaces ignore interface
files (re-type check everything)
-i DIR --include-path=DIR look for imports in
DIR
--no-forcing disable the forcing
optimisation
--safe disable postulates,
unsafe OPTION pragmas and primTrustMe
--show-implicit show implicit
arguments when printing
--show-irrelevant show irrelevant
arguments when printing
-v N --verbose=N set verbosity level
to N
--allow-unsolved-metas allow unsolved meta
variables (only needed in batch mode)
--no-positivity-check do not warn about not
strictly positive data types
--no-termination-check do not warn about
possibly nonterminating code
--termination-depth=N allow termination
checker to count decrease/increase upto N (default N=1)
--no-coverage-check do not warn about
possibly incomplete pattern matches
--type-in-type ignore universe
levels (this makes Agda inconsistent)
--sized-types use sized types
(inconsistent with coinduction)
--injective-type-constructors enable injective type
constructors (makes Agda anti-classical and possibly inconsistent)
--guardedness-preserving-type-constructors treat type
constructors as inductive constructors when checking productivity
--no-universe-polymorphism disable universe
polymorphism
--universe-polymorphism enable universe
polymorphism (default)
--no-irrelevant-projections disable projection of
irrelevant record fields
--experimental-irrelevance enable potentially
unsound irrelevance features (irrelevant levels, irrelevant data matching)
--without-K disable the K rule
(maybe)
--copatterns enable definitions by
copattern matching
Plugins:
Mukeshs-MacBook-Pro:~ mukeshtiwari$ type agda
agda is hashed (/Users/mukeshtiwari/.cabal/bin/agda)
Emacs env output
SHELL=/bin/bash
TERM=dumb
TMPDIR=/var/folders/r5/x23sscw14xg3d6kxwskg_d700000gn/T/
Apple_PubSub_Socket_Render=/tmp/launch-XMjl4B/Render
EMACSDATA=/Applications/Emacs.app/Contents/Resources/etc
EMACSPATH=/Applications/Emacs.app/Contents/MacOS/bin
USER=mukeshtiwari
COMMAND_MODE=unix2003
SSH_AUTH_SOCK=/tmp/launch-1YB3YP/Listeners
Apple_Ubiquity_Message=/tmp/launch-TLU6oJ/Apple_Ubiquity_Message
__CF_USER_TEXT_ENCODING=0x1F5:0:0
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
PWD=/Users/mukeshtiwari
EMACSLOADPATH=/Applications/Emacs.app/Contents/Resources/site-lisp:/Applications/Emacs.app/Contents/Resources/lisp:/Applications/Emacs.app/Contents/Resources/leim
SHLVL=1
HOME=/Users/mukeshtiwari
LOGNAME=mukeshtiwari
INFOPATH=/Applications/Emacs.app/Contents/Resources/info:
DISPLAY=Mukeshs-MacBook-Pro.local
EMACSDOC=/Applications/Emacs.app/Contents/Resources/etc
_=/usr/bin/env
Regards
Mukesh Tiwari
On Thu, Jan 17, 2013 at 3:47 AM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:
> 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.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
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130117/d46a5caf/attachment-0001.html
More information about the Agda
mailing list