[Agda] JS compiler - normalization

[Станислав Черничкин]

Howdy, humans!

I'm trying to solve following issue:
http://code.google.com/p/agda/issues/detail?id=684. Short story: Agda
runs out of 1 GB when attempting to compile standard library with JS
compiler. I'm using head revision (version 2.3.1 so far) from the
darcs repository. The problem occurred while compiling
Data.Bool.Properties module, several other modules can be compiled
normally. MAlonzo compiler is able to compile whole library with
relatively low memory footprint (less than 200 MB), I faced problem
with JS compiler, I have not tried Epic.

I investigated problem a bit and found, that bad things happening then
JS compiler tries to normalize term
Data.Bool.Properties.XorRingSolver._.⟦_⟧↓ (Compiler.hs:239). The
normalization does not seems to terminate or, at least, takes enormous
amount of memory (more than 1GB). I'm new to Agda, so I appreciate any
help/link from more experienced colleagues in solving this issue and
answering my questions:

1. What JS compiler uses normalization for? Why MAlonzo does not call
normalise function?
2. Does normalization guaranteed to terminate? Can it produce enormous
structure from relatively short input? Is
Data.Bool.Properties.XorRingSolver such case and how it can be
diagnosed?
3. Has someone tried to compile standard library with JS compiler
and/or faced similar issue?

Thanks.