From 8d543cbcdcec6b04064ea3d4b3d12a61d7b015c4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 26 Mar 2021 09:54:45 +0100 Subject: [PATCH] doc: using Nix with an external editor --- doc/setup.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/setup.md b/doc/setup.md index 2ac18d301a..400e975d6f 100644 --- a/doc/setup.md +++ b/doc/setup.md @@ -87,6 +87,13 @@ Note that if you rename `MyPackage.lean`, you also have to adjust the `name` att As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command. +If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally: +```bash +$ nix build .#lean-dev -o result-lean-dev +``` +The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed. +This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](../make/nix.md#editor-integration). + Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency: