-
Notifications
You must be signed in to change notification settings - Fork 234
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
[Merged by Bors] - perf (AlgebraicGeometry.Properties): Speed up one declaration #9035
Conversation
!bench |
Here are the benchmark results for commit bc6e97d. Benchmark Metric Change
=============================================================
+ ~Mathlib.AlgebraicGeometry.Properties instructions -34.7% |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Impressive!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
If CI passes, please remove the label awaiting-CI
and merge this yourself, by adding a comment bors r+
.
bors d+
✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with |
!bench |
Here are the benchmark results for commit a5cf391. Benchmark Metric Change
=============================================================
+ ~Mathlib.AlgebraicGeometry.Properties instructions -35.2% |
bors merge |
This speeds up on declaration by breaking up a defeq check into a single task. Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
This speeds up on declaration by breaking up a defeq check into a single task. Co-authored-by: Johan Commelin <johan@commelin.net>
This speeds up on declaration by breaking up a defeq check into a single task.