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