<div dir="ltr">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): <a href="https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18">https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18</a>.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Oct 17, 2015 at 6:13 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I wonder: why Agda does not work any more under emacs under my settings?<br>
<br>
In old days (say, year ago) it worked.<br>
<br>
Now I try to run Development Agda of October 8 2015<br>
under emacs.<br>
<br>
> emacs Foo.agda<br>
<br>
Ctrl-C Ctrl-l<br>
<br>
reports<br>
<br>
"Another command is currently in progress<br>
(if a command has been aborted you may want to restart Agda)<br>
"<br>
<br>
<br>
When installing Agda, I command<br>
<br>
> cabal install Agda<br>
<br>
> agda-mode compile<br>
<br>
And the file .emacs contains this:<br>
<br>
-----------------------------------------------------<br>
(custom-set-variables<br>
'(agda2-include-dirs (quote ("."<br>
"/home/mechvel/agda/stLib/oct8-2015/src")))<br>
'(agda2-program-args (quote ("+RTS" "-K200m " "-M14G" "-H14G" "-RTS"))))<br>
<br>
(custom-set-faces<br>
)<br>
<br>
(load-file (let ((coding-system-for-read 'utf-8))<br>
(shell-command-to-string "agda-mode locate")))<br>
-----------------------------------------------------<br>
<br>
<br>
For emacs, I always do<br>
<br>
-----------<br>
M-x load-library RET agda2-mode<br>
M-x customize-group RET agda2 RET<br>
-----------<br>
<br>
And then, I edit there the fields Agrs, include-dirs.<br>
But today, it does not suggest include-dirs.<br>
<br>
In old days, all the above settings worked. And currently something is<br>
somehow twisted.<br>
<br>
Can you, please, advise of how to fix?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>