Nested try catch

Stream: lean4

[Patrick Massot]

Could we have a better error message in

import Lean

elab "foo" : tactic => do
  try
    evalTactic (← `(tactic|skip))
    try
      evalTactic (← `(tactic|skip))
    catch _ =>
      throwError "One"
  catch _ => do
     throwError "Two"

[Patrick Massot]

Here Lean complains on the first try that invalid `try`, it must have a `catch` or `finally` , which seems pretty unfair to me.

[Patrick Massot]

To be honest I don’t even understand why this is incorrect code.

[Sebastian Ullrich]

It's likely associating both catch to the first try, that would be a parser bug

[Yaël Dillies]

I encountered this recently too. I had to resort to doing try { try ... catch ... } catch .... I agree it is annoying.

[Robin Arnez]

This is lean4#8220. I have a fix but it's unfortunately a bit more complicated than I would've hoped it to be. And for anyone wondering, the complicated cases are:

if ... then
  ...
else try
  ...
catch _ =>
  ...

and

let _ ← try
  ...
catch _ =>
  ...

[Patrick Massot]

Thanks! Yaël, could you please upvote that bug report?