[Agda] Re: Avoid GHC 6.10.1 (for now)

[Makoto Takeyama]

> But, binary-0.4.4 (and hence bytestring-0.9.1.4) 
Oops, sorry, this "and hence" was my mistake; I'll try binary-0.4.4 +
GHC-6.8.3 again.

Makoto


On Thu, 13 Nov 2008 21:44:31 +0900
Makoto Takeyama <makoto.takeyama at aist.go.jp> wrote:

> Hi Nisse,
> 
> > This has now been fixed by a new version of binary.
> 
> On Windows, binary-0.4.4 + GHC-6.10.1 does not seem to solve the
> problem (It is unsuable with the memory usage going through the roof)
> 
> > I should perhaps add that the most recent version of Agda is now
> > configured to only accept new versions of binary, so there is no risk of
> > using the slow version by accident.
> 
> But, binary-0.4.4 (and hence bytestring-0.9.1.4) + GHC-6.8.3 does not
> seem to compile because some precompiled library code expects
> bytestring-0.9.0.1.1, it seems.
> 
> This means I cannot prepare an usable and updatable windows
> distribution with the latest Agda.cabal.  Will you reconsider the
> restriction binary >= 0.4.4 in Agda.cabal?
> 
> Best Wishes,
> Makoto
> 
> (Are there any windows user who can typecheck / reload Everything.agda
> with GHC-6.10.1 in any way?)
> 
> 
> On Tue, 11 Nov 2008 15:45:59 +0000
> Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> 
> > On 07/11/08 16:20, Nils Anders Danielsson wrote:
> > > 
> > > If you compile Agda using GHC 6.10.1, then you can expect drastic
> > > slowdowns (as compared to GHC 6.8.3). Loading the standard library, when
> > > everything is already type-checked, can take roughly ten times longer if
> > > you use 6.10.1.
> > > 
> > > I don't know the reason for this slowdown, but my hunch is that there is
> > > some optimisation of the binary library which is not triggered properly
> > > by the new compiler. Perhaps this will be fixed by a future version of
> > > binary.
> > 
> > This has now been fixed by a new version of binary.
> > 
> > -- 
> > /NAD
> > 
> > This message has been checked for viruses but the contents of an attachment
> > may still contain software viruses, which could damage your computer system:
> > you are advised to perform your own checks. Email communications with the
> > University of Nottingham may be monitored as permitted by UK legislation.
> > 
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
> -- 
> Makoto Takeyama <makoto.takeyama at aist.go.jp>
> AIST/CVS (National Institute of Advanced Industrial Science and Technology /
>           Research Center for Verification and Semantics)
> tel: +81-6-4863-5019   fax: +81-6-4863-5052
> 
> 
> 

-- 
Makoto Takeyama <makoto.takeyama at aist.go.jp>
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052