[Agda] Incompatible interface files?

[Dirk Ullrich]

Hi,

I've just built Agda2 from darcs' head.
It seems that the `agdai' files generated by the `agda' binary are not
compatible with those `agdai' files generated fron within Emacs' agda2
mode:

If I start from a Agda2 source file, say: `Foo.agda', and generate the
correspoding `Foo.agdai' by either:

1. agda Foo.agda

or

2. within Emacs' agda2-mode by `M-x agda2-load' from a buffer visiting
`Foo.agda'

I get different results:

a. The `Foo.agdai' from 1. and 2. are not identical; and

b. If do 1. after 2. or the other way round the `Foo.agdai' will
always generated anew.

Is this indented (or at least tolerated) behavior now?

Dirk