From af1470d5eca636de7a176b5c7f776c6b55798527 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Nov 2021 11:51:27 +0100 Subject: [PATCH 1/3] chore: symlink to source from build dir --- doc/dev/index.md | 5 +---- shell.nix | 3 --- src/CMakeLists.txt | 11 ++++++++++- stage0/src/CMakeLists.txt | 7 +++++++ 4 files changed, 18 insertions(+), 8 deletions(-) diff --git a/doc/dev/index.md b/doc/dev/index.md index 57eba249538f..38140570c301 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md @@ -27,10 +27,7 @@ install`. You use `elan` instead. 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 will be used for file -in that directory. You should also set the `LEAN_SRC_PATH` environment -variable to the path of the `src/` directory to enable -go-to-definition in the stdlib (automatically set when using -`nix-shell`). +in that directory. ## Dev setup using elan diff --git a/shell.nix b/shell.nix index 6d5bb1de6ef9..7e6705bed149 100644 --- a/shell.nix +++ b/shell.nix @@ -16,9 +16,6 @@ in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs, llvmPackages ? null }: GMP = pkgsDist.gmp.override { withStatic = true; }; GLIBC = pkgsDist.glibc; ZLIB = pkgsDist.zlib; - shellHook = '' - export LEAN_SRC_PATH="$PWD/src" - ''; }; with-temci = shell.overrideAttrs (old: { buildInputs = old.buildInputs ++ [ flakePkgs.temci ]; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7868bdc4629d..97fc2e16f5fa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -528,7 +528,16 @@ add_custom_target(clean-stdlib add_custom_target(clean-olean DEPENDS clean-stdlib) -install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib PATTERN temp EXCLUDE) +install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib + PATTERN src EXCLUDE # symlink + PATTERN temp EXCLUDE) + +# symlink source into expected installation location for go-to-definition, if file system allows it +if(${STAGE} EQUAL 0) + file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/lib/lean/src RESULT _IGNORE_RES SYMBOLIC) +else() + file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib/lean/src RESULT _IGNORE_RES SYMBOLIC) +endif() install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean FILES_MATCHING diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index 12a5a5b6cd9e..c1114802c062 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -520,6 +520,13 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean" DESTINATION lib) install(CODE "execute_process(COMMAND sh -c \"cp ${CMAKE_BINARY_DIR}/lib/*.* \${CMAKE_INSTALL_PREFIX}/lib\")") +# symlink source into expected installation location for go-to-definition, if file system allows it +if(${STAGE} EQUAL 0) + file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/lib/lean/src RESULT _IGNORE_RES SYMBOLIC) +else() + file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib/lean/src RESULT _IGNORE_RES SYMBOLIC) +endif() + install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean FILES_MATCHING PATTERN "*.lean" From 201681c9565539ce88232b8f7de5632111969300 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Nov 2021 11:51:44 +0100 Subject: [PATCH 2/3] feat: resolve symlinks in LEAN_SRC_PATH --- src/Lean/Server/FileWorker/RequestHandling.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 1d04eb5c215a..0cd61b7c7840 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -69,8 +69,12 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) let mod? ← findModuleOf? n let modUri? ← match mod? with | some modName => - let modFname? ← rc.srcSearchPath.findWithExt "lean" modName - pure <| modFname?.map toFileUri + let some modFname ← rc.srcSearchPath.findWithExt "lean" modName + | pure none + -- resolve symlinks (such as `src` in the build dir) so that files are opened + -- in the right folder + let modFname ← IO.FS.realPath modFname + pure <| some <| toFileUri modFname | none => pure <| some doc.meta.uri let ranges? ← findDeclarationRanges? n From bd359c3bbf9237b60a1943f63b7d8d55f0d045cf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Nov 2021 11:59:26 +0100 Subject: [PATCH 3/3] doc: advise using Developer Mode on Windows --- doc/make/msys2.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/make/msys2.md b/doc/make/msys2.md index b917986205e2..4b8ee787f108 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.md @@ -9,6 +9,12 @@ It is easy to install all dependencies, it produces native An alternative to MSYS2 is to use [Lean in Windows WSL](wsl.md). +While not necessary for pure building, you should first activate [Developer +Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-device-for-development) +(Settings > Update & Security > For developers > Developer Mode), +which will allow Lean to create symlinks that e.g. enable go-to-definition in +the stdlib. + ## Installing dependencies [The official webpage of MSYS2][msys2] provides one-click installers.