diff --git a/README.md b/README.md index b631ae8..1d9eb93 100644 --- a/README.md +++ b/README.md @@ -104,15 +104,15 @@ Lake uses a lot of terms common in software development -- like workspace, packa * 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). -* A **lakefile** is the Lean file that configures a package. It defines how to view, edit, build, and run the code within it and specifies what other packages it may require in order to do so. +* A **lakefile** is the Lean file that configures a package. It defines how to view, edit, build, and run the code within it, and it specifies what other packages it may require in order to do so. * A **dependency** is a package required by another package and the package requiring it is its **dependent**. See the [Adding Dependencies section](#adding-dependencies) for details on how to specify dependencies. * A **workspace** is the **broadest organizational unit in Lake**. It bundles together a package (termed the **root**), its transitive dependencies, and Lake's environment. Every package can operate as the root of a workspace and the workspace will derive its configuration from this root. -* A **module** is **the smallest unit of code visible to Lake's build system**. It is generally represented by a Lean source file and a set of binary libraries (i.e., a Lean `olean` and `ilean` plus a system shared library if `precompileModules` is turned on). Modules can import one another in order to use each other's code and Lake exists primarily to facilitate this process. +* A **module** is the **smallest unit of code visible to Lake's build system**. It is generally represented by a Lean source file and a set of binary libraries (i.e., a Lean `olean` and `ilean` plus a system shared library if `precompileModules` is turned on). Modules can import one another in order to use each other's code and Lake exists primarily to facilitate this process. -* A **(Lean) library** is a collection of modules that share a single configuration. Its modules are defined by its source directory, a set of **module roots**, and a set of **module globs**. See the [Lean Libraries section](#lean-libraries) for more details. +* A **Lean library** is a collection of modules that share a single configuration. Its modules are defined by its source directory, a set of **module roots**, and a set of **module globs**. See the [Lean Libraries section](#lean-libraries) for more details. * A **Lean binary executable** is a binary executable (i.e., a program a user can run on their computer without Lean installed) built from a Lean module termed its **root** (which should have a `main` definition). See the [Binary Executables section](#binary-executables) for more details. @@ -120,8 +120,9 @@ Lake uses a lot of terms common in software development -- like workspace, packa * A **target** is the **fundamental build unit of Lake**. A package can defining any number of targets. Each target has a name, which is used to instruct Lake to build the target (e.g., through `lake buld `) and to keep track internally of a target's build status. Lake defines a set of builtin target types -- [Lean libraries](#lean-libraries), [binary executables](#binary-executables), and [external libraries](#external-libraries) -- but a user can [define their own custom targets as well](#custom-targets). Complex types (e.g., packages, libraries, modules) have multiple facets, each of which count as separate buildable targets. See the [Defining Build Targets section](#defining-build-targets) for more details. +* A **facet** is an element built from another organizational unit (e.g., a package, module, library, etc.). For instance, Lake produces `olean`, `ilean`, `c`, and `o` files all from a single module. Each of these components are thus termed a *facet* of the module. Similarly, Lake can build both static and shared binaries from a library. Thus, libraries have both `static` and `shared` facets. Lake also allows users to define their own custom facets to build from modules and packages, but this feature is currently experimental and not yet documented. -* A **facet** is a element built from another organizational unit (e.g., a package, module, library, etc.). For instance, Lake produces `olean`, `ilean`, `c`, and `o` files all from a single module. Each of these components are thus termed a *facet* of the module. Similarly, Lake can build both static and shared binaries from a library. Thus libraries have both `static` and `shared` facets. Lake also allows users to define their own custom facets to build from modules and packages, but this feature is currently experimental and not yet documented. +* A **trace** is a piece of data (generally a hash) which is used to verify whether a given target is up-to-date. If the trace stored with a built target matches the trace computed during build, then a target is considered up-to-date. A target's trace is derived from its various **inputs** (e.g., source file, Lean toolchain, imports, etc.). ## Package Configuration Options