Maximum heap size reached on `category-theory.codensity-monads-on-precategories`

[fredrik-bakke]

Recently it's been observed that the typecheck workflow fails due to reaching its designated max heap size. For instance:

 Checking category-theory.codensity-monads-on-precategories (/home/runner/work/agda-unimath/agda-unimath/repo/src/category-theory/codensity-monads-on-precategories.lagda.md).
agda: Heap exhausted;
agda: Current maximum heap size is 6442450944 bytes (6144 MB).
agda: Use `+RTS -M<size>' to increase it.
Command exited with non-zero status 251
672.64user 10.67system 11:21.95elapsed 100%CPU (0avgtext+0avgdata 4461348maxresident)k
0inputs+513496outputs (0major+3169569minor)pagefaults 0swaps
make: *** [Makefile:100: check] Error 251

https://github.com/UniMath/agda-unimath/actions/runs/18375493839/job/52348377771?pr=1560#step:5:2380

Every time it happens while checking category-theory.codensity-monads-on-precategories, so this seems to be the culprit of the error. I profiled the file locally:

frebak@Fredriks-MacBook-Pro agda-unimath % make profile-module MODULE=category-theory.codensity-monads-on-precategories
Attempting to delete interface file for category-theory.codensity-monads-on-precategories
Profiling typechecking of category-theory.codensity-monads-on-precategories
Checking category-theory.codensity-monads-on-precategories (/Users/frebak/Repositories/agda-unimath/src/category-theory/codensity-monads-on-precategories.lagda.md).
Total                                                                                                         9,118ms 
Miscellaneous                                                                                                 3,825ms 
category-theory.codensity-monads-on-precategories._.precomp-right-unit-law-mul-codensity-monad-Precategory    2,773ms 
category-theory.codensity-monads-on-precategories._.right-precomp-associative-mul-codensity-monad-Precategory   655ms 
category-theory.codensity-monads-on-precategories._.precomp-left-unit-law-mul-codensity-monad-Precategory       574ms 
category-theory.codensity-monads-on-precategories._.associative-mul-codensity-monad-Precategory                 421ms 
category-theory.codensity-monads-on-precategories._.left-precomp-associative-mul-codensity-monad-Precategory    359ms 
category-theory.codensity-monads-on-precategories._.right-unit-law-mul-codensity-monad-Precategory              234ms 
category-theory.codensity-monads-on-precategories._.left-unit-law-mul-codensity-monad-Precategory               119ms 
category-theory.codensity-monads-on-precategories._.compute-mul-codensity-monad-Precategory                      64ms 
category-theory.codensity-monads-on-precategories._.compute-unit-codensity-monad-Precategory                     54ms 
category-theory.codensity-monads-on-precategories._.mul-codensity-monad-Precategory                              14ms 
category-theory.codensity-monads-on-precategories._.unit-codensity-monad-Precategory                             10ms 
category-theory.codensity-monads-on-precategories._.codensity-monad-Precategory                                  10ms 
  32,456,399,064 bytes allocated in the heap
   1,766,639,824 bytes copied during GC
     563,354,808 bytes maximum residency (9 sample(s))
       1,086,280 bytes maximum slop
            2297 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0        93 colls,     0 par    1.217s   1.599s     0.0172s    0.2898s
  Gen  1         9 colls,     0 par    0.366s   0.515s     0.0572s    0.2544s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.003s  (  0.004s elapsed)
  MUT     time    7.543s  (  7.554s elapsed)
  GC      time    1.583s  (  2.114s elapsed)
  EXIT    time    0.006s  (  0.002s elapsed)
  Total   time    9.134s  (  9.674s elapsed)

  Alloc rate    4,302,906,675 bytes per MUT second

  Productivity  82.6% of total user, 78.1% of total elapsed

[fredrik-bakke]

Here's the profiling with --profile=internal:

Checking category-theory.codensity-monads-on-precategories (/Users/frebak/Repositories/agda-unimath/src/category-theory/codensity-monads-on-precategories.lagda.md).
Total                      9,227ms          
Miscellaneous                  4ms          
Typing                       304ms (5,403ms)
Typing.CheckRHS            4,479ms          
Typing.OccursCheck           490ms          
Typing.TypeSig               128ms          
Deserialization              887ms (1,472ms)
Deserialization.Compaction   585ms          
Serialization                957ms   (966ms)
Positivity                   829ms          
Parsing                      152ms   (185ms)
Parsing.OperatorsExpr         32ms          
InterfaceInstantiateFull     123ms          
Termination                    0ms    (82ms)
Termination.RecCheck          82ms          
DeadCode                       0ms    (56ms)
DeadCode.DeadCodeReachable    55ms          
Coverage                      55ms          
Import                        39ms          
Scoping                        6ms    (12ms)
Highlighting                  11ms

[fredrik-bakke]

After inserting the answer into a bunch of the _'s it's now down to

Checking category-theory.codensity-monads-on-precategories (/Users/frebak/Repositories/agda-unimath/src/category-theory/codensity-monads-on-precategories.lagda.md).
Total                      4,969ms          
Miscellaneous                  5ms          
Typing                       183ms (2,544ms)
Typing.CheckRHS            1,874ms          
Typing.OccursCheck           356ms          
Typing.TypeSig               128ms          
Deserialization              919ms (1,551ms)
Deserialization.Compaction   631ms          
Serialization                280ms   (288ms)
Parsing                      202ms   (237ms)
Parsing.OperatorsExpr         34ms          
Positivity                   171ms          
Import                        39ms          
InterfaceInstantiateFull      38ms          
Termination                    0ms    (33ms)
Termination.RecCheck          33ms          
Coverage                      24ms          
DeadCode                       0ms    (22ms)
DeadCode.DeadCodeReachable    22ms          
Highlighting                  14ms          
Scoping                        6ms    (13ms)
  15,538,926,024 bytes allocated in the heap
     594,582,600 bytes copied during GC
     384,269,352 bytes maximum residency (8 sample(s))
         660,440 bytes maximum slop
            2125 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0        83 colls,     0 par    0.388s   0.678s     0.0082s    0.2579s
  Gen  1         8 colls,     0 par    0.222s   0.245s     0.0307s    0.1910s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.002s elapsed)
  MUT     time    4.379s  (  4.546s elapsed)
  GC      time    0.610s  (  0.924s elapsed)
  EXIT    time    0.003s  (  0.003s elapsed)
  Total   time    4.994s  (  5.475s elapsed)

  Alloc rate    3,548,237,911 bytes per MUT second

  Productivity  87.7% of total user, 83.0% of total elapsed

so that had a considerable impact both on speed and memory usage.

[lowasser]

#1341 seems to be hitting this too.

[fredrik-bakke]

This should be "patched" by #1578. I'll merge that soon

[fredrik-bakke]

The problem pointed to by this issue does not seem to be resolved 😩
https://github.com/UniMath/agda-unimath/actions/runs/18506984412/job/52738222407?pr=1580#step:5:1550

[fredrik-bakke]

This issue still hits
https://github.com/UniMath/agda-unimath/actions/runs/18510312303/job/52752206006?pr=1571#step:5:2027
reopening