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

[Nils Anders Danielsson]

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