[Agda] type check cost for `open'

[Wolfram Kahl]

On Wed, Aug 19, 2015 at 01:32:46PM +0300, mechvel at scico.botik.ru wrote:
> My current problem is that the project type checking cannot fit into
> 16 Gb.
> [...]
> The last (small) file has only an  "import - open" prelude.
> It needs to define several data and functions, but this very prelude 
> cannot type-check, because RAM is full

Does that last file need (transitively) everything from every file it opens?
If it does not, split those things out of the dependency graph.
(I don't like that kind of splitting either, but sometimes it is necessary.)

(You can call Agda with
   --dependency-graph="DepGraph.dot" 
 and use ``dot'' from graphviz

     Homepage:            http://www.graphviz.org/
     Description:         Open Source Graph Visualization Software

to get a graph layout.
I don't know when Agda generates and writes that graph;
you probably need to do that on sucessful calls.)

(-A1G probably eats into the available heap, and it also leads to
 garbage collections being relatively rare --- try something smaller,
 e.g., -A128M or -A16M, and have -S so you can see how much heap is occupied
 after the last ``Skipping...''.)



Best regards,

Wolfram