Closed sstucki closed 3 years ago
This is an attempt to "fix" the CI script so PR https://github.com/agda/agda-categories/issues/304#issuecomment-904488072 passes the build. From the PR discussion:
I noticed we don't use --auto-inline in the Makefile (or the CI script). Apparently this was a default option prior to 2.6.2 and can help speed up type checking. Maybe it helps with heap usage too?
--auto-inline
See https://github.com/agda/agda/blob/v2.6.2/CHANGELOG.md#pragmas-and-options
Originally posted by @sstucki in https://github.com/agda/agda-categories/issues/304#issuecomment-904488072
This is an attempt to "fix" the CI script so PR https://github.com/agda/agda-categories/issues/304#issuecomment-904488072 passes the build. From the PR discussion:
I noticed we don't use
--auto-inline
in the Makefile (or the CI script). Apparently this was a default option prior to 2.6.2 and can help speed up type checking. Maybe it helps with heap usage too?See https://github.com/agda/agda/blob/v2.6.2/CHANGELOG.md#pragmas-and-options
Originally posted by @sstucki in https://github.com/agda/agda-categories/issues/304#issuecomment-904488072