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

test: big_omega benchmark #5817

Merged
merged 1 commit into from
Oct 24, 2024
Merged

test: big_omega benchmark #5817

merged 1 commit into from
Oct 24, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Oct 23, 2024

Extracted from #5614

@Kha
Copy link
Member Author

Kha commented Oct 23, 2024

@bollu Do you agree to this test being added to the repo?

@Kha Kha force-pushed the push-ruvkruxttkos branch from 8159762 to faa768c Compare October 23, 2024 08:51
@Kha Kha force-pushed the push-ruvkruxttkos branch from faa768c to c9244da Compare October 23, 2024 08:54
@Kha
Copy link
Member Author

Kha commented Oct 23, 2024

!bench

@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 23, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 45b1b367ca1424f5a3c5fdef84bbeee284998216 --onto 66dbad911eaaec4cd512662bd5cc67a2a16d2484. (2024-10-23 09:14:47)

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit c9244da.
There were significant changes against commit 45b1b36:

  Benchmark       Metric       Change
  =============================================
+ bv_decide_mul   wall-clock    -3.0% (-51.9 σ)

@bollu
Copy link
Contributor

bollu commented Oct 23, 2024

LGTM, thank you for checking the testcase in @Kha !

tobiasgrosser
tobiasgrosser approved these changes Oct 23, 2024
View reviewed changes
Copy link
Contributor

@tobiasgrosser tobiasgrosser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you, @Kha.

@Kha Kha added this pull request to the merge queue Oct 24, 2024
Merged via the queue into leanprover:master with commit 9157c1f Oct 24, 2024
13 checks passed
@Kha Kha deleted the push-ruvkruxttkos branch October 24, 2024 08:26
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Oct 27, 2024
@Kha @tobiasgrosser
test: big_omega benchmark (leanprover#5817)
bbf206e 
Extracted from leanprover#5614
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bollu bollu bollu approved these changes

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

Assignees
No one assigned
Labels
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
@Kha @leanprover-community-bot @leanprover-bot @bollu @tobiasgrosser