Commit that blew the 3.5G heap limit

[andreasabel]

@nad Your commit 8a2889c caused CI to fail running out of heap (limited to 3.5G) then.
It seems that now we need 5G: 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)

Maybe it would have been good at that time to not ignore the CI failure but to try to find out the new heap limit. If it was drastically more, maybe there is some type-checking inefficiency in the new code.

The current limit in CI is 6G heap.

[nad]

Your commit 8a2889c caused CI to fail running out of heap (limited to 3.5G) then.

Are you sure that it was this commit, and not some other commit that was pushed at the same time?

Maybe it would have been good at that time to not ignore the CI failure but to try to find out the new heap limit.

I may have forgotten that we use CI for this repository. If the idea is that we should use CI, then it might make sense to only allow pull requests.

When I pushed some changes recently I verified that Everything.agda type-checked for almost every commit:

(set -e; for COMMIT in c85c9bd1 830281bf 975ee6b6 8a720349 3d155c3f acfe82ba d505b42e 04f9346a 9017baf9 a6153cd6 4078e3fd cd07c61b 4f997be3 5727948c; do git checkout $COMMIT && agda Everything.agda +RTS -M6G; done)

I think it would be nice if that was taken care of by some CI script.

[andreasabel]

I think it would be nice if that was taken care of by some CI script.

I think for PRs this could be done: Get the commits between the base branch and the current branch of the PR, and then iterate checkout-then-build for this list.
Of course, if there are too many, the timeout could kill the CI before it finished the list.

For a direct push to master, I do not know how to get the list of new commits...

[nad]

Perhaps one could use the following command:

(set -e; for COMMIT in $(git log --reverse --format=tformat:%h master..HEAD); do git checkout $COMMIT; agda Everything.agda +RTS -M6G; done)

Note that after this command has run the repository might not be on the branch that it was on before the command was started.

[nad]

Perhaps one could use the following command:

(set -e; for COMMIT in $(git log --reverse --format=tformat:%h master..HEAD); do git checkout $COMMIT; agda Everything.agda +RTS -M6G; done)

I think it would make sense to also use -Werror.