[Agda] Re: Good old times... (install trouble)

[Darin Morrison]

On Sun, Feb 15, 2009 at 3:29 PM, Stefan Monnier
<monnier at iro.umontreal.ca> wrote:

> Also, when you finally get Agda compiled, be carefult to check out the
> Agda library as well at the same time, since it also evolves quickly and
> in the same kind of lockstep, apparently (e.g. it already uses → and λ,
> even tho these were added to Agda pretty recently).
>
> What it means for me is "now that I got a working Agda and library,
> I'll stick to it for a (long) while".  Which is kind of a pity for
> a package that evolves so quickly.

It's true that the standard library and the agda code itself both
evolve quickly but I haven't run into any problems with breakage due
to that.  My strategy is to do a darcs pull of the standard library
roughly once a week.  Occasionally this triggers a slightly longer
than usual type checking session if I happen to be using one of the
updated modules but that's not so bad.  I tend to update my main agda
install less frequently, but even then I haven't had any real issues.
Re-compilation is usually incremental and quick.

> So my question is: why is it that the latest Agda code always has to
> depend on the very latest of everything else.

Several of the packages that the Agda code depends on don't
necessarily need the very latest versions available.

I think the problem is that interest in Agda2 has been growing quite
rapidly in recent times (at least from what I can tell) even though
it's still under active development.  This makes sense given how
usable the system already is and given the impressive progress it has
made in the last year or so.  But as the number of non-developer type
users continues to increase, maybe it is time to start thinking about
a more stable release schedule for the interpreter and the standard
library.

-- 
Darin