`grind`: stack overflow on a `match` given the cyclic hypothesis `as = a :: as`
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 45/100
- Issue type
- Bug
- Clarity
- Clearly specified
- Activity status
- Active
- Domain
- compilers
Research direction
The reproduction is a standalone Lean example using grind with a cyclic list equation and a match. Start by running the supplied example on the listed nightly version and inspect the grind implementation for stack overflow behavior on this case. Done means grind proves the goal or returns a regular failure without aborting the Lean process.
Written by the indexing model from the issue text.
Description
Prerequisites
- Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
- Reduce the issue to a minimal, self-contained, reproducible test case.
- Test your test case against the latest nightly release.
Description
grind causes a stack overflow and aborts the Lean process when a match expression is combined with a cyclic constructor equation, as = a :: as.
Steps to Reproduce
example (a : Nat) (as : List Nat) (h : as = a :: as) :
(match as with | 1 :: _ => 1 | _ => 2) > 0 := by
grind
Expected behavior: A proof or a regular grind failure.
Actual behavior: Stack overflow detected. Aborting. The process exits with code 134.
Versions
version 4.36.0-nightly-2026-10-12
Additional Information
try grind does not catch it.
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
- Dominant language
- Lean
- Stars
- 9.7k
- Forks
- 1.1k
- Avg merge
- 20h 22m
- Merged PRs (30d)
- 298
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 7 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 77/100
manuscript-lang/manuscript#1604 ·
Maintainers usually reply within 1 day
-
rust testing
Difficulty 2/5 1-3 hours Newbie friendliness 79/100
NekomyaDev/nudge#275 ·
Maintainers usually reply within 1 day
-
crash lld:COFF
Difficulty 2/5 1-3 hours Newbie friendliness 77/100
llvm/llvm-project#235970 · 1 comment ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 64/100
Maintainers usually reply within 1 day
-
bug scope:types
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
Maintainers usually reply within 1 day