Feature request: default flags in .agda-lib file

[jespercockx]

It would be nice if we could put some default flags for an entire library in its .agda-lib file, like for Cabal. For example this would be very useful for --without-K or --safe. Or is there already an easy way to get the same effect?

[nad]

I think that the flags should only apply to the modules in the given library, not to the dependencies. See also #4029 and #2770, and perhaps #4272.

[jespercockx]

I've been trying to implement this. The main issue seems to be that currently, the only thing .agda-lib files do is add some implicit command-line options to the call to the agda executable. However, if we would treat flags in the .agda-lib file as command-line flags, that means the flags are applied to all imports, including those from outside the library. Worse, importing a library with default flags would also apply those flags to the current file. This is not the behaviour we'd want.

Instead we want the library flags to only apply to the things in the current library, and let the (co)infection rules do their job for flags such as --safe or --rewriting. However, this seems to require adding the concept of a "library" to Agda proper, rather than just the preprocessor for command-line flags which we have currently. This takes away a bit from the "lightweight" aspect of the current approach, but that's not necessarily a bad thing.

[jespercockx]

One problem is that the current approach searches for an .agda-lib file once per call to the agda executable, the new approach would do this once per file that is checked. So any performance problems (such as #4526) would suddenly get a lot worse. We might try to cache the results of looking for the .agda-lib file if that becomes a problem in practice.

[gallais]

We are already storing information about the directories in scope for
import resolution. Each one could come with a set of options attached
to it.

[andreasabel]

Thanks, @jespercockx !