Interface files

Note

This is a stub. Contributions, additions and corrections are greatly appreciated.

When an .agda file is saved, another file with the same name and extension .agdai is automatically created. The latter file is what we call an interface file.

Interface files store the results from the type-checking process. These results include:

• A translation of pattern-matching definitions to case trees (this translation speeds up computation).
• The resolution of all implicit arguments. (Note: under the flag --allow-unsolved-metas not all implicit arguments need to be resolved to create an interface file.)

Storage

In projects that do not use any Agda library, the .agdai files are stored alongside the .agda source file.

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 agda versions. You can revert this behaviour with the flag --no-project.

Note

When an .agda file is renamed, the old .agdai file is kept, and a new .agdai file is created. This is the intended behavior, and the orphan files can be safely deleted from the user’s file system if needed.

The compression run to create .agdai files introduces sharing. Sharing improves the memory efficiency of the code loaded from interface files.

The syntax represented in .agdai files differs significantly from the syntax of source files.

Compilation

An external module is loaded by loading its interface file. Interface files are also intermediate points when compiling through a backend to e.g. Haskell.