[Agda] about serialization

[Wolfram Kahl]

On Fri, Mar 31, 2017 at 11:41:37PM +0300, Sergei Meshveliani wrote:
> My real example is of the scheme
> 
> [...]
> So that  M2  does almost nothing.
> 
> Only in the real example  M11  has certain complex definitions inside
> it, with  p : CommutativeMonoid  (represented by a dependent record).
> But real  M2  has nothing besides importing  p  from a certain
> parametric module and declaring  
>            module M11-p = M11 p.
> 
> In the above example I replace this with the line
> 
>    module M11-2 = M11 2. 
> 
> And type-checking of the real  M2.agda  takes 75 sec on a 3 GHz machine,
> and needs more than 3 Gb heap.

Have you tried this with Andrea Vezzosi's patch from
https://github.com/agda/agda/issues/1625#issuecomment-132196576
?



Wolfram