[Agda] Re: A patch making Agda smaller and faster

[Makoto Takeyama]

Hi,

Sorry, I lied about "the maximal sharing", my code does no such thing
(the data about improvement is true).
I am trying to memoize the class method "value" for decoding, but so
far seeing little to no improvement.

Best Wishes,
Makoto

> On Wed, Mar 5, 2008 at 2:18 PM, Makoto Takeyama <makoto.takeyama at aist.go.jp>
> wrote:
> 
> > Hi Ulf and Nisse,
> >
> > This patch adds the module TypeChecking.SerialiseShare, a replacement
> > for TypeChecking.Serialise .  This one deserialises interface files to
> > Interface data with the maximal substructure sharing.
> >
> > When loading lib/Everything.agda from interface files with this version,
> >
> > - the loading becomes twice as fast (14 sec -> 7 sec)
> >
> > - the memory allocation as reported by ":set +s" reduces to about
> > one-fifth
> >  (3.1G -> 0.67G)
> >
> > - the max resident memory size shown by Windows task manager becomes less
> >  than half (839M -> 332M)
> >
> > The space-leak problem (ghci just gets bigger almost linearly when you
> > repeat loading) is still there, but the reduced memory usage alleviates
> > it.
> 
> 
> Wonderful. Thanks a lot.
> 
> / Ulf

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