chore: symlink to source from build dir

Author: Kha

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
 

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