Investigate memory usage when typechecking the whole library
VojtechStep opened this issue · 2 comments
The CI workflows started running out of memory at the end of typechecking the library (the last line of the logs is that it's checking everything.lagda.md).
Examples of failed jobs:
- MacOS: https://github.com/UniMath/agda-unimath/actions/runs/7232860795/job/19707495899
- Ubuntu: https://github.com/UniMath/agda-unimath/actions/runs/7186165597/job/19570972093
The runners themselves should have enough memory (7 GB for Ubuntu and 14 GB for MacOS according to the docs), so for now we probably can bump Agda's internal memory limit, but it'd still be best to investigate why we need 4 GB of RAM to typecheck the library.
Agda does have some functionality for measuring the type-checking performance of a formalization. It would be nice regardless to log this on the master branch, although perhaps the runners aren't designed for performance testing.
This is not an issue we have much power over. After #1031 we at least record memory usage over time. But in the end, we are subject to the limitations of what Agda can and can't handle.