[Agda] type check performance

[Wolfram Kahl]

On Tue, Mar 31, 2015 at 05:32:41PM +0200, Nils Anders Danielsson wrote:
> On 2015-03-31 17:15, Andrea Vezzosi wrote:
> >>While the compiler is running Agda should only touch a small amount of
> >>memory (unless the compiler prints lots of stuff to stdout/stderr), so I
> >>would hope that the rest of the memory should be paged out, if
> >>necessary.
> >
> >Can we hope that in a garbage collected language like Haskell?
> 
> Perhaps that is too much to hope for, unless the run-time system
> actively makes it easy to swap out older generations.

Originally I had hoped that, too, but I arrived at my current method
through observing serious contention between Agda -H8G -M8G
and GHC -H7G -M7G (or similar numbers) on a 16G machine.
Dropping -H might help (hoping (again) that most Agda heap is garbage
by that time, and the RTS returns the memory to the OS after GC),
but omitting -H or setting it lower than -M also tends to be quite costly.
(Perhaps that can be offset using -A, but right now I am sufficiently happy
 with my procedure and sufficiently busy with other things...)


Wolfram