[Agda] type check cost for `open'

[mechvel at scico.botik.ru]

Thank you.
I command  "agda ..." in the command line,
and also command `top' on another terminal, and it shows who takes 
memory/processor and how much of them.

My current problem is that the project type checking cannot fit into
16 Gb.
The code is on
http://www.botik.ru/pub/local/Mechveliani/agdaNotes/bugRep-aug18-2015.zip

It has  README.agda,
also I have put it to the bug tracker.

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
(total 16Gb, options:  -M13200m -H13200m -AG1,
increasing heap leads to swapping).
So that module splitting will not help here.

Regards,

------
Sergei


Wolfram Kahl писал 18.08.2015 19:20:
> On Mon, Aug 17, 2015 at 06:09:38PM +0300, Sergei Meshveliani wrote:
>> Now I look more attentively at the `top' output on memory, and see 12
>> Gb.
> 
> Just a quick note: I find htop
> 
>      Homepage:            http://hisham.hm/htop/
>      Description:         interactive process viewer
> 
> (possible available as a package from your distribution)
> indispensible for watching Agda, especially when I work
> interactively, since Emacs has insufficient information
> on whether the Agda process is active or not.
> 
>   F6 ``sort by'' --> MEM
> 
> makes sure that, most of the time, your Agda process is
> at the top of the listing...
> 
> 
> Wolfram