chore: agent-driven modulize - #19
Closed
BoltonBailey wants to merge 3 commits into
Closed
Conversation
The module migration left `Repetition.Validation` and `Tseitin.Machine.Validation` with `public import`s only. Their `#eval`/`native_decide` regression guards run at elaboration time and need the imported instances/IR (`instDecidableEqΓ`, `fallbackEncoding`, `reductionTM`) accessible as `meta`, so add a parallel `meta import` alongside each `public import` (matching the SingleTape/Encoding validation files). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Owner
|
Oh nice, this is great. I was just working on the same thing but via a script written by Sol. |
Collaborator
Author
|
There is a "Modulize.lean" script in lean4 that is supposed to do it automatically, but it broke the build so I had to ask an agent to fix it. I'd like to try and rebuild with and without the changes to make sure they are actually helping. |
Owner
|
On my branch I saw a pretty significant >10% build time reduction from scratch |
Owner
|
Mine built one minute faster than yours, so I am going to merge it instead of this one. Apologies you did this work for naught! |
Collaborator
Author
|
Right on, I'll close this one. |
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
2 participants
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 ran Opus to convert the project to the module system using the modulize script