<div dir="ltr">I don&#39;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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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>
&gt; emacs Foo.agda<br>
<br>
  Ctrl-C Ctrl-l<br>
<br>
reports<br>
<br>
&quot;Another command is currently in progress<br>
(if a command has been aborted you may want to restart Agda)<br>
&quot;<br>
<br>
<br>
When installing Agda, I command<br>
<br>
  &gt; cabal install Agda<br>
<br>
  &gt; agda-mode compile<br>
<br>
And the file  .emacs  contains this:<br>
<br>
-----------------------------------------------------<br>
(custom-set-variables<br>
&#39;(agda2-include-dirs (quote (&quot;.&quot;<br>
   &quot;/home/mechvel/agda/stLib/oct8-2015/src&quot;)))<br>
&#39;(agda2-program-args (quote (&quot;+RTS&quot; &quot;-K200m &quot; &quot;-M14G&quot; &quot;-H14G&quot; &quot;-RTS&quot;))))<br>
<br>
(custom-set-faces<br>
)<br>
<br>
(load-file (let ((coding-system-for-read &#39;utf-8))<br>
                (shell-command-to-string &quot;agda-mode locate&quot;)))<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>