Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - perf: speed up some algebraic geometry with explicit universes #12494

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - perf: speed up some algebraic geometry with explicit universes #12494

wants to merge 1 commit into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

Open in Gitpod

@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-review The author would like community review of the PR label Apr 28, 2024
@erdOne
Copy link
Member

erdOne commented Apr 29, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 0a97bc5.
There were significant changes against commit b119a28:

  Benchmark                                  Metric         Change
  ================================================================
+ ~Mathlib.AlgebraicGeometry.AffineScheme    instructions   -13.0%
+ ~Mathlib.AlgebraicGeometry.FunctionField   instructions   -35.7%
+ ~Mathlib.AlgebraicGeometry.Properties      instructions   -49.5%

@erdOne
Copy link
Member

erdOne commented Apr 29, 2024

Very nice!
maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by erdOne.

@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 29, 2024
@Ruben-VandeVelde
perf: speed up some algebraic geometry with explicit universes (#12494)
888ba02
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title perf: speed up some algebraic geometry with explicit universes [Merged by Bors] - perf: speed up some algebraic geometry with explicit universes Apr 29, 2024
@mathlib-bors mathlib-bors bot closed this Apr 29, 2024
@mathlib-bors mathlib-bors bot deleted the speed-up-alg-geom branch April 29, 2024 12:56
@mattrobball mattrobball mentioned this pull request Apr 30, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@mattrobball
perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557)
ac46644 
Following #12469 and #12494, we add explicit universe levels in `AlgebraicGeometry.Spec` to speed up the file now and forestall greater slowdowns with the next version of Lean.
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@Ruben-VandeVelde @apnelson1
perf: speed up some algebraic geometry with explicit universes (#12494)
74fcd6c
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@mattrobball @apnelson1
perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557)
e6e9cb4 
Following #12469 and #12494, we add explicit universe levels in `AlgebraicGeometry.Spec` to speed up the file now and forestall greater slowdowns with the next version of Lean.
callesonne pushed a commit that referenced this pull request May 16, 2024
@Ruben-VandeVelde @callesonne
perf: speed up some algebraic geometry with explicit universes (#12494)
87f4e61
callesonne pushed a commit that referenced this pull request May 16, 2024
@mattrobball @callesonne
perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557)
4cae3b6 
Following #12469 and #12494, we add explicit universe levels in `AlgebraicGeometry.Spec` to speed up the file now and forestall greater slowdowns with the next version of Lean.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@Ruben-VandeVelde @erdOne @leanprover-bot @semorrison