[Agda] memory eagerness
mechvel at botik.ru
Tue May 7 09:39:48 CEST 2013
thank you for your notes.
To my letter of 2013-05-06
> On Mon, May 06, 2013 at 10:33:16PM +0400, Sergei Meshveliani wrote:
> > [...]
> > The longest one has about 250 lines of a proper source code.
> > And it needs more than 6 Gb memory to type check:
> > agda -c -i . -i $agdaStLib +RTS -K200m -M8000m -RTS Main.agda
> > (-M6000m is not enough).
> (How much memory does your machine have?
> If it has only 8G, don't do -M8000m!
> ``kill -STOP'' your firefox, and run
It has 16 Gb now! And I have given half of it.
But happiness is not in Gb-s!
As this example takes more than 6 Gb to type-check, further practical
examples will need much more than the machine has.
Various further option tricks with controlling memory will not help,
for the same reason
(-H looks good, in a certain sense).
On the other hand, 1 Gb is quite a lot of memory for any reasonable
Your experience with type-checking in 12 Gb confirms my impression
that something essential needs to be improved in the type checker
Because you have already applied various precautions against the space
eating, and still have 12 Gb -- an awful size.
> Agda typechecking performs a lot of evaluation/reduction,
> and the current reduction engine that is used for this
> does not implement the degree of sharing you might expect.
This is mentioned again. A naive user's wish to the developers:
please, do more sharing in the type checker!
> Sharing happens when interface files are written,
> but not while a single module is checked.
> For that reason, sometimes it makes sense to split a
> two-definition module into two one-definition modules...
I had modules of 600 proper lines; then I have split them voluntarily
(not by their sense!) to 300 lines each; this somewhat helped.
Now, I need to divide them once more ... A suspicious activity.
> > 1. Record vs ordinary module
> > ------------------------------
> > For example, the record Group
> > has a parameter : UpMonoid c l
> > and a single field totalInversion : ...
> > There are also several related auxiliary functions
> > (defined via the parameter and field totalInversion)
> > and their proved lemmata:
> > division, proof for inv (x * y) == (inv y) * (inv x),
> > for inv (inv x) == x, and such.
> > And I put all them into this very record, so that it exports them
> > (because a record is also a module).
> > Their code size is about 20 times larger than the proper Group
> > record part. And it can grow further several times, because
> > there are many useful lemmata about groups.
> > I think, so far, that this is a natural style. Is it?
> I consider this natural, too, and followed this style for a long time.
> But recently I had to remove large chunks of such code into separate modules
> to get my developments typechecked (in 12G...).
> > Another design may be:
> > to create
> > module Group-related (G : Group ...)
> > where
> > ...
> > and move there the above Group related items, so that the proper
> > Group record will become a small code.
> > Will this approach save much space in the type-check?
> It did in my case.
> I also have what in your case is ``Group-related'' in a separate file,
> and actually have multiple such modules for different topics.
My case is a bit more complicated:
module GroupPack (upM : UpMonoid c l)
<prelude using upM>
record Group : Set _
where -- it uses <prelude>
field totalInversion : ...
<lemmata for Group> -- uses <prelude>, <prelude-2>,
-- a parametrized module with a large record Group inside.
Now, I need to move a large part of <lemmata> to a separate file ...
Well, may be this is not difficult.
But look: you did all these tricks -- and still have 12 Gb in the type
check! 12 Gb is a very un-natural size for this.
I shall see further. Thanks again,
More information about the Agda