Description
A bit more than 4 years ago it was decided to set the maximum heap size for Agda to 3.5G:
Line 864 in a9c1763
A CI run fails for me where this limit is reached: https://github.com/graded-type-theory/graded-type-theory/actions/runs/7666738532/job/20895151382
I was in vain searching workflow- and make-files to look for a setting of the maximum heap size, only to remember that I had seen something in Agda.cabal...
From a UX perspective, I find it odd that we ship Agda with a default max heapsize.
Issue #3759 talks in the OP about a custom error should the heap be exhausted:
Setting a maximum heap size can mean that Agda runs faster and needs less memory. However, it can also mean that Agda crashes when it otherwise wouldn't. Thus, if we change the default maximum heap size, then it might be a good idea to make Agda print a customised error message, informing the user of how to increase the maximum heap size, when the program runs out of heap (by catching the HeapOverflow exception; perhaps it makes sense to tweak the -Mgrace RTS option).
Such a nice error has never been implemented, so I suppose from a UX perspective we should also not set a max heap size by default.
ATTN (original contributors): @nad @WolframKahl @jespercockx @UlfNorell