We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Please put an X between the brackets as you perform the following steps:
The following malformed input causes Lean to crash with a stack overflow:
structure D:=(t:A)(c N:={s with} 0
Here is the repeating part of the call stack from gdb:
#26501 0x00007ffff540023d in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg (x_1=0x7ffff1365938, x_2=0x7ffff136acf8, x_3=0x7ffff120eae0, x_4=0x7ffff12feae8, x_5=0x7ffff1d489b8, x_6=0x7ffff12fec08, x_7=0x7ffff1258858, x_8=0x7ffff12fe8a8, x_9=0x1) at ../build/debug/stage1/lib/temp/Lean/Elab/Term.c:45232 #26502 0x00007ffff53ff851 in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg___lambda__1 (x_1=0x7ffff1365938, x_2=0x7ffff136ada0, x_3=0x7ffff120eae0, x_4=0x7ffff12feae8, x_5=0x7ffff1d489b8, x_6=0x7ffff12fec08, x_7=0x7ffff1258858, x_8=0x7ffff12fe8a8, x_9=0x1) at ../build/debug/stage1/lib/temp/Lean/Elab/Term.c:45086 #26503 0x00007ffff7219009 in lean::lean_apply_8 (f=0x7ffff1366cb8, a1=0x7ffff136ada0, a2=0x7ffff120eae0, a3=0x7ffff12feae8, a4=0x7ffff1d489b8, a5=0x7ffff12fec08, a6=0x7ffff1258858, a7=0x7ffff12fe8a8, a8=0x1) at /home/markus/code/lean4/src/runtime/apply.cpp:510 #26504 0x00007ffff5383e17 in l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__1___rarg___lambda__1 (x_1=0x7ffff1366cb8, x_2=0x7ffff120eae0, x_3=0x7ffff12feae8, x_4=0x7ffff136ada0, x_5=0x7ffff1d489b8, x_6=0x7ffff12fec08, x_7=0x7ffff1258858, x_8=0x7ffff12fe8a8, x_9=0x1) at ../build/debug/stage1/lib/temp/Lean/Elab/Term.c:7263 #26505 0x00007ffff72153a3 in lean::lean_apply_6 (f=0x7ffff1371ce8, a1=0x7ffff136ada0, a2=0x7ffff1d489b8, a3=0x7ffff12fec08, a4=0x7ffff1258858, a5=0x7ffff12fe8a8, a6=0x1) at /home/markus/code/lean4/src/runtime/apply.cpp:406 #26506 0x00007ffff6278dab in l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___rarg (x_1=0x7ffff136ada0, x_2=0x7ffff136af98, x_3=0x7ffff1371ce8, x_4=0x7ffff1d489b8, x_5=0x7ffff12fec08, x_6=0x7ffff1258858, x_7=0x7ffff12fe8a8, x_8=0x1) at ../build/debug/stage1/lib/temp/Lean/Meta/Basic.c:23052 #26507 0x00007ffff6279147 in l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg (x_1=0x7ffff1362238, x_2=1 '\001', x_3=0x7ffff136af98, x_4=0x7ffff1371ce8, x_5=0 '\000', x_6=0x7ffff1d489b8, x_7=0x7ffff12fec08, x_8=0x7ffff1258858, x_9=0x7ffff12fe8a8, x_10=0x1) at ../build/debug/stage1/lib/temp/Lean/Meta/Basic.c:23128 #26508 0x00007ffff5383ed8 in l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__1___rarg (x_1=0x7ffff1362238, x_2=1 '\001', x_3=0x7ffff136af98, x_4=0x7ffff1366cb8, x_5=0 '\000', x_6=0x7ffff120eae0, x_7=0x7ffff12feae8, x_8=0x7ffff1d489b8, x_9=0x7ffff12fec08, x_10=0x7ffff1258858, x_11=0x7ffff12fe8a8, x_12=0x1) at ../build/debug/stage1/lib/temp/Lean/Elab/Term.c:7275 #26509 0x00007ffff540023d in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg (x_1=0x7ffff1365938, x_2=0x7ffff136af98, x_3=0x7ffff120eae0, x_4=0x7ffff12feae8, x_5=0x7ffff1d489b8, x_6=0x7ffff12fec08, x_7=0x7ffff1258858, x_8=0x7ffff12fe8a8, x_9=0x1) at ../build/debug/stage1/lib/temp/Lean/Elab/Term.c:45232
Discovered through fuzzing, so probably low priority.
Expected behavior: Lean exits gracefully with an error message.
Actual behavior: Stack overflow detected. Aborting.
Stack overflow detected. Aborting.
Lean (version 4.9.0, commit fe7b96d, DEBUG)
Linux markus-laptop 6.8.9-arch1-2 #1 SMP PREEMPT_DYNAMIC Tue, 07 May 2024 21:35:54 +0000 x86_64 GNU/Linux
[Additional information, configuration or data that might be necessary to reproduce the issue]
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered:
fix: add checkSystem and withIncRecDepth to withAutoBoundImplicit
checkSystem
withIncRecDepth
withAutoBoundImplicit
5ac0662
Fix stack overflow crash. Closes #4117 The fix can be improved: we could try to avoid creating hundreds of auto implicits before failing.
fix: add checkSystem and withIncRecDepth to `withAutoBoundImplici…
a6d186a
…t` (#4128) Fix stack overflow crash. Closes #4117 The fix can be improved: we could try to avoid creating hundreds of auto implicits before failing.
Successfully merging a pull request may close this issue.
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The following malformed input causes Lean to crash with a stack overflow:
Here is the repeating part of the call stack from gdb:
Context
Discovered through fuzzing, so probably low priority.
Steps to Reproduce
Expected behavior: Lean exits gracefully with an error message.
Actual behavior:
Stack overflow detected. Aborting.
Versions
Lean (version 4.9.0, commit fe7b96d, DEBUG)
Linux markus-laptop 6.8.9-arch1-2 #1 SMP PREEMPT_DYNAMIC Tue, 07 May 2024 21:35:54 +0000 x86_64 GNU/Linux
Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: