From c0edda137315db281e37a4c872d67339331f3d1a Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 7 Jun 2023 22:25:52 -0400 Subject: [PATCH] doc: fix some README wording --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index b4b7b42c24..638326e838 100644 --- a/README.md +++ b/README.md @@ -372,6 +372,6 @@ Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby) The `lake` executable needs to know where to find the Lean library files (e.g., `.olean`, `.ilean`) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and `lean`. -Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in `/bin`, their Lean libraries in `/lib/lean`, Lean's source files in `/src/lean`, and Lake's source files in `/src/lean/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `/build/bin/lake` with its Lean libraries at `/build/lib` and its sources in directly in ``. +Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in `/bin`, their Lean libraries in `/lib/lean`, Lean's source files in `/src/lean`, and Lake's source files in `/src/lean/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `/build/bin/lake` with its Lean libraries at `/build/lib` and its sources directly in ``. -This search path can be augmented by including other directories of Lean libraries in the `LEAN_PATH` environment variable (and their sources in `LEAN_SRC_PATH`), allowing the user to correct Lake's search if the files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important in development, as it prevents the Lake version being used to build Lake from using the Lake version being built's Lean libraries to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors). +This search path can be augmented by including other directories of Lean libraries in the `LEAN_PATH` environment variable (and their sources in `LEAN_SRC_PATH`). This can allow the user to correct Lake's search when the files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important during development, as this prevents the Lake version used to build Lake from using the Lake version being built's Lean libraries (instead of its own) to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors).