[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

Usage: agda [OPTIONS...] [FILE]

  -V      --version                                   show version number
  -?      --help                                      show this help
  -I      --interactive                               start in interactive
          --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
          --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
          --no-forcing                                disable the forcing
          --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
          --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
          --copatterns                                enable definitions by
copattern matching

Mukeshs-MacBook-Pro:~ mukeshtiwari$ type agda
agda is hashed (/Users/mukeshtiwari/.cabal/bin/agda)

Emacs env output


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