Hi,<br><br>A while ago Agda became accessible to much wider group of people than before, thanks to the cabal support. This is really great !<br><br>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.<br>
(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)<br><br>Anyway ... I want to raise a principal question:<br><br>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 ? <br>
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.<br>
<br>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.<br>
<br>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.<br>
What negative effects would such a decision have ?<br><br><br>Best regards,<br><br> David Wahlstedt<br><br>