[Agda] Are .agdai files portable?

[Nils Anders Danielsson]

On 2010-04-11 20:20, kahl at cas.mcmaster.ca wrote:
> Are .agdai files portable?

Yes, since 2.2.6, but they are dependent on a particular version of
Agda.

> If yes, is this by design, or by accident?

By design.

> Would checking a shipped .agdai file against the underlying .agda theories
> be any easier than recreating the .agdai file?

If you want to ship sources + .agdai files, then you need to make sure
that the .agdai files are unpacked with time stamps that are at least as
new as those of the source files, because otherwise Agda will ignore
them. (Using some kind of hash of the source would be nicer;
contributions are welcome.)

--
/NAD