[Agda] yet another grinding reload

[Ulf Norell]

On Mon, Mar 22, 2010 at 11:13 PM, Conor McBride
<conor at strictlypositive.org>wrote:

> Hi folks
>
> Loading the file and committing that
> refinement takes a while: it's done in less than half a minute on
> my pathetic-but-thin computer. However (you guessed it) loading
> the completed proof just does not want to happen.
>
> But it might also be worth trying to figure out what the reason
> for the discrepancy is. I'm sure it's known that it's a problem,
> but is it known what problem it is?


I just had a quick look and it's termination checking that takes most
of the time when reloading. We don't do termination checking after a
refinement (maybe we should), so that's why refining the goal works
and not reloading. It seems that the reason for it taking so long is that
the term you give is massive after all the implicit arguments are in
place.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100326/b027fb17/attachment.html