Avoid discarding cached interfaces

[nad]

I often use the following setup in my Agda libraries:

• The exported source files are placed in a subdirectory src.
• Other files are placed elsewhere. One example might be a file ./README.agda that provides an overview over the library, importing modules located in src.
• The .agda-lib file lists src as the only include directory.

In order to be able to type-check ./README.agda I include -i. in the Agda program options. However, this has a drawback: If I load ./README.agda and then load some file in src, then Agda discards cached interface files, because the include directories have changed. As a workaround I sometimes temporarily put . in the include directories. I would like to find a more principled solution to this problem.

[gallais]

Would it help to turn -i into a pragma option? You'd be able to mention that additional path directly at the top of README.

[nad]

I don't think it should be possible to change the include directories inside a module.

[UlfNorell]

I guess the right thing to do would be to keep the cached interfaces and check that they refer to the module you expect when trying to load them.

[nad]

I assume that you mean file rather than module.

I don't think it's quite as easy as that. What if you have changed the include path so that some module that the given file depends on now resides in a different file?

[UlfNorell]

Right.

I believe we store the module (file? I'm unclear on when I'm allowed to use which word) dependencies in the interface. Maybe the best thing to do would be to prune the cached interfaces when the include path changes and throw out any interfaces with changed dependencies.

[nad]

Maybe the best thing to do would be to prune the cached interfaces when the include path changes and throw out any interfaces with changed dependencies.

I've implemented something like that.

Switching between different libraries can still be slow. One could imagine storing the decoded libraries that are now discarded in a separate data structure, and reusing them if, say, the old include paths are restored (and nothing else has changed). However, I don't think we should waste memory on this.