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

Makoto Takeyama makoto.takeyama at aist.go.jp
Thu Nov 13 13:44:31 CET 2008


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





More information about the Agda mailing list