Stack overflow in `refine'`

Stream: lean4

[Eric Wieser]

This crashes the lean server:

example : False := by
  refine' absurd (congrArg (·.1) sorry) _

[Kim Morrison]

Seems like a good one for a bug report!

[Eric Wieser]

lean4#4144 (edited)

[Eric Wieser]

The bug template feels extremely verbose for what is ultimately captured by a two line repro and a version number, but I guess all that matters really is whether the FRO is happy reading the verbosity

[Utensil Song]

I guess you mean lean4#4144

[Eric Wieser]

Now fixed, thanks Leo :)

rss-bot said:

fix: missing occurs-check at delayed assignment (lean4#4217)

closes lean4#4144

Authored-by: leodemoura (commit)

Though now my stack pointer is beyond another castle: lean#4219