[Agda] Dependencies for compiling agda, principal question

Martin Escardo m.escardo at cs.bham.ac.uk
Tue Apr 20 12:05:39 CEST 2010


I also tried cabal a while ago and gave up for reasons given below. (I 
run a probably very old version from an ubuntu repository.) Martin

James McKinna wrote:
> 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 ?
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list