[Agda] .agdai weirdness

[Ulf Norell]

On Sun, Mar 2, 2008 at 12:27 PM, Conor McBride <conor at strictlypositive.org>
wrote:

> Hi folks
>
> When I try to load UntypedLambda.agda, it fails at
> import Syntacticosmos with the following error:
>
>   /Users/ctm/Desktop/Syntacticosmos/UntypedLambda.agda:6,1-22
>   /Users/ctm/Desktop/Syntacticosmos/Syntacticosmos.agdai:
>   getModificationTime: does not exist (No such file or directory)


I don't think I've seen that before.


> Moreover, by the joy of Finder, I watched the directory
> as this ran. The file Syntacticosmos.agdai appeared and
> then disappeared in the course of the failed load.
> My attempts to mimic the pattern of files with similar
> structure but less distraction have not reproduced the
> problem. I hope you enjoy the distraction...


If things go badly wrong the interface file is removed to avoid creating
corrupt interfaces. That could be what's going on.


> How should I be organizing the library modules, anyway?


That's anyone's guess at the moment, I think.

Er, um, I'm afraid I've (tried and) failed to condense
> the problem to a toy example, so I'll summarize. If
> you want a tar of the files, just ask.
>

A tar would be helpful. I'm also curious about what kind of hackery you've
been up to :-)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080302/21109357/attachment.html