[Agda] Dependencies for compiling agda, principal question

[David Wahlstedt]

Hi,

A while ago Agda became accessible to  much wider group of people than
before, thanks to the cabal support. This is really great !

However, I recently wanted to try the darcs version. It turned out that the
version of the Haskell platform that is now widely available, with ghc 6.10,
and cabal 1.6 is not enough to install the darcs version of Agda. Right now
I can't afford the time needed to install it. I don't want to go into
details about why I failed. Since the issue concerns the darcs version,
somehow I accept things as they are.
(in fact it failed even when I checked out with the tag 2.2.6, it still
required cabal 1.8, that ghc 6.10 didn't accept)

Anyway ... I want to raise a principal question:

Why should a system for dependent type theory depend on the very latest
version of the Haskell tools, especially, why should it depend on the very
latest cabal in order to be buildable ? Is it really needed ?
I can understand that the UTF-8 support requires some newer versions of
tools, and probably there are other internals that I am not aware of that
motivates these dependencies, but there must be a reasonable trade-off.

This tendency to introduce dependencies to the very latest Haskell stuff
makes the installation too difficult and time consuming for many people,
even proficient type theorists and programmers. It is a pity, since agda is
such an nice system.

I would be very grateful if one could take a principal conservative
decision---that the code should always be buildable with the widely
available version of the Haskell platform (which is now still 6.10). By such
a decision Agda would win a lot of users, I'm sure.
What negative effects would such a decision have ?


Best regards,

 David Wahlstedt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100420/dac48698/attachment.html