Bump extractor workspaces for doc-gen4 SQLite support#79
Merged
Conversation
Updates lakefile.lean, lean-toolchain, and lake-manifest.json across the cslib, flt, formal-conjectures, mathlib, and physlean extractor workspaces to the latest toolchain (v4.30.0-rc2) and reorders the doc-gen4 require before the main package dependency to avoid transitive conflicts. Four workspaces pin doc-gen4 @ "main" for access to the new SQLite api-docs.db output. PhysLean remains pinned to v4.29.0 to match its Lean toolchain. PhysExtract.lean is updated to import Physlib and QuantumInfo, the post-rename library targets. Manifests regenerated via `lake update` in each workspace.
This was referenced Apr 19, 2026
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.
Summary
lean/{cslib,flt,formal-conjectures,mathlib,physlean}workspaces to Leanv4.30.0-rc2and regenerateslake-manifest.jsonin each vialake update.require «doc-gen4»before the main package dependency in eachlakefile.leanso Lake resolves transitive deps correctly (otherwise packages likeplausiblecan conflict).doc-gen4 @ "main"to pick up the new SQLiteapi-docs.dboutput. PhysLean stays pinned tov4.29.0because its toolchain is older; it also updatesPhysExtract.leanto import the renamedPhyslib/QuantumInfolibrary targets.