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: add two benchmarks that are slow to parse or elaborate #5656

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

test: add two benchmarks that are slow to parse or elaborate #5656

wants to merge 2 commits into from
+3,552 −0

Conversation

atomb
Copy link

@atomb atomb commented Oct 8, 2024

Add two example Lean files that include unusually large definitions and take a long time to parse or elaborate.

It may be that it's difficult to process them more efficiently, but perhaps someone will discover a way to improve them if they're in the benchmark suite. Improved performance on these benchmarks will likely make program analysis and verification within Lean more feasible.

@atomb
Two benchmarks that are slow to parse or elaborate
93f8e51 
This commit includes two example Lean programs that include unusually
large definitions and take a long time to parse or elaborate. It may be
that it's difficult to process them more efficiently, but perhaps
someone will discover a way to improve them if they're in the benchmark
suite.
@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 8, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 8, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fdd5aec172c48f1aac19e90b68775f4cd344d429 --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-08 22:35:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fdd5aec172c48f1aac19e90b68775f4cd344d429 --onto d10d41bc07942ca6d8f3081a637045321db15c5a. (2024-10-11 23:37:28)

@atomb
Copy link
Author

atomb commented Oct 11, 2024

!bench

@atomb atomb marked this pull request as ready for review October 11, 2024 23:45
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
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.
2 participants
@atomb @leanprover-community-bot