[Agda] Are .agdai files portable?

[Iain Lane]

Hi,

On Sun, Apr 11, 2010 at 10:45:12PM +0100, Nils Anders Danielsson 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.)

How portable? Are they dependent on architecture / endianness / anything 
else?

I'm thinking of my Debian packages here. If you take a look at

   https://buildd.debian.org/status/package.php?p=agda-stdlib

you can see that several of the weaker architectures are having trouble 
type cheking the whole standard library. Some OOM and some overflow the 
stack.

If I could compile for one of the arches where this is no trouble, such 
as x86, and use the built agdai files everywhere, then we wouldn't have 
a problem. Would this work?

Cheers,
Iain