chore: revert "chore: make USE_LAKE the default" (#10011)
Reverts leanprover/lean4#10003, which broke the merge queue's breakage check
This commit is contained in:
Sebastian Ullrich
GitHub
parent
d604c16c0e
commit
679df58329
8 changed files with 17 additions and 33 deletions
15
.github/workflows/ci.yml
vendored
15
.github/workflows/ci.yml
vendored
|
|
@ -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
|
||||
//{
|
||||
|
|
|
|||
2
.github/workflows/update-stage0.yml
vendored
2
.github/workflows/update-stage0.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
|
||||
|
|
@ -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`)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`")
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue