Lake: Compile all dependencies with same options set

Stream: general

[Simon Dima]

I have a small lake package called leaf which depends on another package, stem. Both are local on my machine, and leaf refers to stem by the filesystem path.

I want to test compiling leaf with the old and new Lean compilers. If leaf was a standalone package, adding moreLeanArgs = ["-D compiler.enableNew=false"] (resp true) to its lakefile.toml would work, I think, but this leads to errors when not set to the default. I think this is because lake is setting the option only for the compilation of leaf, and so stem is compiled using the setting in its own Lakefile, which is incompatible.

Is there a way to specify options that also apply to the compilation of stem in leaf's Lakefile? I want to avoid having to change stem's Lakefile each time.

Another solution approach I thought about was changing leaf's lean-toolchain file to use different versions of Lean with the default value of compiler.enableNew set to false resp. true; I hoped this would make Lake recompile stem with the toolchain specified for leaf, but this doesn't seem to work either. Lake outputs

warning: toolchain not updated; multiple toolchain candidates:

but it's not clear to me which toolchain it ends up using.

[Simon Dima]

If I understand correctly this would also not be a problem if stem wasn't a local package, because in that case stem's sources would be copied over into leaf's .lake directory and built there. Does that sound right? Is there a way to get Lake to treat stem as a non-local package?

[Simon Dima]

I've tried mucking around with require … with and get_config? to enable leaf to tell Lake that it wants stem to be built with specific leanOptions, but with no success so far.
From the messages I'm getting, which look like failed to compile definition, consider marking it as 'noncomputable' because it depends on 'instOfNatNat', and it does not have executable code, I assume that lake is using the Init oleans from my Lean installation, which were compiled with a different value of compiler.enableNew. Is there some way I can tell Lake to recompile everything?

[Simon Dima]

@Cameron Zwarich, I assume you must test things between the old and new compiler regularly. What's your workflow for that? I feel like the solutions I'm considering are too complicated, I hope I'm missing something

[Cameron Zwarich]

@Simon Dima I use git worktree to make two directories tracking two separate branches and constantly rebuild things. I do have the advantage of an extremely overpowered dev machine.

Thankfully, the new compiler will probably be enabled by default within the next week, so there won't be much of a need to do this any longer. After that, switching to the old compiler will require a stage0 update, similar to testing the new one right now. I suspect that the code will stick around for a short while, but we will also make no real effort to keep it working.

[Simon Dima]

I use git worktree to make two directories tracking two separate branches and constantly rebuild things.

I'll look into that to see if it helps with my usecase, thanks!

Thankfully, the new compiler will probably be enabled by default within the next week, so there won't be much of a need to do this any longer.

Yay! But alas, I would like to compare both the old and new compiler, which won't become much easier (Though I do look forward to no longer having to wait a few hours every once in a while for the new-codegen branch to build on my extremely underpowered machine, when the next release with the new compiler enabled by default comes out.)

So is set_option compiler.enableNew only usable for definitions which do not depend on anything defined before the option was set, and there's no good way to get it to apply to everything?

[Cameron Zwarich]

@Simon Dima That's basically correct. There are some changes we could've made to make this work better (e.g. have the IR phases use separate environment extensions for storing IR from each compiler), but at the time it was seemed like it was only me testing this, and it would actually slow down the 10+ bootstrap builds I do every day. Apologies if I made the wrong decision a few months ago.

If you find any interesting codegen differences, please let me know about it. The largest set of issues that I am aware about are due to IR passes having suboptimal behavior related to the increased usage of join points. It is unlikely that all of these will be fixed before enabling the new compiler. Another set is related to inlining heuristics: the old compiler inlines a lot more, and while increasing inlining thresholds can even decrease binary size, there are some perf regression outliers that make it a non-obvious choice. Tuning inlining heuristics is one of the most tedious parts of compiler engineering, and I'd rather leave it for the (hopefully short-term) future where we have support for recursive join points, which will lead to increased usage of inlining over specialization and change the tradeoffs anyways.