From 168c125cf5d114834617c6c8c16076ffd593b40d Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 25 Feb 2026 11:23:35 +0100 Subject: [PATCH] chore: relative lean-toolchains (#12652) This PR changes all `lean-toolchain` to use relative toolchain paths instead of `lean4` and `lean4-stage0` identifiers, which removes the need for manually linking toolchains via Elan. After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code extension will be needed to edit core. Co-authored-by: Claude Sonnet 4.6 --- doc/std/grove/lean-toolchain | 2 +- lean-toolchain | 2 +- lean.code-workspace | 12 ------------ script/lean-toolchain | 2 +- src/lean-toolchain | 2 +- tests/bench/mergeSort/lean-toolchain | 2 +- tests/bench/mvcgen/sym/lean-toolchain | 2 +- tests/bench/qsort/lean-toolchain | 2 +- tests/lake/tests/shake/input/lean-toolchain | 2 +- tests/lean-toolchain | 2 +- .../projects/InverseModuleHierarchy/lean-toolchain | 2 +- tests/pkg/builtin_attr/lean-toolchain | 2 +- tests/pkg/cbv_attr/lean-toolchain | 2 +- tests/pkg/debug/lean-toolchain | 2 +- tests/pkg/def_clash/lean-toolchain | 2 +- tests/pkg/deriving/lean-toolchain | 2 +- tests/pkg/frontend/lean-toolchain | 2 +- tests/pkg/initialize/lean-toolchain | 2 +- tests/pkg/leanchecker/lean-toolchain | 2 +- tests/pkg/linter_set/lean-toolchain | 2 +- tests/pkg/misc/lean-toolchain | 2 +- tests/pkg/mod_clash/lean-toolchain | 2 +- tests/pkg/module/lean-toolchain | 2 +- tests/pkg/path with spaces/lean-toolchain | 2 +- tests/pkg/prv/lean-toolchain | 2 +- tests/pkg/rebuild/lean-toolchain | 2 +- tests/pkg/setup/lean-toolchain | 2 +- tests/pkg/signal/lean-toolchain | 2 +- tests/pkg/structure_docstrings/lean-toolchain | 2 +- tests/pkg/test_extern/lean-toolchain | 2 +- tests/pkg/user_attr/lean-toolchain | 2 +- tests/pkg/user_attr_app/lean-toolchain | 2 +- tests/pkg/user_ext/lean-toolchain | 2 +- tests/pkg/user_opt/lean-toolchain | 2 +- tests/pkg/user_plugin/lean-toolchain | 2 +- tests/pkg/ver_clash/lean-toolchain | 2 +- 36 files changed, 35 insertions(+), 47 deletions(-) diff --git a/doc/std/grove/lean-toolchain b/doc/std/grove/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/doc/std/grove/lean-toolchain +++ b/doc/std/grove/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/lean-toolchain b/lean-toolchain index dcca6df980..83c5d0ac92 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -lean4 +build/release/stage1 diff --git a/lean.code-workspace b/lean.code-workspace index 8a1b1429a7..9d53f4b0f7 100644 --- a/lean.code-workspace +++ b/lean.code-workspace @@ -2,21 +2,9 @@ "folders": [ { "path": "." - }, - { - "path": "src" - }, - { - "path": "tests" - }, - { - "path": "script" } ], "settings": { - // Open terminal at root, not current workspace folder - // (there is not way to directly refer to the root folder included as `.` above) - "terminal.integrated.cwd": "${workspaceFolder:src}/..", "files.insertFinalNewline": true, "files.trimTrailingWhitespace": true, "cmake.buildDirectory": "${workspaceFolder}/build/release", diff --git a/script/lean-toolchain b/script/lean-toolchain index dcca6df980..247b118618 100644 --- a/script/lean-toolchain +++ b/script/lean-toolchain @@ -1 +1 @@ -lean4 +../build/release/stage1 diff --git a/src/lean-toolchain b/src/lean-toolchain index 0694e2bc29..9b74c709f1 100644 --- a/src/lean-toolchain +++ b/src/lean-toolchain @@ -1 +1 @@ -lean4-stage0 +../build/release/stage0 diff --git a/tests/bench/mergeSort/lean-toolchain b/tests/bench/mergeSort/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/bench/mergeSort/lean-toolchain +++ b/tests/bench/mergeSort/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/bench/mvcgen/sym/lean-toolchain b/tests/bench/mvcgen/sym/lean-toolchain index dcca6df980..663a5ec06a 100644 --- a/tests/bench/mvcgen/sym/lean-toolchain +++ b/tests/bench/mvcgen/sym/lean-toolchain @@ -1 +1 @@ -lean4 +../../../../build/release/stage1 diff --git a/tests/bench/qsort/lean-toolchain b/tests/bench/qsort/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/bench/qsort/lean-toolchain +++ b/tests/bench/qsort/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/lake/tests/shake/input/lean-toolchain b/tests/lake/tests/shake/input/lean-toolchain index dcca6df980..ff15f240c1 100644 --- a/tests/lake/tests/shake/input/lean-toolchain +++ b/tests/lake/tests/shake/input/lean-toolchain @@ -1 +1 @@ -lean4 +../../../../../build/release/stage1 diff --git a/tests/lean-toolchain b/tests/lean-toolchain index dcca6df980..247b118618 100644 --- a/tests/lean-toolchain +++ b/tests/lean-toolchain @@ -1 +1 @@ -lean4 +../build/release/stage1 diff --git a/tests/lean/interactive/projects/InverseModuleHierarchy/lean-toolchain b/tests/lean/interactive/projects/InverseModuleHierarchy/lean-toolchain index dcca6df980..ff15f240c1 100644 --- a/tests/lean/interactive/projects/InverseModuleHierarchy/lean-toolchain +++ b/tests/lean/interactive/projects/InverseModuleHierarchy/lean-toolchain @@ -1 +1 @@ -lean4 +../../../../../build/release/stage1 diff --git a/tests/pkg/builtin_attr/lean-toolchain b/tests/pkg/builtin_attr/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/builtin_attr/lean-toolchain +++ b/tests/pkg/builtin_attr/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/cbv_attr/lean-toolchain b/tests/pkg/cbv_attr/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/cbv_attr/lean-toolchain +++ b/tests/pkg/cbv_attr/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/debug/lean-toolchain b/tests/pkg/debug/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/debug/lean-toolchain +++ b/tests/pkg/debug/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/def_clash/lean-toolchain b/tests/pkg/def_clash/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/def_clash/lean-toolchain +++ b/tests/pkg/def_clash/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/deriving/lean-toolchain b/tests/pkg/deriving/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/deriving/lean-toolchain +++ b/tests/pkg/deriving/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/frontend/lean-toolchain b/tests/pkg/frontend/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/frontend/lean-toolchain +++ b/tests/pkg/frontend/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/initialize/lean-toolchain b/tests/pkg/initialize/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/initialize/lean-toolchain +++ b/tests/pkg/initialize/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/leanchecker/lean-toolchain b/tests/pkg/leanchecker/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/leanchecker/lean-toolchain +++ b/tests/pkg/leanchecker/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/linter_set/lean-toolchain b/tests/pkg/linter_set/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/linter_set/lean-toolchain +++ b/tests/pkg/linter_set/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/misc/lean-toolchain b/tests/pkg/misc/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/misc/lean-toolchain +++ b/tests/pkg/misc/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/mod_clash/lean-toolchain b/tests/pkg/mod_clash/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/mod_clash/lean-toolchain +++ b/tests/pkg/mod_clash/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/module/lean-toolchain b/tests/pkg/module/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/module/lean-toolchain +++ b/tests/pkg/module/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/path with spaces/lean-toolchain b/tests/pkg/path with spaces/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/path with spaces/lean-toolchain +++ b/tests/pkg/path with spaces/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/prv/lean-toolchain b/tests/pkg/prv/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/prv/lean-toolchain +++ b/tests/pkg/prv/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/rebuild/lean-toolchain b/tests/pkg/rebuild/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/rebuild/lean-toolchain +++ b/tests/pkg/rebuild/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/setup/lean-toolchain b/tests/pkg/setup/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/setup/lean-toolchain +++ b/tests/pkg/setup/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/signal/lean-toolchain b/tests/pkg/signal/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/signal/lean-toolchain +++ b/tests/pkg/signal/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/structure_docstrings/lean-toolchain b/tests/pkg/structure_docstrings/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/structure_docstrings/lean-toolchain +++ b/tests/pkg/structure_docstrings/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/test_extern/lean-toolchain b/tests/pkg/test_extern/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/test_extern/lean-toolchain +++ b/tests/pkg/test_extern/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/user_attr/lean-toolchain b/tests/pkg/user_attr/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/user_attr/lean-toolchain +++ b/tests/pkg/user_attr/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/user_attr_app/lean-toolchain b/tests/pkg/user_attr_app/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/user_attr_app/lean-toolchain +++ b/tests/pkg/user_attr_app/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/user_ext/lean-toolchain b/tests/pkg/user_ext/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/user_ext/lean-toolchain +++ b/tests/pkg/user_ext/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/user_opt/lean-toolchain b/tests/pkg/user_opt/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/user_opt/lean-toolchain +++ b/tests/pkg/user_opt/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/user_plugin/lean-toolchain b/tests/pkg/user_plugin/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/user_plugin/lean-toolchain +++ b/tests/pkg/user_plugin/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1 diff --git a/tests/pkg/ver_clash/lean-toolchain b/tests/pkg/ver_clash/lean-toolchain index dcca6df980..d55e55c366 100644 --- a/tests/pkg/ver_clash/lean-toolchain +++ b/tests/pkg/ver_clash/lean-toolchain @@ -1 +1 @@ -lean4 +../../../build/release/stage1