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

perf: optimize isClassQuickConst? #4319

Closed
wants to merge 5 commits into from
Closed

perf: optimize isClassQuickConst? #4319

wants to merge 5 commits into from

Conversation

JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented May 31, 2024 •
edited
Loading

isClassQuick? is used as a quicker version of isClassExpensive?, returning .undef when it encounters an unfoldable constant. It checks this in the global transparency setting. But isClassExpensive? runs in the reducible transparency setting. I fixed it so that isClassQuick? does this check in the reducible setting as well.

In this refactor I've also deleted the private functions getConstTemp? and getDefInfoTemp, which aren't used anywhere else.

And I moved isClassImp? outside of the mutual block it was in.

This leads to a 0.1% reduction in build instructions for Mathlib

@JovanGerb JovanGerb marked this pull request as draft May 31, 2024 22:11
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 31, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4319
b6c8d10
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4319
379e3b2
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
100aef8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
0d76244
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels May 31, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented May 31, 2024 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
0f00ae8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
951f023
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
7bc314d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
1a423ec
@JovanGerb JovanGerb changed the title perf: optimize isClassQuickConst perf: optimize isClassQuickConst? Jun 1, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
569cf35
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
bf7664e
@JovanGerb JovanGerb marked this pull request as ready for review June 1, 2024 13:50
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
d5b5596
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 1, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4319
a8c2e6b
@JovanGerb
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Jun 2, 2024
@JovanGerb JovanGerb mentioned this pull request Jun 8, 2024
Closed
@Kha
Copy link
Member

Kha commented Aug 26, 2024

Closing as per reasoning in #4379

@Kha Kha closed this Aug 26, 2024
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
awaiting-review Waiting for someone to review the PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JovanGerb @leanprover-community-mathlib4-bot @Kha