doc(lake): expand require ... with <opts> documentation and -K propagation guidance#14006
Open
kim-em wants to merge 1 commit into
Open
doc(lake): expand require ... with <opts> documentation and -K propagation guidance#14006kim-em wants to merge 1 commit into
require ... with <opts> documentation and -K propagation guidance#14006kim-em wants to merge 1 commit into
Conversation
…ion guidance This commit expands the documentation around Lake's `require X from … with <options>` 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 leanprover#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 (leanprover/lp#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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR expands the documentation around Lake's
require X from … with <options>channel, which is currently mentioned in one sentence insrc/lake/README.mdand is the only sanctioned way for a workspace-root-K name=valueflag to reach a dependency'sget_config?. Three edits:src/lake/README.md— expand the "Leanrequire" section with a worked example that forwards a root-K leanLibDir=…value into a dependency by computing theNameMap Stringfromget_config?at the require site. State explicitly that-Kpopulates only the root package'sget_config?and thatrequire … withis the documented per-edge forwarding channel. Briefly note the underspecified conflict semantics when tworequires resolve to the same dep with different opts.src/lake/Lake/Config/Dependency.lean— expand theDependency.optsdoc-string from a single line to point at the DSL surface (require … with), the reader (get_config?), and the README section.src/lake/Lake/CLI/Help.lean— extend the-Klong-form help blurb to note that the flag's scope is the workspace-root package and to signpostrequire … withfor cross-package forwarding.The current docs left at least one downstream consumer (leanprover/lp#170 follow-up) iterating through several broken workarounds (env-var fallbacks via
@[init], CI-side hacks copying the toolchain archive over system paths) before discovering the existing feature.Companion design issue for the conflict-semantics piece: #14005.
🤖 Prepared with Claude Code