Agda: Better error message if include field is missing from .agda-lib file

[karljs]

Either I've misunderstood the documentation, or depending on a library using a .agda-lib file fails for me in Agda 2.5.2.

~/.agda/libraries contains:

/Users/karl/src/agda-stdlib/standard-library.agda-lib

~/a/.agda-lib contains:

name: a
depend: standard-library

~/a/a.agda contains:

module a where

When I load the a.agda file, I get the the following error. As far as I'm concerned, my file name does match my module name. Why is it looking for my file inside the standard-library directory instead of just loading that code?

The name of the top level module does not match the file name. The
module a should be defined in one of the following files:
  /Users/karl/src/agda-stdlib/src/a.agda
  /Users/karl/src/agda-stdlib/src/a.lagda
  /usr/local/Cellar/agda/2.5.2/share/x86_64-osx-ghc-8.0.1.20161213/Agda-2.5.2/lib/prim/a.agda
  /usr/local/Cellar/agda/2.5.2/share/x86_64-osx-ghc-8.0.1.20161213/Agda-2.5.2/lib/prim/a.lagda

[karljs]

I'll note that this works when I put the library in a defaults file, but I don't want to do that.

[karljs]

I figured this out. I'm required to put an explicit include: . in my .agda-lib file which was not clear to me from the documentation.

[nad]

Perhaps the error message could include a hint that one might want to consider adding an include field to some .agda-lib file.

We could also reject .agda-lib files without include fields, but I imagine that one might want to define "meta-libraries" without local source code.

[msuperdock]

This same issue happens when using the --library flag; see below for a minimal reproduction. (I almost posted this as a separate issue but then found this issue.) Based on the documentation, the current directory is added to the path only when there is no --library flag or .agda-lib file in the project root. So if you use the --library flag, you must also add the current directory to the path with --include-path=.. Similarly, if you use an .agda-lib file in the project root, you must also add the current directory to the path, either with --include-path=. or with include: . in .agda-lib.

I found this behavior surprising, and it took me a while to figure out what was going on. It makes sense to have to add the current directory to the path if the file you are compiling references files in the current directory. But it doesn't make sense to have to add the current directory to the path just to get past the module name check.

Here are a few possible solutions, at least that I can see:

• Solution 1: Always add the current directory to the path.
• Solution 2: Make the module name check allow the current directory as a root directory.
• Solution 3: Make a clearer error message that suggests one of the fixes above when the file has the right name but doesn't appear in the right directory.

Minimal example:

$ ls -a ~/
.agda
agda-stdlib-1.1
code
...

$ ls ~/.agda
defaults
libraries

$ ls ~/code
Test.agda

$ cat ~/.agda/defaults
standard-library

$ cat ~/.agda/libraries
~/agda-stdlib-1.1/standard-library.agda-lib

$ cat ~/code/Test.agda
module Test where

Successful check using the libraries specified by the defaults file:

$ cd ~/code
$ agda Test.agda
Checking Test (/home/matt/code/Test.agda).

Unexpected behavior:

$ cd ~/code
$ agda --library=standard-library Test.agda
/home/matt/code/Test.agda:1,8-12
The name of the top level module does not match the file name. The
module Test should be defined in one of the following files:
  /home/matt/agda-stdlib-1.1/src/Test.agda
  /home/matt/agda-stdlib-1.1/src/Test.lagda
  /nix/store/9db1xsvqjl2vbhqg41xkz4n7prb988bi-Agda-2.6.0.1-data/share/ghc-8.6.3/x86_64-linux-ghc-8.6.3/Agda-2.6.0.1/lib/prim/Test.agda
  /nix/store/9db1xsvqjl2vbhqg41xkz4n7prb988bi-Agda-2.6.0.1-data/share/ghc-8.6.3/x86_64-linux-ghc-8.6.3/Agda-2.6.0.1/lib/prim/Test.lagda

Workaround using --include-path=.:

$ cd ~/code
$ agda --library=standard-library --include-path=. Test.agda

(In the last example, there is no output; I think this means the Test.agda file checks.)

I am using agda version 2.6.0.1, on NixOS.