[Agda] Dependencies for compiling agda, principal question

[Darin Morrison]

On 20 Apr 2010, at 10:26, David Wahlstedt wrote:

> 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.

The darcs version of Agda is meant to be the bleeding edge development version.  As far as I am aware, there are no guarantees that it should even compile, let alone work with older dependencies.

This isn't any different from other project with an open development repository.  In my opinion, if you cannot or are unwilling to put in the extra time and effort that will probably be necessary to use development quality code, you should instead use the non-darcs released version.

> 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 ?

The Cabal support for Agda that I have been working on essentially requires the latest version.

> 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.

The current release version works fine for this.

> What negative effects would such a decision have ?

I don't see why Agda developers should worry about backwards compatibility (as far as build dependencies are concerned) with versions of Agda that have not yet been released.  This prevents them from using what may be the best tools available to them at the moment.  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.

Is there a particular reason you needed the darcs version over the release version?

Cheers,
Darin