memory limit is hit about agda-categories HOT 14 CLOSED

removing memory upper bound seems to allow Agda to swallow 13.6G of memory from a clean build.

from agda-categories.

note that this issue occur when attempting to make the library from scratch. continue making won't fail again.

from agda-categories.

detailed stats:

 467,499,321,488 bytes allocated in the heap
  43,000,081,592 bytes copied during GC
   4,883,174,248 bytes maximum residency (11 sample(s))
      14,761,112 bytes maximum slop
           13920 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       797 colls,     0 par   29.152s  29.261s     0.0367s    0.8225s
  Gen  1        11 colls,     0 par   15.386s  16.877s     1.5343s    4.8577s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time  195.514s  (196.902s elapsed)
  GC      time   44.538s  ( 46.138s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time  240.053s  (243.041s elapsed)

  %GC     time      18.6%  (19.0% elapsed)

  Alloc rate    2,391,130,159 bytes per MUT second

  Productivity  81.4% of total user, 81.0% of total elapsed

from agda-categories.

Did the library this is a rewrite of need the same amount of memory to typecheck?
If not, what has changed?

from agda-categories.

the original library takes 0 memory cuz it no longer compiles.

other than a few other things, this library has grown bigger. another thing is that the previous library was mainly a package of definitions, but there are a lot more proofs in this one.

from agda-categories.

I managed to compile it in 6G on my 8G Mac. If it starts to need more, that's going to be a problem -- once Agda start to swap, it's hopeless for it to finish.

from agda-categories.

If this makes it into the standard library (which I think it probably should!) then its current size is going to be a problem. The standard library is ~2G which combined with this 6G is going to push it over 8G...

from agda-categories.

I was always thinking that agda-categories should be migrated to stdlib in pieces. First, everything needed to define Category, Functor and NaturalTransformation would go in. Then, I'm not quite sure what chunks to do next (we could certainly ask).

In any case, I do think this provides a nice test case for the Agda devs to figure out why Agda consumes so many resources here. Not quite sure how to start that process though -- posting an issue on agda/agda?

from agda-categories.

I tried to compile this the other day and it took 18GB of memory which seems a bit silly. I had to make a bigger swap partition just to get it to not crash

from agda-categories.

I can compile on my laptop with 8GB of memory, with things capped at 6GB. So I'm surprised that yours goes quite so high. What version of Agda are you using?

But I agree: the amount of memory taken to compile this library is too high. We just don't know how to debug this problem. Certainly it does seem to be inside the equational proofs of some of the more advanced categorical results (so that's a good sign, for whatever that's worth). The terms involved are very large, once you add all the implicits, though the amount of sharing is also huge, so that in a proper representation the terms are of quite reasonable size.

from agda-categories.

agda 2.6.0.1 I think and stdlib 1.1 . The problem may be that I'm using nix to build it and it does something weird but I think it just runs agda on the everything file. It crashed on my laptop with 8gb ram + 8gb swap

from agda-categories.

Monoidal.Properties and Pseudo functors were troublesome from what I remember

from agda-categories.

yeah I believe Monoidal.Closed.IsClosed is also a slow one, as well as Bicategory.Instance.Cats. I suppose it has something to do with the aggressive eta expansion of Agda.

from agda-categories.

This issue is mostly obsolete - the changes in 2.6.1 have fixed quite a few memory issues, and then I also split things so as to reduce pressure. So I'm going to close this one as no longer relevant. Please feel free to reopen with new data that shows that things are still bad, or a new issue.

from agda-categories.