New compiler has been enabled

Stream: lean4

[Cameron Zwarich]

As of 7f8ccd8, the new compiler has been enabled on master. This is a major step forward for Lean. The new compiler has been in the works for several years, and I have spent almost all of my time at the FRO this year finishing it and readying it for production. While there are some nice results from this initial switch, the real benefits will be seen when the new compiler is used as the foundation for future improvements, as we aim to increase the kinds of programs that can reasonably be written (and verified) in Lean.

In the coming weeks, I'll be going over the GitHub issues with the fixed-by-new-code-generator and depends-on-new-code-generator labels. While I haven't looked at all of them, many of the latter should be relatively easy fixes now. In general, you should expect more rapid responses to issues reported in the compiler going forward.

If you see any regressions, please CC me on GitHub issues or any threads here on Zulip. I will be on the lookout for anything, but the Lean community is thankfully now so large that it is unreasonable to expect to come across everything myself.

[Matthew Ballard]

@Cameron Zwarich Congratulations on the awesome accomplishment!

[Jovan Gerbscheid]

Do you have a speedcenter comparison to see what the impact on mathlib is? I'd be curious to see the differences.

[Ruben Van de Velde]

I hear the speedcenter is down

[Jovan Gerbscheid]

It was down yesterday, but not anymore I think

[Cameron Zwarich]

Jovan Gerbscheid said:

Do you have a speedcenter comparison to see what the impact on mathlib is? I'd be curious to see the differences.

No, I actually didn't even know that it was possible to test the build time of Mathlib for a PR that way. That might be helpful in the future. This week there's also the additional complication that I can't push changes to branches in the mathlib4 repo for my PRs against lean4.

I did do some perf testing clean builds of Mathlib locally a few weeks ago (just after I got it building) and it was basically identical. There were some considerable performance fixes in the following week, so perhaps that got better since then.

We honestly weren't expecting huge speedups on the core of Lean just from this switch (although we did get some, especially on more code-heavy files), because Lean itself is implemented in a way that avoids most of the performance glass jaws of the old compiler. Newer sections of code (e.g. Lake, the new iterators library, etc.) see larger improvements. However, some of the future compiler improvements unlocked by all of this work should affect Lean itself significantly. There are also some non-compiler improvements, e.g. the new compiler is better able to integrate with async/parallel elaboration and the new module system.

[Matthew Ballard]

It would interesting to see if this #mathlib4 > Why is tensor product noncomputable? @ 💬 is no longer necessary with the new compiler

[Cameron Zwarich]

Yes, I was just about to find the various noncomputable-related threads and reply to them. Understanding exactly what was going on with noncomputable (both the old compiler's implementation and Mathlib's expectations) was a lot of the work in the final push to get this landed. There were even a few cases where I couldn't completely understand why one example from Mathlib was considered computable (non-noncomputable?) but my reduced test case was not.

There is a bit of a tradeoff between wanting the noncomputable check to be smarter and wanting it to be predictable and easy to understand. In an ideal world, we could move it right after elaboration, so that its behavior could be explained without any understanding of compiler optimizations (and we could change thee order of these optimizations freely without affecting the check). Based on my recent experiences, I am somewhat confident that we can make improvements here, and will resurrect some of the discussions here on Zulip to get into the details.

There's also the problem of noncomputable section being useful but making it more difficult to debug why things are happening. I would like to add more detailed error messages that will print a noncomputability trace, potentially through multiple noncomputable sections back to the underlying cause. I had to make a hacky version of this for myself when debugging and I found it useful.

[Jovan Gerbscheid]

For example, I would be curious to know if the definition docs#bestFirstSearch still takes 100 seconds to compile :)