Add profiling and defeq guidance in style #764
Add profiling and defeq guidance in style #764bryangingechen merged 10 commits intoleanprover-community:lean4from
Conversation
Co-authored-by: Bryan Gin-ge Chen <[email protected]>
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Thanks a lot for writing this! I have a few grammar nits only.
Co-authored-by: Michael Rothgang <[email protected]>
| performance regressions. In particular, if the PR touches significant components | ||
| of the language like adding instances, adding `simp` lemmas, changing imports, | ||
| or creating new definitions, then authors should benchmark their changes | ||
| proactively. |
There was a problem hiding this comment.
This is very broadly formulated. Do we really want to require a benchmark for every PR containing one of these? I think that in practice, most added instances or simp lemmas are for (very) specialized declarations with specific discrimination keys, so no performance regression would be expected.
There was a problem hiding this comment.
Yes it is intentionally broad. The only real limit is benchmarking capacity. I don't see a way to draw it lower that it becomes effectively meaningless or convoluted. Suggestions welcome.
There was a problem hiding this comment.
How about:
"In particular, if the PR touches significant components of the library like adding generic instances, adding generic simp lemmas, changing imports or changing transparency levels of definitions, then authors should benchmark their changes proactively."
"generic" is of course vague, and we could maybe say something more precise in terms of discrimination keys, but I am not sure this would help.
There was a problem hiding this comment.
A lot of things here would become simple with better automation. Checking for weak keys is one. I would keep the import switching because that is a completely inscrutable ball of yarn right now.
If this is meant for contributors that know little, then the default should be simple to understand and execute.
Co-authored-by: Michael Rothgang <[email protected]>
templates/contribute/style.md
Outdated
| - `irreducible` definitions are never unfolded unless the user explicitly | ||
| requests it. |
There was a problem hiding this comment.
Should this explain (or point to documentation that explains) how to "request" unfolding of irreducible defs?
There was a problem hiding this comment.
Yes. Please add if you can. See the tactic file for documentation. I can't git right now
Co-authored-by: Robin Carlier <[email protected]>
Co-authored-by: Robin Carlier <[email protected]>
Co-authored-by: Robin Carlier <[email protected]>
Co-authored-by: Robin Carlier <[email protected]>
|
Thanks! This looks good to me (modulo the open suggestions). |
Co-authored-by: Bhavik Mehta <[email protected]>
Co-authored-by: Bhavik Mehta <[email protected]>
|
Shall we merge this as is? Maybe we can iterate on the advice about benchmarking in a future PR? |
7 participants
Contributor guidance around transparency and code design was requested. Note that some of these opinions are mine.