Symlink to source from build dir for go-to-definition

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
 

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.

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 ];

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

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