diff --git a/README.md b/README.md index eb188ad01a..da7eeb3c34 100644 --- a/README.md +++ b/README.md @@ -105,7 +105,7 @@ Examples of different package configurations can be found in the [`examples`](ex ## Glossary of Terms -Lake uses a lot of terms common in software development -- like workspace, package, library, executable, target, etc. -- and some more esoteric onces -- like facet. However, whether common or not these terms mean different things to different people, so it is important to elucidiate how Lake defines these terms: +Lake uses a lot of terms common in software development -- like workspace, package, library, executable, target, etc. -- and some more esoteric ones -- like facet. However, whether common or not, these terms mean different things to different people, so it is important to elucidate how Lake defines these terms: * A **package** is the **fundamental unit of code distribution in Lake**. Packages can be sourced from the local file system or downloaded from the web (e.g., via Git). The `package` declaration in package's lakefile names it and [defines its basic properties](#package-configuration-options). @@ -139,9 +139,9 @@ Lake provides a large assortment of configuration options for packages. * `manifestFile`: The path of a package's manifest file, which stores the exact versions of its resolved dependencies. Defaults to `lake-manifest.json`. * `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.) * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`. -* `oleanDir`: The build subdirectory to which Lake should output the package's `.olean` files. Defaults to `lib`. -* `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`. -* `libDir`: The build subdirectory to which Lake should output the package's libraries. Defaults to `lib`. +* `oleanDir`: The build subdirectory to which Lake should output the package's binary Lean libraries (i.e., `.olean`, `.ilean` files). Defaults to `lib`. +* `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c`, `.o` files). Defaults to `ir`. +* `libDir`: The build subdirectory to which Lake should output the package's native libraries (e.g., `.a`, `.so`, `.dll` files). Defaults to `lib`. * `binDir`: The build subdirectory to which Lake should output the package's binary executables. Defaults to `bin`. ### Build & Run