RFC: Lazy code generation

Stream: lean4 dev

[Henrik Böving]

I just had a talk with @Jannis Limperg where he showed me a file that consumes several seconds of compilation time in the old code generator (the new one just a few hundred ms though :sparkles:) even though he only wants to live edit the file (so there is obviously need for constant recompilation by the LSP elaboration process). As I understand it we currently always add and compile declarations (that we can generate code for anyways) when they are done with being elaborated. I am guessing this is because we want to be able to always #eval them in the same file. However it is obviously not acceptable to wait ~5 seconds on a computation that has essentially no effect if you do not want to #eval and did not indicate to the lean compiler that you desire to output a binary (i.e. you are just editing code without using #eval which is the most common use case of Lean programmers).

The most naive idea I'd have for "fixing" this (apart from finally gettig the new code generator done /o\) would be to add an option that allows you to disable compilation completely (very similar to the new code generator option I proposed in this PR: https://github.com/leanprover/lean4/pull/2075). A slightly better and more user friendly approach might be to compile code conditionally, that is things like #eval check if the declaration has been compiled and if it has not run the compilation procedure on it, this does obviously have some usability impacts as well since for example code generator error messages would be cumulated on the #eval line but those would be a bug anyways.

If we wanted to do this the LSP Lean process would basically have to run in a "no code generation" (or "lazy code generation") mode (unless explicitly asked to, e.g. useful for code generator devs like me) while the flags that lake (or cmake for that matter) passes to the compiler would make it run the compilation procedure again.

Does this approach sound reasonable?

[Kyle Miller]

Re disabling compilation: in Lean 3 we had some issues with the code generator (i.e., the VM compiler) either mistakenly failing or taking a very long time, so since we were never going to put resources into fixing it, I added a noncomputable! modifier to turn it off completely for a definition. We had considered a noncomputable! theory to turn off code generation for all definitions, but, while I remember that there were reasons against having such a feature, I don't remember what they were.

[Kyle Miller]

Do I remember correctly that the Lean 4 way of determining whether a definition is marked noncomputable is whether the code generator succeeds or not? If so, that's a complication to lazily generating code. (The Lean 4 situation is an improvement to the Lean 3 one, where there is a separate noncomputability checker that has to guess whether or not the VM compiler will succeed. The noncomputable! feature is partly there to override the checker when it is wrong.)

[Sebastian Ullrich]

Separating compilation from file elaboration is a topic that has come up a few times before, both to improve parallelism as well as efficiency of the hypothetical module system. For interpretation purposes I would indeed run the compiler pipeline on demand, ideally even a simpler pipeline than usual, and then throw away the results at the end of the file in favor of the proper compilation running as a separate build task.

[Sebastian Ullrich]

But also what Kyle said sounds like a central issue, yeah

[Jannis Limperg]

Henrik Böving said:

(the new one just a few hundred ms though :sparkles:)

Small correction: the new codegen still takes 1.4s on my machine. Everything else about the file takes 2s, so disabling compilation would amount to a substantial speedup even with the new codegen.

What's the trouble with a separate check for noncomputability? Is this inherently hard or is Lean 3 just buggy?

[Kyle Miller]

"Computable" in Lean means "we can generate code", so the most accurate check is whether the code generator succeeds. I think most Lean 3 bugs are either (1) the noncomputability checker is too strict (i.e., it doesn't realize some noncomputable thing is dead code or otherwise transformable into something computable) or (2) the code generator has a bug and it fails to compile something that passes the noncomputability checker.

It's clear what to do with the second sort of bug(*), but how do you handle the first type without eventually re-implementing most of the code generator?

Rather than re-implementing it, maybe there's some part of the code generator that could run with some faster configuration (e.g., turn off optimizations that don't alter computability) that could serve as a noncomputability checker? This is similar to Sebastian's idea of a simpler pipeline.

Or, maybe the way definitions are marked noncomputable could be re-thought? Does anything need to know what is noncomputable except for the code generator? Could the noncomputable modifiers be checked eventually rather than immediately? If there is something that wants to know, that thread could wait on the code generator for that definition.

(*) It's been "don't fix it because Lean 4 is around the corner" :smile:

[Mario Carneiro]

One point of comparison here would be cargo check vs cargo build for rust code. cargo check is intended for active development, and it roughly speaking only runs the type checker and does not attempt to generate code, while cargo build also runs the code generator. There is a very small category of compile time errors that are caught only at cargo build time, called "post-monomorphization errors"; if you are doing development with cargo check only then you will not get these errors. (These include things like "this type is too large to exist on the architecture" in addition to static assertions about generic types; the latter category used to only be doable with complicated hacks but will soon get simpler syntax to invoke.)

For lean, I find cargo check comparable to doing type checking without code generation (or only doing lazy code generation / interpreter code) and cargo build comparable to lake build done at the command line (including in particular anything which is cross-file). This would suggest the following course of action: noncomputable checking is simply not done at all in interactive mode (or it is controlled by a default-disabled flag), but it is done by lake build so you get errors about it at the command line.

[Jannis Limperg]

Mario's suggestion would be better than the status quo imo. But even better would be if we had a simple criterion for what should count as computable (i.e. Lean 3's computability checker, only not buggy). I feel like this criterion ought to be much simpler than the whole code generator and should be considered part of typechecking. However, I have not looked into this in any detail, so there may well be subtleties which make this intractable.

If such a checker misses certain definitions for which code could be generated due to non-obvious optimisations, that to me is a feature. I don't want the computability of a definition to depend on codegen heuristics which may change at any time.

[Henrik Böving]

What exactly is hard about computability checking? The only thing that we cannot generate code for right now is recursors right? (and that is also mostly because nobody has wanted to do this yet, its not like this is impossible, its just annoying to get right in a strict language). Are there any other things we look out for?

[Kyle Miller]

@Jannis Limperg I'm not sure where you're getting the idea that the Lean 3 computability checker is buggy -- as far as I know it only lets through things that are computable, and it's the VM compiler that ends up being wrong due to its own bugs. The fundamental issue is having two parallel implementations of roughly the same things (inlining, let-substitutions, computational irrelevance analysis) and them not matching up exactly due to slight differences in how they're implemented.

The noncomputability checker is fairly simple, but it's frustrating when it mistakenly flags things as being noncomputable due to its simplistic algorithm. That's not a bug per se, but it being overly strict.

[Kyle Miller]

Regarding cargo check, doesn't that involve compiling all the rust code to at least MIR to be able to do borrow checking analysis?

[Kyle Miller]

Like rust, we don't need to run the entire code generator, just up to the point where we can do the analysis that can tell whether the definition is computable. (Examples of what needs to be done: inlining, applying csimp lemmas, ignoring computationally irrelevant values like types and proofs, ignoring arguments that are computationally irrelevant like the parameters and indices for constructors, ...)

[Mario Carneiro]

Kyle Miller said:

Regarding cargo check, doesn't that involve compiling all the rust code to at least MIR to be able to do borrow checking analysis?

Yes, but I would argue that this is roughly equivalent to lean having to elaborate the syntax into an Expr. In particular generic functions are still generic, so many optimization passes cannot run, or will need to be run again later (like inlining). I agree that the lean 3 style for doing noncomputable checking does not seem inherently flawed to me, and can fit as part of the "check" configuration, but not the lean 4 style which involves literally running the code generator.

[Mario Carneiro]

But I can understand if the maintenance overhead of a separate noncomputable checker is considered too high.

[Mario Carneiro]

One thing to consider about using a separate noncomputable checker which is framed in a more "type checking" way is that it would be less sensitive to optimizations. For example, calling a noncomputable function in a statement that is optimized out will probably work with lean 4 style checking, and that may not be a good thing (since it means that optimization changes can break code). This is a big no-no in rust, the compiler goes out of its way to avoid this situation because it has such a strong focus on avoiding breaking changes

[Mario Carneiro]

case in point:

noncomputable def foo := 1
def bar : Nat := let x := foo; 1

lean 3 would not accept this code

[Kyle Miller]

Lean 3 does accept this code:

noncomputable! def foo := 1
def bar : ℕ := let x := foo in 1

(I put noncomputable! just to force foo to be noncomputable.)

Just to make this more obvious that it's not unfolding foo:

noncomputable def foo := classical.arbitrary ℕ
def bar : ℕ := let x := foo in 1

And of course this does not affect Lean 4 computability:

noncomputable def foo := Classical.arbitrary Nat
def bar : Nat := let x := foo; 1

[Kyle Miller]

How do you profile different compiler passes? How much time does it take to get to compiler.stage2 (which is already pretty far along) vs running the whole thing? That's the point where at least computationally irrelevant things have been removed and simplification passes have been done, and these seem to happen after compiler.stage1. (Also, how close is this architecture to the new compiler?)

[Mario Carneiro]

hm, bad example. Better:

-- Lean 4
noncomputable def foo := 1
def bar : Nat := have x := foo; 1 -- ok

-- Lean 3
noncomputable! def foo := 1
def bar : ℕ := have x : nat, from foo, 1 -- fails

[Kyle Miller]

I'd need to recompile Lean 3 to check, but I'd guess the Lean 3 example would be able to generate code anyway for that example.

Here are examples with the same behavior but without the have notation:

-- Lean 4
noncomputable def foo := Classical.arbitrary Nat
def bar : Nat := (fun (x : Nat) => 1) foo -- ok

-- Lean 3
noncomputable def foo := classical.arbitrary ℕ
def bar : ℕ := (λ (x : ℕ), 1) foo

For Lean 4, both the have and fun examples pretty quickly see foo is unused and eliminate it (at least a few steps before compiler.stage1).

The Lean 3 noncomputability checker only knows about substituting lets, which is arguably just an approximation. For applications it only knows about inlining, and that not every argument to a constructor is computationally relevant.

[Jannis Limperg]

Regarding me calling the Lean 3 checker "buggy": if the checker fails to recognise "obvious" computable functions as such, I would call this a bug as well. (A completeness bug, then, not a soundness bug.) My impression was that this was happening often enough to be annoying. But maybe these cases are actually rare and the involved functions can be rewritten fairly easily to satisfy the checker? I have no clear picture.

I strongly agree with Mario's point that optimisations should not change what is or isn't considered noncomputable. So I would still advocate for a Lean 3-style checker. However, a compromise would be possible: introduce a checker, but also a keyword (computable!?) that disables the checker and defers the decision to the codegen. This way the hack is at least localised. This would also allow the checker to be even simpler, possibly even disabling let-inlining and such, if that's desired.

[Mario Carneiro]

I would prefer to solve the let-inlining situation by having a proper "type system" solution: marking let and lambda variables as "ghost" based on the results of computability analysis of the things assigned to them, and using that to propagate information to the body. In other words, it should be possible to argue that have x := foo; 1 is computable without inlining

[Sebastian Ullrich]

So not too different from irrelevance analysis in other systems. I wonder if we need to make it interprocedural (via annotations) if we want to avoid inlining (though adhering to macro_inline might still make sense). If someone was motivated, could be interesting to adjust/simplify the Lean 3 computability checker in that way and/or port and test it on Lean 4.

[Mario Carneiro]

the interprocedural version sounds doable but also much closer to a paper-worthy topic, since you would need a little algebra of "this is computable if that is computable" annotations on higher order functions

[Sebastian Ullrich]

Yep, that's where the fun begins. Which is why we should first find out if there is a need for it.

[Mario Carneiro]

I would be happy with just a binary thing + some kind of inlining

[Mario Carneiro]

IIRC one place where the noncomputable checker wasn't doing what I wanted was in docs#erased

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/nonconstructive.20proofs/near/252687109

[Henrik Böving]

Kyle Miller said:

How do you profile different compiler passes? How much time does it take to get to compiler.stage2 (which is already pretty far along) vs running the whole thing? That's the point where at least computationally irrelevant things have been removed and simplification passes have been done, and these seem to happen after compiler.stage1. (Also, how close is this architecture to the new compiler?)

Regarding the profiling passes, can someone explain to me of the profiler option makes the timings appear on the synthInstance traces? I'll add it for at least the new compiler then...I suspect the old compiler might be uglier since it stays in C++ until phase 3/3