From aeb481b6be6764225da2f67ff7cdd68149f1854c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 11 Jun 2026 15:49:30 +1000 Subject: [PATCH] doc(lake): expand require...with documentation and -K propagation guidance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit expands the documentation around Lake's `require X from … with ` channel, which is currently mentioned in one sentence in `src/lake/README.md` and is the only sanctioned way for a workspace-root `-K name=value` flag to reach a dependency's `get_config?`. Three edits: * `src/lake/README.md` "Lean `require`" section: add a worked example showing how to forward a root `-K` value into a dependency, state that `-K` populates only the workspace-root package's `get_config?`, and reference https://github.com/leanprover/lean4/issues/14005 for the underspecified conflict semantics when two requires resolve to the same dep with different opts. * `src/lake/Lake/Config/Dependency.lean`: expand the `Dependency.opts` doc-string from one line to point at the DSL surface, the `get_config?` reader, and the README section. * `src/lake/Lake/CLI/Help.lean`: extend the `-K` long-form help blurb to note the workspace-root scope and to signpost `require … with` for cross-package forwarding. The current docs left at least one downstream consumer (https://github.com/leanprover/lp/issues/170 follow-up) iterating through several broken workarounds before discovering the existing feature. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.7 (1M context) --- src/lake/Lake/CLI/Help.lean | 1 + src/lake/Lake/Config/Dependency.lean | 8 +++++++- src/lake/README.md | 16 ++++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index c2a2aba4f6be..c53676a5434f 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/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) diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index 6a27f24ec791..002db7bc5246 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/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 `. + 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 diff --git a/src/lake/README.md b/src/lake/README.md index 2bc9c7832db6..aa85a77d17af 100644 --- a/src/lake/README.md +++ b/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.