feat: require imported root dependencies in generated workspaces - #8
Merged
Merged
Conversation
A problem statement may import a package other than Mathlib, for example TauCeti for the classification of finite simple groups. Its generated workspace then needs a `[[require]]` for that package, but the root lakefile also requires tooling packages (Cli, lean-eval-generator) that must never leak into a workspace. `loadRootDependencies` now reads the mathlib pin together with every other git-pinned root require, and each workspace lakefile requires those whose name is the first component of a module the workspace imports. Extra requires come first, in root lakefile order, and Mathlib last: Lake resolves shared transitive dependencies from the later require, so Mathlib must win. Workspaces that import only Mathlib render exactly as before, and a bare `DependencySpec` still coerces to the new `RootDependencies`, so existing callers of `renderWorkspace` keep compiling. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
feat/extra-workspace-dependencies
branch
from
September 25, 2026 12:43
cf315d2 to
eabb0fc
Compare
The JSON request gains an optional `dependencies` array of extra git pins, so the CLI path can render workspaces for problems that import packages other than Mathlib; omitting it keeps every existing version 1 request's meaning and output. Root requires other than mathlib are now only checked when a problem selects them, so tooling requires may use any Lake syntax, and a selected require using fields a workspace would not reproduce (`subDir`, `scope`, table-valued `git`, ...) is a clear error rather than being silently dropped. Require values are TOML-escaped, which leaves ordinary names, URLs and revisions unchanged. The README documents the selection rule and its limitation for packages whose library root differs from their package name. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Generation now refuses a root mathlib require carrying fields such as `subDir` or `scope`, which the emitted `[[require]]` would silently drop, just as it does for a selected extra require; `loadRootMathlibDependency` keeps ignoring them as before. CLI requests must use the same problem id rule as manifests, and the workspace name is emitted as an escaped TOML string. The README tells consumers to install the root lake-manifest.json into a generated workspace, so the pruned requires resolve to the same package revisions as the root workspace. Co-Authored-By: Claude Opus 5.5 (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 lets a generated workspace require packages other than Mathlib. A workspace's
lakefile.tomlgains a[[require]]for every candidate package whose name is the first component of a module the problem imports (after following repo-local imports), emitted in root order before Mathlib, which stays last so that Lake resolves shared transitive dependencies (batteries, aesop, Qq, ...) from Mathlib's pins. Library callers get the candidates from the root lakefile throughloadRootDependencies; CLI requests pass them in a new optionaldependenciesarray, and omitting it keeps every existing version 1 request's output unchanged. Tooling requires such asCliandlean-eval-generatorare never selected because no problem imports them, and non-mathlib requires are only validated once selected: a selected require must be a plain git require with non-emptygitandrev, and fields a workspace would not reproduce (subDir,scope, table-valuedgit, ...) are an error. Require values are TOML-escaped. Workspaces that import only Mathlib render byte-identically to before.renderWorkspacenow takes aRootDependencies, a bareDependencySpeccoerces to it, andloadRootMathlibDependencyis kept. This is needed so lean-eval can add a problem importing TauCeti, for the statement of the classification of finite simple groups.🤖 Prepared with Claude Code