chore(vendor): refresh geb-mathlib and extend the module exclusions - #306
Merged
Merged
Conversation
Refresh `vendor/geb-mathlib` to upstream 7d54d29 (mathlib
`v4.35.0-rc2`) and re-anchor the back-port patch, which the
automated refresh rejected at `Prototypes/Typechecker.lean` after
upstream rewrote that module around `DecisionProblem`.
Exclude the new `Computability.Oitavem` tree, whose `Word` module
imports the excluded `BitTreeScanner.Encoding` and whose
`Machine.SpaceTime` imports a cslib `MultiTape` module absent from the
pin, together with its importers `BitStream.Oitavem`,
`Typechecker.Oitavem`, and `RoseTree.{Bits,Spine,Packed}`; and, under
`SizeBounded.Logspace`, `EliasTree` and the `WTree` modules that reach
the excluded `BitTree.Elias` machinery.
Extend the patch's categories 8, 9, 11, 14, 17, and 20 to the newly
ingested modules and add category 22 for mathlib's `PFunctor.Obj.mk`
(mathlib pull request 43056), documenting each in
`docs/geb-mathlib-backport-notes.md`.
Co-Authored-By: Claude Fable 5.1 <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.
Refresh
vendor/geb-mathlibto upstream 7d54d29 (mathlibv4.35.0-rc2) and re-anchor the back-port patch, which the automated refresh rejected atPrototypes/Typechecker.leanafter upstream rewrote that module aroundDecisionProblem.Exclude the new
Computability.Oitavemtree, whoseWordmodule imports the excludedBitTreeScanner.Encodingand whoseMachine.SpaceTimeimports a cslibMultiTapemodule absent from the pin, together with its importersBitStream.Oitavem,Typechecker.Oitavem, andRoseTree.{Bits,Spine,Packed}; and, underSizeBounded.Logspace,EliasTreeand theWTreemodules that reach the excludedBitTree.Eliasmachinery.Extend the patch's categories 8, 9, 11, 14, 17, and 20 to the newly ingested modules and add category 22 for mathlib's
PFunctor.Obj.mk(mathlib pull request 43056), documenting each indocs/geb-mathlib-backport-notes.md.