[Agda] JS compiler - normalization

[Andreas Abel]

Hello Stanislav,

On you questions:

1. I do not know the JS compiler and I do not know why it normalizes. 
Normalization can be a bad idea, e.g., consider this Haskell program:

   mylist = [1..100000000000]

   main = do
     n <- parse first command line argument
     print (take n mylist)

Normalizing mylist would probably make the compiler run out of mem.

2. Normalization is guaranteed to terminate.  However, it might produce 
insanely large normal forms (see above and issue 415):

   http://code.google.com/p/agda/issues/detail?id=415

Maybe try to switch off normalization in the JS compiler and see what 
happens...

Cheers,
Andreas

On 30.08.12 2:43 PM, Станислав Черничкин wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/