[Agda] Re: Issue 1041 in agda: `Maybe' causes a great type-check cost

[Sergei Meshveliani]

On Thu, 2014-02-06 at 05:28 +0000, agda at googlecode.com wrote:
> Comment #27 on issue 1041 by k... at cas.mcmaster.ca: `Maybe'  causes a great  
> type-check cost
> http://code.google.com/p/agda/issues/detail?id=1041
> 
> (I am apparently bitten by different issues: The  
> Categoric.MonCoAlg.SEAG.Cat2.FromTo I mentioned above, and which I  
> previously have seen typechecked in 13.5GB heap, still does not check in  
> 11GB. (I haven't tried more heap with the new Agda version.) )
> 

Му current project is complex enough: 
* 15 modules, about 5000 essential lines, 
* modules are not small, some of them have about 400 essential lines, 
* `with' is set almost everywhere instead of `case' (except in 
  Main.agda),
* records nested to 25-30 levels, and export many lemmata implementation
  besides `field'-s.

And despite all this  Agda of  February 5  type-checks it fast spending
1.5 Gb space. 

I do not know of whether this is by a lucky occasion. 
 
Now, Wolfram's project takes more than 10 Gb to type-check.
Suppose that it is also fixed, may be, by also fixing Agda further.

If (and after) this happens, it will be desirable for me to know of this
event, in order to test new Agda.

Regards,

------
Sergei