Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Try splitting up What4.Expr.Builder to improve compile times #220

Open
RyanGlScott opened this issue Oct 14, 2022 · 0 comments
Open

Try splitting up What4.Expr.Builder to improve compile times #220

RyanGlScott opened this issue Oct 14, 2022 · 0 comments
Labels
enhancement New feature or request performance Issues related to compile-time or runtime performance

Comments

@RyanGlScott
Copy link
Contributor

what4's compile times are rather slow, and especially so on GHC 9.0 and earlier. On our CI, GHC 9.0 takes about 13 minutes to build, most of it coming from the What4.Expr.Builder module. The story is even more dire for non-x86 architectures. On Debian's build servers, for instance, building what4 times out on the armhf architecture after compiling What4.Expr.Builder for 150 minutes straight (see here). That is so egregiously slow that I cannot help but wonder if there is some other GHC issue at play, but the point remains: What4.Expr.Builder is uncomfortably slow to build.

One idea for improving the compile times is to split up What4.Expr.Builder module into several smaller modules. While this is not guaranteed to improve compile times, my experiences with GHC suggest that this usually provides a modest boost. If nothing else, it would force us to reconsider if we really need to put as much stuff into What4.Expr.Builder as it currently contains.

It is worth noting that the story is far improved on GHC 9.2, which features a much more efficient pattern-match coverage checker. On GHC 9.2, what4 takes about 3 minutes to build, which is about 10 minutes faster than previous versions of GHC. Indeed, most of What4.Expr.Builder consists of this one instance, which pushes the pattern exhaustiveness checker to its absolute limits. Nevertheless, it still takes 3 minutes to build—perhaps we can still do better.

@RyanGlScott RyanGlScott added enhancement New feature or request performance Issues related to compile-time or runtime performance labels Oct 14, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request performance Issues related to compile-time or runtime performance
Projects
None yet
Development

No branches or pull requests

1 participant