[Agda] Are .agdai files portable?

[Nicolas Pouillard]

On Sun, 11 Apr 2010 22:45:12 +0100, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> 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.)

A hash of some normalization (at least ignoring comments, extra whitespaces)
function would be really nice.

Regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr