[Agda] Agda interface generation memory consumption

[kahl at cas.mcmaster.ca]

On Tue, 16 Feb 2010, 10:58, nad at Cs.Nott.AC.UK wrote:

 >  Perhaps we will try to optimise Agda further in the upcoming
 > Agda meeting

(Which unfortunately is shortly before our end of term (8 April),
 and in addition has significant overlap with ETAPS...)

Anyway, where does this crazy space usage come from?

I have no good understanding what exactly Agda is doing for type checking,
but just from the time and space behaviour, I have the gut feeling
that there might be a lot of sharing missing,
and in particular observable sharing.

Caclulational reasoning seems to be particularly costly,
and I am doing it in setoids or posets for which the definition
can be expanded quite a lot --- and I have the impression that it might be
expanded again and again, just to check whether the expansions are equal.
But if it is inside a calculational reasoning chain,
then that structure will be referred to by a single name,
and if that sharing is not broken, then the equality check is
essentially free.

Does the problem lie in this direction?


Wolfram


P.S.:  In the meantime I have hacked my GHC's RTS option parsing,
       and managed to start the type checking of
       Data.Algebra.Generalised.BisimConvCommutes with 2.7G of heap ---
       still runs out of heap.
       Right now it is running on 2.9G, and grinding at full heap:

 20553712  16428060 2857608220  0.16  0.16 2101.78 2140.33    0    0  (Gen:  0)
   524288   2319076 2857832000  0.02  0.02 2101.80 2140.35    0    0  (Gen:  0)
   524260    313184 2768035168 59.81 61.29 2161.62 2201.64    0    0  (Gen:  1)
 22974464   9960820 2777840476  0.13  0.13 2161.85 2201.88    0    0  (Gen:  0)
 76906484  38569924 2810625412  0.46  0.49 2162.66 2202.75    0    0  (Gen:  0)
 42545152  37216732 2828756648  0.38  0.41 2163.24 2203.37    0    0  (Gen:  0)
 27766768  24378404 2840592736  0.25  0.27 2163.62 2203.78    0    0  (Gen:  0)
 23777272  18327656 2850729412  0.20  0.21 2163.93 2204.10    0    0  (Gen:  0)
 21884924  13336764 2860057136  0.14  0.16 2164.17 2204.37    0    0  (Gen:  0)
   524284   6674808 2860280764  0.06  0.06 2164.24 2204.43    0    0  (Gen:  0)
   524248    316396 2803102808 68.81 69.85 2233.05 2274.28    0    0  (Gen:  1)
  6516716   2938668 2805887148  0.04  0.04 2233.12 2274.35    0    0  (Gen:  0)
 60092412  26139000 2831505912  0.33  0.33 2233.71 2274.96    0    0  (Gen:  0)
 42467328  19368284 2849616428  0.24  0.24 2234.14 2275.39    0    0  (Gen:  0)
 25620452  17354800 2860537324  0.19  0.19 2234.45 2275.70    0    0  (Gen:  0)
   524284   7779000 2860760468  0.07  0.07 2234.52 2275.77    0    0  (Gen:  0)
   524284    315016 2825053904 69.75 70.76 2304.27 2346.54    0    0  (Gen:  1)
  4276184   1986472 2826883332  0.02  0.02 2304.32 2346.58    0    0  (Gen:  0)
 45400044  19688536 2846245856  0.25  0.25 2304.77 2347.04    0    0  (Gen:  0)
 30339056  16746880 2859174492  0.19  0.19 2305.10 2347.37    0    0  (Gen:  0)
   524272   9164700 2859399488  0.08  0.08 2305.18 2347.45    0    0  (Gen:  0)


       Without -M, it runs out of memory at roughly these heap sizes,
       so I move in small steps.