[Agda] Agda under emacs

[Ulf Norell]

I don't know about the other stuff, but agda-include-dirs has been removed.
You can either use agda-program-args (with -iDIR) or use the new library
management system (recommended):
https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18.

/ Ulf

On Sat, Oct 17, 2015 at 6:13 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> People,
> I wonder: why Agda does not work any more under emacs under my settings?
>
> In old days (say, year ago) it worked.
>
> Now I try to run  Development Agda  of October 8 2015
> under  emacs.
>
> > emacs Foo.agda
>
>   Ctrl-C Ctrl-l
>
> reports
>
> "Another command is currently in progress
> (if a command has been aborted you may want to restart Agda)
> "
>
>
> When installing Agda, I command
>
>   > cabal install Agda
>
>   > agda-mode compile
>
> And the file  .emacs  contains this:
>
> -----------------------------------------------------
> (custom-set-variables
> '(agda2-include-dirs (quote ("."
>    "/home/mechvel/agda/stLib/oct8-2015/src")))
> '(agda2-program-args (quote ("+RTS" "-K200m " "-M14G" "-H14G" "-RTS"))))
>
> (custom-set-faces
> )
>
> (load-file (let ((coding-system-for-read 'utf-8))
>                 (shell-command-to-string "agda-mode locate")))
> -----------------------------------------------------
>
>
> For emacs, I always do
>
> -----------
> M-x load-library  RET  agda2-mode
> M-x customize-group RET agda2 RET
> -----------
>
> And then, I edit there the fields  Agrs,  include-dirs.
> But today, it does not suggest  include-dirs.
>
> In old days, all the above settings worked. And currently something is
> somehow twisted.
>
> Can you, please, advise of how to fix?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
>
> _______________________________________________
> 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/20151017/65006c11/attachment.html