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.

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

square braces can cause exponential time/memory consumption #1760

Closed
dwrensha opened this issue Oct 20, 2022 · 1 comment · Fixed by #1799
Closed

square braces can cause exponential time/memory consumption #1760

dwrensha opened this issue Oct 20, 2022 · 1 comment · Fixed by #1799

Comments

@dwrensha
Copy link
Contributor

The following input (found via fuzz testing) causes lean to take 140 seconds and consume 11.6 GB:

def foo : [[[[[[[[[[[[[

Adding more braces seems to make it exponentially worse.
My expectation is that, even if lean must perform exponential work in some situation, some kind of heartbeat will trigger before things get out of hand like this.

Lean (version 4.0.0-nightly-2022-10-18, commit faa612e7b79a, Release)
@leodemoura
Copy link
Member

Plan: add cache to parser, no choice when there are errors

@Kha Kha linked a pull request Nov 4, 2022 that will close this issue
@Kha Kha closed this as completed in #1799 Nov 11, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants