[ fix #2610 ] Build directory for version specific agdai files

[gallais]

If an .agda 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 we create a _build/VERSION directory at that root and we
write the .agdai file storing its interface in it.

If it does not have an identifiable root then we simply store the
.agdai interface file alongside the file itself.

Additional refactoring: disambiguating between AbsolutePath standing
for source files and the ones standing for interface files.

[rwe]

• Should flags passed to the compiler (e.g. --with-K) be considered here too? Even for a given version of Agda, a particular source file might be interpreted differently when run with different flags. (And some flags are inherited transitively). I could imagine a naming scheme like .${AGDA_VERSION}-${FLAG_BITMAP}-${MODULE_NAME}.agdai. I believe the flags are encoded in the .agdai file itself, but that means they might be clobbered when alternating between projects.

• Instead of hard coding _build, I wonder if that should also be a command line (or project config) flag. That would facilitate things like a global shared cache (e.g. ${XDG_DATA_HOME}/agda/…) which might help when working on multiple workspaces.

Could make tracking issues for those, these are just drive-by thoughts!

[jespercockx]

OTOH, .agdai files are not small (65 MB for the standard library), so keeping too many different versions could eat up a lot of disk space. Maybe instead we could have a flag for specifying a different suffix when required?

[gallais]

Instead of hard coding _build, I wonder if that should also be a command line (or project config) flag.

I think a global configuration (similar to the libraries file) would make
more sense. Otherwise users would have to edit a library's .agda-lib file to
match the personal scheme they are using. Much easier if they can install them
without modifications.

[gallais]

That being said, I would be in favour of merging this as is. Currently the users
have no control whatsoever on where the .agdai files are placed so this change
is neutral with respect to a possible extension allowing them to pick a location.

[Saizan]

@gallais make install-bin is broken by this change if the agda directory happens to be in a subdir of an agda project, maybe there should also be a flag to always put the .agdai files by the correspnding sources?

The problem is with building and copying the builtin files in src/data/lib/prim/.

[gallais]

Right.

The easy option is to add a --no-project flag reverting to the old behaviour.
The better option is to only consider an .agda-lib file to be a project root
if the module we are considering would have a valid name in the include paths
this file mentions.

(For the agda-stdlib travis build I simply made sure I was building agda in a
part of the tree not below the standard-library.agda-lib file).

[fredrikNordvallForsberg]

On top of these suggestions (why not both?), wouldn't it also make sense to update Setup.hs's toIFile to match the semantics of Agda.Interaction.FindFile's toIFile? Or is that putting to much logic (and hence dependencies) into Setup.hs?

[nad]

@gallais make install-bin is broken by this change if the agda directory happens to be in a subdir of an agda project, maybe there should also be a flag to always put the .agdai files by the correspnding sources?

I tripped over this problem while running agda-bisect. I fixed a similar problem a while ago (#3648).

[guilhermehas]

I am using nix and my libraries are in $AGDA_PACKAGE_PATH environment variable.
It tries to compile agdai files in the directory of the library instead of my directory. This is a problem, because it can not write in the library directory.
Does someone here have the same problem as me? How to fix it?

[gallais]

Agda has always needed write access to the library's directory to write
interface files.

[nad]

This can presumably be fixed by creating the interface files when the library is installed (and recreating them when Agda is reinstalled).