[Agda] Dependencies for compiling agda, principal question

James McKinna james.mckinna at cs.ru.nl
Tue Apr 20 11:56:27 CEST 2010


Seconded.

For my money (and more importantly: time) it would good to avoid the 
current ghc6.12/cabal installation mess affecting other software, such 
as agda.

The Coq people manage a no-holds-barred development version side-by-side 
with a conservative deployment version (though ocaml is a slightly less 
moving target than ghc). They are surely a much bigger team, but even 
so, I support the idea of a release version for "the rest of us".

James.

David Wahlstedt wrote:
> ... [problems with cabal] and ghc6.10/6.12
>
> 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 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 ?
>


More information about the Agda mailing list