doc(lake): expand require ... with <opts> documentation and -K propagation guidance

src/lake/Lake/CLI/Help.lean

@@ -49,6 +49,7 @@ BASIC OPTIONS:
   --dir, -d=file        use the package configuration in a specific directory
   --file, -f=file       use a specific file for the package configuration
   -K key[=value]        set the configuration file option named key
+                        (workspace-root only; forward to a dep with `require … with`)
   --old                 only rebuild modified modules (ignore transitive deps)
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update              update dependencies on load (e.g., before a build)

src/lake/Lake/Config/Dependency.lean

@@ -103,7 +103,13 @@ public structure Dependency where
   -/
   src?  : Option DependencySrc
   /--
-  Arguments to pass to the dependency's package configuration.
+  Arguments to pass to the dependency's package configuration. Set via the
+  `with` clause of a `require` declaration: `require X from … with <opts>`.
+  These are exposed inside the dependency's lakefile through `get_config?`,
+  the same surface as workspace-root `-K name=value` flags. `-K` flags
+  themselves only reach the workspace-root package's `get_config?`, so the
+  `with` clause is the channel for forwarding a root option to a specific
+  dependency; see the "Lean `require`" section of `src/lake/README.md`.
   -/
   opts : NameMap String
   deriving Inhabited, TypeName

src/lake/README.md

@@ -461,6 +461,22 @@ The `scope` is used to disambiguate between packages in the registry with the sa
 
 The `with` clause specifies a `NameMap String` of Lake options used to configure the dependency. This is equivalent to passing `-K` options to the dependency on the command line.
 
+A `-K name=value` flag on `lake build` only populates the **workspace-root** package's options, so a transitive dependency's `get_config? name` returns `none` even when the root was invoked with the flag set. The `with` clause is the documented per-edge channel for forwarding a workspace-root option to a specific dependency:
+
+```lean
+-- In the workspace-root lakefile. Forward our own `-KleanLibDir=...` value
+-- into a dependency whose own lakefile reads `get_config? leanLibDir`.
+def forwardedDepOpts : Lean.NameMap String :=
+  match get_config? leanLibDir with
+  | some d => Lean.NameMap.empty.insert `leanLibDir d
+  | none => Lean.NameMap.empty
+
+require SoplexFFI from git "https://github.com/leanprover/soplex-ffi" @ "..." with
+  forwardedDepOpts
+```
+
+If two `require`s in the workspace resolve to the same dependency `X` with different `opts` maps, one configuration wins for the workspace-wide `X` instance and the other is silently discarded; the precedence is currently underspecified. See https://github.com/leanprover/lean4/issues/14005.
+
 ### Supported Sources
 
 Lake supports the following types of dependencies as sources in a `from` clause.