feat: support Lake for building Lean core oleans

[david-christiansen]

This is from a pairtriple programming session with @tydeu and @mhuisi.

If stage 1 is built with -DUSE_LAKE=ON, the CMake run will generate lakefile.toml files for the root, src, and tests. These Lake configuration files can then be used to build core oleans. While they do not yet allow Lake to be used to build the Lean binaries. they do allow Lake to be used for working interactively with the Lean source. In our preliminary experiments, this allowed updates to Init.Data.Nat to be noticed automatically when reloading downstream files, rather than requiring a full manual compiler rebuild. This will make it easier to work on the system.

As part of this change, Lake is added to stage 0. This allows Lake to function in src, which uses the stage 0 toolchain.

[Kha]

The lakefile.toml will have to be generated by CMake to correctly heed LEAN_MAKE_OPTS/LEANC_OPTS/...

[tydeu]

@Kha Right now, this is just for interactive editing, not for building the binaries or shared libraries, so we do not need those options at the moment.

[Kha]

Okay, I would not have expected that to be a desirable intermediate state if it forces me to redo the build in cmake whenever I want to actually run and test Lean. It also begs the question of how to opt into the current workflow when the lakefile.toml always exists.

[tydeu]

@Kha

Okay, I would not have expected that to be a desirable intermediate state if it forces me to redo the build in cmake whenever I want to actually run and test Lean.

While it does require an additional run of CMake to run/test Lean, it does not require redoing work, as Make can successfully make use of elaboration results (as there are no relevant LEAN_OPTS to standard dev builds).

[tydeu]

I am flummoxed by the linker errors in the CMake build of stage0 Lake. It builds successfully on my machine.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 092ca8530a6f272b7cb19235750479cdffab11de --onto b470eb522bfd68ca96938c23f6a1bce79da8a99f. (2024-05-03 08:38:43)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 092ca8530a6f272b7cb19235750479cdffab11de --onto 00cf5771f31e7de7f6ab3089cb4b9ffa606a35ed. (2024-05-03 19:35:36)
• ✅ Mathlib branch lean-pr-testing-3886 has successfully built against this PR. (2024-06-11 02:53:48) View Log
• ✅ Mathlib branch lean-pr-testing-3886 has successfully built against this PR. (2024-06-11 09:44:23) View Log
• ✅ Mathlib branch lean-pr-testing-3886 has successfully built against this PR. (2024-06-13 17:26:42) View Log

[Kha]

I added a -DUSE_LAKE=ON CMake flag to opt into the new behavior and to fix the hard-coded path so if that looks good and the stage0 update is removed to be redone on master, I think this PR is ready to be merged.

It wasn't clear to me why the additional lakefile.tomls in the root and in tests/ are necessary, so I've removed them for now.

[tydeu]

@Kha

It wasn't clear to me why the additional lakefile.tomls in the root and in tests/ are necessary, so I've removed them for now.

They are necessary for the multiple roots of the VS Code workspace. Each root needs to have a lakefile for the server to make use of Lake at that root. Without them, Lake will not be used for Lean files in the root (outside src/) or in tests/.

[Kha]

Why is that relevant? tests/ is not a Lake project, even running the full build from src/ in it does not help as it will not actually build the executables. I'd rather have it not to work at all than stop half-way to a successful build.

[tydeu]

@Kha

Why is that relevant? tests/ is not a Lake project, even running the full build from src/ in it does not help as it will not actually build the executables.

It is not for building (e.g., the executables). It is for interactively editing the tests using the modules built from src (via Lake in the server). For example, when we pair programming this at the retreat, we added a definition in Init.Data.Nat and the immediately saw the change propagate to a test file in tests.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit a25f4b4.
There were no significant changes against commit 287d46e.

[tydeu]

@Kha What are you attempting to benchmark? Without the stage0 update, this PR has no practical effect.

[Kha]

@tydeu The update-stage0 size increase but I noticed we don't actually have a benchmark for that :) . Do you know how much it was?