8000 perf: `infer_app` with `infer_only := false` (WIP) by leodemoura · Pull Request #2781 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

perf: infer_app with infer_only := false (WIP) #2781

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
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

perf: infer_app with infer_only := false (WIP) #2781

wants to merge 1 commit into from

Conversation

leodemoura
Copy link
Member

No description provided.

8000

@leodemoura leodemoura marked this pull request as draft October 29, 2023 02:21
@leodemoura
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d1dd4b9.
There were significant changes against commit f76a17b:

  Benchmark                  Metric   Change
  ====================================================
+ tests/bench/ interpreted   maxrss    -1.1% (-11.5 σ)

@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 Oct 29, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 29, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2781
fb5cafb
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 29, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator
leanprover-community-mathlib4-bot commented Oct 29, 2023 •
edited
Loading

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 29, 2023
This was referenced Oct 29, 2023
Closed
Draft
@kim-em
Copy link
Collaborator
kim-em commented Oct 30, 2023

@leodemoura here is the comparison between Mathlib runs:
http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash1=1ca67b1a4b326c4224bb25a792b22c304c83b597&hash2=bb1b2648e3674b537c07efac0d4e66162fb7dab5

Unfortunately it doesn't look good: a 2.4% wallclock regression.

@leodemoura
Copy link
Member Author

Unfortunately it doesn't look good: a 2.4% wallclock regression.

I took a look at the results. This commit affects "type checking" time, and it seems it went down.

image

This commit minimizes the number of instantiate operations, but it is not caching the type for partial applications. That is, if we have f a b and f a c. The previous approach caches the result for f a, but this commit skips it. That being said, it seems "type checking" time still went down. It is unclear to me how the "wall clock" time went up.

@Kha
Copy link
Member
Kha commented Nov 6, 2023

Either of these might or might not be noise, the instruction count suggests that there is probably no impact overall. We should try again on top of leanprover-community/mathlib4#8224

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
builds-mathlib CI has verified that Mathlib builds against this PR 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.
5 participants
@leodemoura @leanprover-bot @leanprover-community-mathlib4-bot @kim-em @Kha
0