[Agda] Incompatible interface files?

Dirk Ullrich dirk.ullrich at googlemail.com
Tue Nov 2 18:04:40 CET 2010


Hallo Nils,

2010/11/2 Nils Anders Danielsson <nad at cs.nott.ac.uk>:
> On 2010-11-01 23:23, Dirk Ullrich wrote:
>>
>> 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:
>
> It sounds as if you didn't rebuild the "agda" executable; the interface
> file format changes rather frequently, so the two tools need to be in
> sync.
At first glance this was not so: I install Agda system-wide, and
before building and installing I always clean up both build and
installation directory. But at a closer look (and some hours later) I
discovered some user local left-over files from whatever former
installation attempt of Agda. After cleaning up this cruft everything
seems okay now.

Sorry for the noise - and thank you for the tip that put me on the
right track at the end!

Dirk


More information about the Agda mailing list