doc: update w/ extern_lib + some cleanup

Lake/Config/Package.lean

@@ -69,6 +69,10 @@ structure PackageConfig extends WorkspaceConfig where
   /-
   An `Array` of the package's dependencies.
   See the documentation of `Dependency` for more information.
+
+  **DEPRECATED:**
+  This setting will be removed in a future version of Lake.
+  Use the `require` syntax to declare dependencies instead.
   -/
   dependencies : Array Dependency := #[]
 
@@ -200,6 +204,8 @@ structure PackageConfig extends WorkspaceConfig where
   Additional library `FileTarget`s (beyond the package's and its dependencies'
   Lean libraries) to build and link to the package's binaries (and to dependent
   packages' binaries).
+
+  **DEPRECATED:** Use separate `extern_lib` targets instead.
   -/
   moreLibTargets : Array FileTarget := #[]
 

README.md

@@ -1,21 +1,22 @@
 # Lake
 
 Lake (Lean Make) is a new build system and package manager for Lean 4.
-With Lake, package configuration is written in Lean inside a dedicated `lakefile.lean` stored in the root of the package directory. Each `lakefile.lean` includes a `package` declaration (akin to `main`) which defines the package's configuration.
+With Lake, the package's configuration is written in Lean inside a dedicated `lakefile.lean` stored in the root of the package's directory.
+
+Each `lakefile.lean` includes a `package` declaration (akin to `main`) which defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via `lake script run`).
 
 ## Table of Contents
 
 * [Getting Lake](#getting-lake)
 * [Creating and Building a Package](#creating-and-building-a-package)
 * [Package Configuration Options](#package-configuration-options)
-  + [Workspace Options](#workspace-options)
-  + [Per Package Options](#per-package-options)
 * [Defining Build Targets](#defining-build-targets)
   + [Lean Libraries](#lean-libraries)
   + [Binary Executables](#binary-executables)
+  + [External Libraries](#external-libraries)
 * [Adding Dependencies](#adding-dependencies)
   + [Syntax of `require`](#syntax-of-require)
-* [Writing and Running Lake Scripts](#writing-and-running-lake-scripts)
+* [Writing and Running Scripts](#writing-and-running-scripts)
 * [Building and Running Lake from the Source](#building-and-running-lake-from-the-source)
   + [Building with Nix Flakes](#building-with-nix-flakes)
   + [Augmenting Lake's Search Path](#augmenting-lakes-search-path)
@@ -24,7 +25,7 @@ With Lake, package configuration is written in Lean inside a dedicated `lakefile
 
 Lake is part of the [lean4](https://github.com/leanprover/lean4) repository and is distributed along with its official releases (e.g., as part of the [elan](https://github.com/leanprover/elan) toolchain). So if you have installed a semi-recent Lean 4 nightly, you should already have it!
 
-Note that the Lake included with Lean is not updated as frequently as this repository, so some bleeding edge features may be missing. If you want to build the latest version from the source yourself, check out the build instructions at the bottom of this README.
+Note that the Lake included with Lean is not updated as frequently as this repository, so some bleeding edge features may be missing. If you want to build the latest version from the source yourself, check out the [build instructions](#building-and-running-lake-from-the-source) at the bottom of this README.
 
 ## Creating and Building a Package
 
@@ -82,7 +83,7 @@ lean_exe hello {
 }
 ```
 
-The command `lake build` can then be used to build the package (and its dependencies, if it has them) into a native executable. The result will be placed in `build/bin`.
+The command `lake build` can then be used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `build/bin`.
 
 ```
 $ lake build
@@ -97,13 +98,13 @@ Examples of different package configurations can be found in the [`examples`](ex
 
 Lake provides a large assortment of configuration options for packages.
 
-### Workspace Options
+**Workspace Options**
 
 Workspace options are shared across a package and its dependencies.
 
 * `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `lean_packages`.
 
-### Per Package Options
+**Per Package Options**
 
 * `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`.
@@ -115,12 +116,12 @@ Workspace options are shared across a package and its dependencies.
 * `moreServerArgs`:  Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
 * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files.
 * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes `-O3` and `-DNDEBUG` automatically, but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
-* `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' Lean libraries) to build and link to the package's binaries (and to dependent packages' binaries).
-* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** Package facets will be removed in a future version of Lake. Use a separate `lean_lib` or `lean_exe` default target instead.
+* `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' Lean libraries) to build and link to the package's binaries (and to dependent packages' binaries). **DEPRECATED:** Use separate [`extern_lib`](#external-libraries) targets instead.
+* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** Package facets will be removed in a future version of Lake. Use a separate [`lean_lib`](#lean-libraries) or [`lean_exe`](#binary-executables) default target instead.
 
 ## Defining Build Targets
 
-A Lake package can include multiple configurations for building different Lean libraries and binary executables. Libraries are defined using the `lean_lib` command and executables are defined using `lean_exe`. Any number of these declarations can be marked with the `@[defaultTarget]` attribute to tell Lake to build them on a bare `lake build` of the package.
+A Lake package can have many build targets, such as different Lean libraries and multiple binary executables. Any number of these declarations can be marked with the `@[defaultTarget]` attribute to tell Lake to build them on a bare `lake build` of the package.
 
 ### Lean Libraries
 
@@ -161,6 +162,17 @@ lean_exe «target-name» {
 * `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
 * `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` when linking the binary executable. These will come *after* the paths of libraries built with the package's `moreLibTargets`.
 
+### External Libraries
+
+A external library target is a non-Lean binary library that will be linked to the binaries of the package and its dependents (e.g., their shared libraries and executables).
+
+**Syntax**
+
+```lean
+extern_lib «target-name» :=
+  -- term of type `FileTarget` that builds the external library
+```
+
 ## Adding Dependencies
 
 Lake packages can have dependencies. Dependencies are other Lake packages the current package needs in order to function. They can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositories. For example, one can depend on the Lean 4 port of [mathlib](https://github.com/leanprover-community/mathlib4) like so:
@@ -187,7 +199,7 @@ The first form adds a local dependency and the second form adds a Git dependency
 
 Both forms also support an optional `with` clause to specify arguments to pass to the dependency's package configuration (i.e., same as `args` in a `lake build -- <args...>` invocation). The elements of both the `from` and `with` clauses are proper terms so normal computation is supported within them (though parentheses made be required to disambiguate the syntax).
 
-## Writing and Running Lake Scripts
+## Writing and Running Scripts
 
 A configuration file can also contain a number of `scripts` declaration. A script is an arbitrary `(args : List String) → ScriptM UInt32` definition that can be run by `lake script run`. For example, given the following `lakefile.lean`: