Oh ok, a simple matter of adding --include-path=. then.<br><br><br>Thanks,<br>Pedro<br><br><div class="gmail_quote">2012/1/11 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 2012-01-11 16:29, José Pedro Magalhães wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm trying to compile an Agda file with the command line compiler.<br>
This file uses the standard library, so I'm using the --include-path<br>
flag to point to the location of the standard library:<br>
<br>
agda --include-path="C:\agda2\lib-<u></u>0.5\src" code.agda<br>
<br>
But the compiler complains with:<br>
<br>
The name of the top level module does not match the file name. The<br>
module code should be defined in one of the following files:<br>
C:\agda2\lib-0.5\src\code.agda<br>
C:\agda2\lib-0.5\src\code.<u></u>lagda<br>
<br>
Why is this? The file loads fine in emacs (with the agda2-include-dirs<br>
Emacs mode variable set appropriately). This is with version 2.2.10,<br>
on Windows.<br>
</blockquote>
<br></div></div>
If you set the include path manually, then the current directory is not<br>
included automatically.<br>
<br>
>From the release notes for Agda 2.2.6:<br>
<br>
* If a file F is loaded, and this file defines the module M, it is an<br>
error if F is not the file which defines M according to the include<br>
path.<br>
<br>
Note that the command-line tool and the Emacs mode define the<br>
meaning of relative include paths differently: the command-line tool<br>
interprets them relative to the current working directory, whereas<br>
the Emacs mode interprets them relative to the root directory of the<br>
current project. (As an example, if the module A.B.C is loaded from<br>
the file <some-path>/A/B/C.agda, then the root directory is<br>
<some-path>.)<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br>