Skip to content

chore: upstream ToExpr derive handler#221

Closed
kim-em wants to merge 9 commits intoleanprover-community:mainfrom
kim-em:Deriving_ToExpr
Closed

chore: upstream ToExpr derive handler#221
kim-em wants to merge 9 commits intoleanprover-community:mainfrom
kim-em:Deriving_ToExpr

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Aug 20, 2023 •
edited
Loading

Upstreaming Kyle's derive handler for ToExpr.

Co-authored-by: Kyle Miller kmill31415@gmail.com

@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Aug 20, 2023

Currently missing doc-strings on some definitions, as these files were added to Mathlib during the period we had the doc-string linter turned off. :-(

Hoping I can tempt @kmill to add these for me, otherwise I'll come up with something!

@kim-em kim-em added the WIP work in progress label Aug 20, 2023
@kim-em kim-em mentioned this pull request Aug 20, 2023
Merged
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Aug 20, 2023 •
edited
Loading

Ideally we'd upstream leanprover-community/mathlib4#5952, though I guess it's probably not too bad to rebase those changes onto an Std4 branch.

kmill
kmill reviewed Aug 20, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@kmill kmill left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here are some docstrings for each definition that try to explain what's going on.

For the PR summary, could you please change it to something like

Upstreaming Kyle's derive handler for ToExpr.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

I've noticed that if @kmill appears then every time someone merges the main branch in public downstream projects I get notified (!)

@kmill
Copy link
Copy Markdown
Contributor

kmill commented Aug 20, 2023

Ideally we'd upstream leanprover-community/mathlib4#5952, though I guess it's probably not too bad to rebase those changes onto an Std4 branch.

@eric-wieser I'd prefer if ToExpr were left alone and there be a completely new ToExprQ, mainly because ToExpr still exists in core. I know that you have this instance so deriving ToExprQ gives you a ToExpr instance, but still, I'd like to see ToExpr be deprecated in favor of ToExprQ rather than be replaced by it.

kim-em
kim-em commented Aug 20, 2023
View reviewed changes
@kim-em @kmill
Kyle's doc-strings
708c86f 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@kim-em kim-em added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed WIP work in progress labels Aug 20, 2023
kmill
kmill reviewed Aug 20, 2023
View reviewed changes
@kim-em kim-em requested a review from digama0 August 20, 2023 23:12
@eric-wieser eric-wieser mentioned this pull request Aug 21, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Aug 21, 2023
@eric-wieser @kmill
doc: add missing docstrings around ToExpr (#6699)
425f4ca 
These are extracted from leanprover-community/batteries#221

Co-authored-by: Kyle Miller <kmill31415@gmail.com>



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@kim-em kim-em added no-action There is no need to act on this and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Aug 22, 2023
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Aug 22, 2023

We've decided not to do this for now. The long term plan is to migrate quote4 into std4 and then implement the ToExprQ derive handler instead.

(For what it's worth, I think "perfect is the enemy of good" applies here...)

@kim-em kim-em closed this Aug 22, 2023
@alexkeizer alexkeizer mentioned this pull request Oct 31, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kmill kmill kmill left review comments

@digama0 digama0 Awaiting requested review from digama0

Assignees

No one assigned

Labels

no-action There is no need to act on this

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @eric-wieser @kmill