Library (.agda-lib) files below the project root

[nad]

Consider the following situation:

• The top-level directory contains the file top.agda-lib, and no other files:

  name:    top
  include: .
  flags:   --safe
  

• The subdirectory A contains the file B.agda:

  module A.B where
  
  {-# NON_TERMINATING #-}
  
  easy : (A : Set) → A
  easy = easy

Would you expect Agda to complain if you run agda A/B.agda in the top-level directory? I would have hoped so, but that is not necessarily the case. See what happens if the directory A contains B.agda and the empty file sneaky.agda-lib (and no other files):

$ agda A/B.agda
Checking A.B ([…]/A/B.agda).

In this case the module name of A.B suggests to me that any .agda-lib files for this module should be in a parent directory of A. I consider the current behaviour to be a bug.

[jespercockx]

Yep, I agree that this is a bug. We should probably have a check that the root of the hierarchy of top-level modules corresponds to the location of the .agda-lib file.

[nad]

That would mean that you could not have the source files in a subdirectory (like src). I've changed the code so that the .agda-lib files have to be in or above the root directory.

[nad]

I suggested a further change (#6465).

[nad]

I noticed that one part of the documentation should be updated:

agda/doc/user-manual/tools/interface-files.rst

Lines 31 to 34 in f926e3d

	If the ``.agda`` source file is part of a project with an *identifiable root*
	(i.e. if there is an ``.agda-lib`` file in any of the directories above it),
	then the interface file is stored in the ``_build/VERSION`` directory at the
	identified root. This prevents losing the interface file when switching between

[andreasabel]

I noticed that one part of the documentation should be updated:

Please open a new issue for this. We should proceed with the release now. Documentation shortcomings don't count as release-blockers at this stage.

[nad]

I have already created a pull request.