-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
perf: deduplicate ← instantiateMVars (← inferType mvar)
in TC search
#4379
Conversation
!bench |
Here are the benchmark results for commit 1c0787e. |
Mathlib CI status (docs):
|
Dear @JovanGerb , We have noticed that you have been submitting many PRs, and it is great to see your enthusiasm. Thank you for filing issues and proposing fixes. We are always looking for new contributors. Best wishes, |
Dear @leodemoura and @Kha, Thank you for your kind message. I can undestand that making significant changes to core Lean requires trust and careful consideration. And the benefits of the change need to outweigh the cost of worsened maintanability. Best whishes, |
Thanks for your understanding. Maintainability of the code is one important aspect, but reviewing work is another one I would like to highlight. For a critical module like TC synth, there are basically no uncontroversial changes because every change must be reviewed with the full context of the module in mind, which usually means there is at most one potential reviewer and that person likely does not have that context ready in their mind right now.
So even positive but insignificant changes to such modules can be distractive and will be considered very low priority. For significant changes, as Leo wrote one should start at less critical places. |
Closes #4284