diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 254d0a31f5..eb21083f35 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -181,9 +181,7 @@ jobs: "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*", "binary-check": "ldd -v", // foreign code may be linked against more recent glibc - "CTEST_OPTIONS": "-E 'foreign'", - # not compatible with `prepare-llvm` currently - "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", + "CTEST_OPTIONS": "-E 'foreign'" }, { "name": "Linux Lake", @@ -194,6 +192,7 @@ jobs: "check-stage3": level >= 2, // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest` "test-speedcenter": large && level >= 2, + "CMAKE_OPTIONS": "-DUSE_LAKE=ON", }, { "name": "Linux Reldebug", @@ -222,9 +221,7 @@ jobs: "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst", "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*", "binary-check": "otool -L", - "tar": "gtar", // https://github.com/actions/runner-images/issues/2619 - # not compatible with `prepare-llvm` currently - "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", + "tar": "gtar" // https://github.com/actions/runner-images/issues/2619 }, { "name": "macOS aarch64", @@ -240,8 +237,6 @@ jobs: // See "Linux release" for release job levels; Grove is not a concern here "check-level": isPr ? 0 : 2, "secondary": isPr, - # not compatible with `prepare-llvm` currently - "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, { "name": "Windows", @@ -255,8 +250,6 @@ jobs: "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*", "binary-check": "ldd" - # not compatible with `prepare-llvm` currently - "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, { "name": "Linux aarch64", @@ -267,8 +260,6 @@ jobs: "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}", "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*" - # not compatible with `prepare-llvm` currently - "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation //{ diff --git a/.github/workflows/update-stage0.yml b/.github/workflows/update-stage0.yml index e3e9cc6439..45b2b86582 100644 --- a/.github/workflows/update-stage0.yml +++ b/.github/workflows/update-stage0.yml @@ -70,7 +70,7 @@ jobs: restore-keys: | Linux Lake-build-v3 - if: env.should_update_stage0 == 'yes' - run: cmake --preset release + run: cmake --preset release -DUSE_LAKE=ON shell: 'nix develop -c bash -euxo pipefail {0}' - if: env.should_update_stage0 == 'yes' run: make -j$NPROC -C build/release update-stage0-commit diff --git a/CMakeLists.txt b/CMakeLists.txt index 015cbddee3..10168e4f86 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -147,10 +147,6 @@ add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1) -add_custom_target(clean-stdlib - COMMAND $(MAKE) -C stage1 clean-stdlib - DEPENDS stage1) - install(CODE "execute_process(COMMAND make -C stage1 install)") add_custom_target(check-stage3 diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md index 43ad0b025e..0f48769d92 100644 --- a/doc/dev/bootstrap.md +++ b/doc/dev/bootstrap.md @@ -1,6 +1,6 @@ # Lean Build Bootstrapping -Lean is a bootstrapped program: the +Since version 4, Lean is a partially bootstrapped program: most parts of the frontend and compiler are written in Lean itself and thus need to be built before building Lean itself - which is needed to again build those parts. This cycle is broken by using pre-built C files checked into the repository (which ultimately @@ -73,11 +73,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`. The github repository will automatically update stage0 on `master` once `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync. -NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed. -Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`. -The same is true for further stages except that a rebuild of them is retriggered on any commited change, not just to a specific directory. -Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point. - If you have write access to the lean4 repository, you can also manually trigger that process, for example to be able to use new features in the compiler itself. You can do that on @@ -87,13 +82,13 @@ gh workflow run update-stage0.yml ``` Leaving stage0 updates to the CI automation is preferable, but should you need -to do it locally, you can use `make -C build/release update-stage0-commit` to -update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to +to do it locally, you can use `make update-stage0-commit` in `build/release` to +update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage. This command will automatically stage the updated files -and introduce a commit, so make sure to commit your work before that. +and introduce a commit,so make sure to commit your work before that. If you rebased the branch (either onto a newer version of `master`, or fixing -up some commits prior to the stage0 update), recreate the stage0 update commits. +up some commits prior to the stage0 update, recreate the stage0 update commits. The script `script/rebase-stage0.sh` can be used for that. The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`) diff --git a/doc/dev/index.md b/doc/dev/index.md index e9717f10ad..996f3b5cf4 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md @@ -9,7 +9,7 @@ You should not edit the `stage0` directory except using the commands described i ## Development Setup You can use any of the [supported editors](../setup.md) for editing the Lean source code. -Please see below for specific instructions for VS Code. +If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory. ### Dev setup using elan @@ -68,9 +68,6 @@ code lean.code-workspace ``` on the command line. -You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets. -In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md). - ### `ccache` Lean's build process uses [`ccache`](https://ccache.dev/) if it is diff --git a/doc/make/index.md b/doc/make/index.md index 93c22e69c6..04055c00fa 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -53,6 +53,11 @@ There are also two alternative presets that combine some of these options you ca Select the C/C++ compilers to use. Official Lean releases currently use Clang; see also `.github/workflows/ci.yml` for the CI config. +* `-DUSE_LAKE=ON`\ + Experimental option to build the core libraries using Lake instead of `lean.mk`. Caveats: + * As native code compilation is still handled by cmake, changes to stage0/ (such as from `git pull`) are picked up only when invoking the build via `make`, not via `Refresh Dependencies` in the editor. + * `USE_LAKE` is not yet compatible with `LAKE_ARTIFACT_CACHE` + Lean will automatically use [CCache](https://ccache.dev/) if available to avoid redundant builds, especially after stage 0 has been updated. diff --git a/script/bench.sh b/script/bench.sh index 459d9d05a1..8f87427beb 100755 --- a/script/bench.sh +++ b/script/bench.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash set -euxo pipefail -cmake --preset release 1>&2 +cmake --preset release -DUSE_LAKE=ON 1>&2 # We benchmark against stage2/bin to test new optimizations. timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 697bd78dd3..e218d0d0de 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -81,7 +81,7 @@ option(USE_MIMALLOC "use mimalloc" ON) # development-specific options option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF) -option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON) +option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" OFF) set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make") set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")