max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: add checkSystem and withIncRecDepth to withAutoBoundImplicit (#4128)

Browse source 
Fix stack overflow crash.

Closes #4117

The fix can be improved: we could try to avoid creating hundreds of auto
implicits before failing.
This commit is contained in:
Leonardo de Moura 2024-05-10 23:55:26 +02:00 • committed by GitHub
parent 6c6b56e7fc
commit a6d186a81d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Term.lean
View file

@ -1523,7 +1523,8 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
let flag := autoImplicit.get (← getOptions)
if flag then
withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) do
let rec loop (s : SavedState) : TermElabM α := do
let rec loop (s : SavedState) : TermElabM α := withIncRecDepth do
checkSystem "auto-implicit"
try
k
catch

1
tests/lean/4117.lean Normal file
View file

@ -0,0 +1 @@
structure D:=(t:A)(c N:={s with} 0

1
tests/lean/4117.lean.expected.out Normal file
View file

@ -0,0 +1 @@
4117.lean:2:0: error: unexpected end of input; expected ')'

4
tests/lean/run/simpDiag.lean
View file

@ -35,8 +35,8 @@ info: [simp] used theorems (max: 1201, num: 3):
⏎
Nat.reduceAdd (builtin simproc) ↦ 771
⏎
ack.eq_1 ↦ 768[simp] tried theorems (max: 1974, num: 2):
ack.eq_3 ↦ 1974, succeeded: 1201
ack.eq_1 ↦ 768[simp] tried theorems (max: 1973, num: 2):
ack.eq_3 ↦ 1973, succeeded: 1201
⏎
ack.eq_1 ↦ 768, succeeded: 768use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
---