Don't set a default maximum heapsize for Agda runs

[andreasabel]

Don't set a default maximum heapsize for Agda runs

[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.

[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:

• graded-type-theory/graded-type-theory#23

[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)