Don't set a default maximum heapsize for Agda runs

[andreasabel]

A bit more than 4 years ago it was decided to set the maximum heap size for Agda to 3.5G:

agda/Agda.cabal

Line 864 in a9c1763

"-with-rtsopts=-M3.5G -I0"

• Change the default RTS options? #3759

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

[UlfNorell]

I'm in favour of removing the default limit.

I think the argument was that people who need more than 3.5G for Agda are savvy enough to set their own RTS options, but I'm not sure I believe that setting the maximum heap size will make things faster... do we have an example that shows this?

[ncfavier]

A CI run fails for me where this limit is reached

The plot thickens: this is the fourth project I've heard of that has recently (roughly since 2.6.4.1, although I could not establish a direct correlation with the update) started exceeding the maximum heap size. I mentioned this here before.

Is this still a coincidence, or has something changed recently that made Agda more memory-hungry?

[andreasabel]

@ncfavier wrote:

Is this still a coincidence, or has something changed recently that made Agda more memory-hungry?

Good question! One could do a matrix-build (2.6.4 vs. 2.6.4.1; different heap limits) to find out if it is a regression in 2.6.4.1.
What setup-agda concerns, it seems to build 2.6.4.1 with GHC 9.4.7 but 2.6.4 with GHC 9.6.3:
https://github.com/wenkokke/setup-agda/blob/8b21b460abb9f58abe2d884ff4db188916540f7e/data/Agda.versions.yml#L35-L37
https://github.com/wenkokke/setup-agda/blob/8b21b460abb9f58abe2d884ff4db188916540f7e/data/Agda.versions.yml#L69-L71

[andreasabel]

For the project in question, there seems no obvious difference between 2.6.4 and 2.6.4.1: https://github.com/graded-type-theory/graded-type-theory/actions/runs/7708057745

$ gh run view 7708057745  

JOBS
X build (2.6.4, 3.5G) in 40m20s (ID 21006382426)
X build (2.6.4, 4G) in 39m39s (ID 21006382755)
X build (2.6.4, 4.5G) in 39m56s (ID 21006382982)
✓ build (2.6.4, 5G) in 40m42s (ID 21006383267)
X build (2.6.4.1, 3.5G) in 38m52s (ID 21006383561)
X build (2.6.4.1, 4G) in 38m2s (ID 21006383812)
X build (2.6.4.1, 4.5G) in 37m18s (ID 21006384072)
✓ build (2.6.4.1, 5G) in 39m23s (ID 21006384300)

2.6.4.1 is slightly faster (3%) than 2.6.4, but both either succeed or run out of memory in about 40 minutes.

It seems like the heap increase was rather triggered by adding more code to the project:

• Commit that blew the 3.5G heap limit graded-type-theory/graded-type-theory#23

[andreasabel]

I experimented with different max heap sizes but they do not seem to make any impact (that has any significance) on the total running time for the SUT.
https://github.com/graded-type-theory/graded-type-theory/actions/runs/7709851320

$ gh run view  7709851320

JOBS
✓ build (2.6.4.1, 5G) in 39m22s (ID 21011895130)
✓ build (2.6.4.1, 6G) in 38m46s (ID 21011895413)
✓ build (2.6.4.1, 8G) in 39m9s (ID 21011895714)
✓ build (2.6.4.1, 10G) in 38m17s (ID 21011896018)

So I guess the conclusion is to remove the max heap pre-setting for Agda.

[nad]

I experimented with different max heap sizes but they do not seem to make any impact (that has any significance) on the total running time for the SUT.

Did you also try to omit the -M flag? I seem to recall that just having a maximum heap size could make a difference, but that was a few years ago, perhaps this has changed.

[andreasabel]

Started a test at: https://github.com/graded-type-theory/graded-type-theory/actions/runs/7742297113

Update: Blunder, if I do not set a limit there then the default limit -M3.5G of Agda will apply, of course...

[andreasabel]

I now ran a test with Agda nightly which doesn't have the default -M setting anymore, and there is no difference between not setting -M and setting a sufficient -M: https://github.com/graded-type-theory/graded-type-theory/actions/runs/7743167201/job/21113959483
(The runs are ~55min instead of ~40min with 2.6.4.1, so maybe the nightly builds are less optimised...)

✓ ci-matrix Matrix · 7743167201
Triggered via push about 1 hour ago

JOBS
✓ build (nightly) in 56m7s (ID 21113959483)
✓ build (nightly, -M5G) in 57m20s (ID 21113959816)
✓ build (nightly, -M6G) in 57m49s (ID 21113960149)