diff --git a/doc/setup.md b/doc/setup.md
index b5aa6ee49e..99b09edaa4 100644
--- a/doc/setup.md
+++ b/doc/setup.md
@@ -24,6 +24,9 @@ It has been tested on Windows by installing these tools using [MSYS2](https://ww
 
 Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4/tree/master/lean4-mode/README.md), [VS Code](https://github.com/mhuisi/vscode-lean4), and possibly other editors.
 
+There is no integration of `leanpkg` and the language server at the moment, so the `LEAN_PATH`, which is the last line returned by `leanpkg configure`, must be set explicitly before starting the editor.
+Changes must be saved and compiled with `leanpkg build` to be visible in other files, which must then be invalidated using an editor command (see links above).
+
 ## Nix Setup
 
 The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension. Howeover, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
@@ -67,6 +70,9 @@ $ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code
 ```
 Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
 
+There is preliminary integration of the Nix-based build system into editors started as above, which automatically builds dependencies when opening or invalidating a file.
+There is no progress report yet, and build errors from dependencies will crash the language server; see the stderr logs for the build error in that case.
+
 Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
 
 For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean
index 78ee3a8fde..ecbfad043e 100644
--- a/src/Leanpkg.lean
+++ b/src/Leanpkg.lean
@@ -75,14 +75,14 @@ def usage :=
 
 Usage: leanpkg <command>
 
-configure              download dependencies
-build [-- <Lean-args>] download dependencies and build *.olean files
+configure              download and build dependencies and print resulting LEAN_PATH
+build [-- <Lean-args>] configure and build *.olean files
 init <name>            create a Lean package in the current directory
 
 See `leanpkg help <command>` for more information on a specific command."
 
 def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
-  | "configure", [],     []        => discard <| configure
+  | "configure", [],     []        => configure >>= IO.println
   | "build",     _,      leanArgs  => build leanArgs
   | "init",      [Name], []        => init Name
   | "help",      ["configure"], [] => IO.println "Download dependencies