[Agda] Re: Dependencies for compiling agda, principal question

[James Chapman]

I would just like to point out that, as I learned recently from an
agda list discussion, you can compile the current darcs version of
agda with ghc 6.10.4 (16 July 2009). You just have to do without
Darin's patches for now:

$ darcs obliterate --match='author dwm at cs.nott.ac.uk'

It's nice to have the development version as it has pattern matching
and performance improvements for records.

Even without this workaround I don't think it's so bad that the
development version of agda depends on the most recent stable version
of ghc (6.12.1 - 14 December 2009). It's not like it requires the
latest unstable development version of ghc.

The annoying thing is that various linux distributions are slow at
adding updating their version of ghc. But, ghc is much easier and
faster to build yourself these days. It works out of the box most of
the time and can be installed easily in an isolated manner in
somewhere like /usr/local.

James

On Wed, Apr 21, 2010 at 9:57 PM, Ulf Norell <ulfn at chalmers.se> wrote:
>
> On Wed, Apr 21, 2010 at 8:41 PM, Stefan Monnier <monnier at iro.umontreal.ca>
> wrote:
>>
>> > Sure, it may make the development version more difficult to build and
>> > use for non-developers, but then I think that non-developers probably
>> > shouldn't try to use the development version to begin with.
>>
>> That would tend to put off developers.
>> I would also be interested to hear a concrete response to the OP's
>> question: which features justify that Agda only works with the very
>> latest version of every other library it links to (or at least, so it
>> seems).  As a naive outsider, I'd expect that a tool like Agda would
>> compile just fine with 2-year old tools (tho maybe less efficiently).
>
> The concrete answer is what Darin said:
> On Tue, Apr 20, 2010 at 12:30 PM, Darin
> Morrison <darinmorrison at gmail.com> wrote:
>>
>> The Cabal support for Agda that I have been working on essentially
>> requires the latest version.
>
> In general we try to keep Agda compatible with the two most recent ghc
> releases, but in this
> case the changes between ghc-6.10 and ghc-6.12 (or the corresponding Cabal
> releases) were
> too big to make the effort worthwhile.
> / Ulf
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>