diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eb21083f35..8ae0a11d8e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -181,7 +181,9 @@ 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'" + "CTEST_OPTIONS": "-E 'foreign'", + // not compatible with `prepare-llvm` currently + "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, { "name": "Linux Lake", @@ -192,7 +194,6 @@ 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", @@ -221,7 +222,9 @@ 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 + "tar": "gtar", // https://github.com/actions/runner-images/issues/2619 + // not compatible with `prepare-llvm` currently + "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, { "name": "macOS aarch64", @@ -237,6 +240,8 @@ 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", @@ -249,7 +254,9 @@ jobs: "CTEST_OPTIONS": "--repeat until-pass:2", "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" + "binary-check": "ldd", + // not compatible with `prepare-llvm` currently + "CMAKE_OPTIONS": "-DUSE_LAKE=OFF", }, { "name": "Linux aarch64", @@ -259,7 +266,9 @@ jobs: "check-level": 2, "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*" + "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 45b2b86582..e3e9cc6439 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 -DUSE_LAKE=ON + run: cmake --preset release 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 10168e4f86..015cbddee3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -147,6 +147,10 @@ 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 0f48769d92..43ad0b025e 100644 --- a/doc/dev/bootstrap.md +++ b/doc/dev/bootstrap.md @@ -1,6 +1,6 @@ # Lean Build Bootstrapping -Since version 4, Lean is a partially bootstrapped program: most parts of the +Lean is a bootstrapped program: 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,6 +73,11 @@ 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 @@ -82,13 +87,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 update-stage0-commit` in `build/release` to -update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to +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 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 996f3b5cf4..7b352889d5 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. -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. +Please see below for specific instructions for VS Code. ### Dev setup using elan @@ -68,6 +68,10 @@ 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). +You should then run the `Restart Server` command to update all open files and the server watchdog process as well. + ### `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 04055c00fa..93c22e69c6 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -53,11 +53,6 @@ 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 8f87427beb..459d9d05a1 100755 --- a/script/bench.sh +++ b/script/bench.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash set -euxo pipefail -cmake --preset release -DUSE_LAKE=ON 1>&2 +cmake --preset release 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 e218d0d0de..697bd78dd3 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" OFF) +option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON) 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`")