[Agda] Path to the standard library for the command line compiler

[José Pedro Magalhães]

Oh ok, a simple matter of adding --include-path=. then.


Thanks,
Pedro

2012/1/11 Nils Anders Danielsson <nad at chalmers.se>

> On 2012-01-11 16:29, José Pedro Magalhães wrote:
>
>> I'm trying to compile an Agda file with the command line compiler.
>> This file uses the standard library, so I'm using the --include-path
>> flag to point to the location of the standard library:
>>
>>    agda --include-path="C:\agda2\lib-**0.5\src" code.agda
>>
>> But the compiler complains with:
>>
>>    The name of the top level module does not match the file name. The
>>    module code should be defined in one of the following files:
>>    C:\agda2\lib-0.5\src\code.agda
>>    C:\agda2\lib-0.5\src\code.**lagda
>>
>> Why is this? The file loads fine in emacs (with the agda2-include-dirs
>> Emacs mode variable set appropriately). This is with version 2.2.10,
>> on Windows.
>>
>
> If you set the include path manually, then the current directory is not
> included automatically.
>
> From the release notes for Agda 2.2.6:
>
> * If a file F is loaded, and this file defines the module M, it is an
>  error if F is not the file which defines M according to the include
>  path.
>
>  Note that the command-line tool and the Emacs mode define the
>  meaning of relative include paths differently: the command-line tool
>  interprets them relative to the current working directory, whereas
>  the Emacs mode interprets them relative to the root directory of the
>  current project. (As an example, if the module A.B.C is loaded from
>  the file <some-path>/A/B/C.agda, then the root directory is
>  <some-path>.)
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120111/5b2e6ced/attachment.html