Error Propagation with tryCatch

Stream: metaprogramming / tactics

[Francisco Lima]

I am making a automatic theorem solver, as such i need to loop over all available goals the best way I found yet has been to use a try catch with the getMainGoal but as shown in the following example it does not work, the catch pickups the error but the encompassing scope also receives the error for some reason, and only happens once as shown in the second case, so it only happens to the last goal

import Lean

open Lean Elab Meta Tactic

partial def loop (n := 0) : TacticM String :=
  withMainContext do
    try
      let goal ← getMainGoal
      admitGoal goal
      let rest ← loop (n + 1)
      return s!"sorry\n{rest}"
    catch e =>
      Lean.logInfo m!"Error: {e.toMessageData}"
      return ""

syntax (name := endSorry) "sorry?" : tactic

elab_rules : tactic
  | `(tactic| sorry?) => do
    let raw ← loop
    Lean.logInfo raw
    return

theorem test : True := by
  sorry?

theorem test2 : a → b → a ∧ b := by
  intro a
  intro b
  apply And.intro
  sorry?

[Aaron Liu]

Well if you logInfo the error obviously it's going to show up

[Aaron Liu]

what did you expect to happen

[Francisco Lima]

Aaron Liu said:

Well if you logInfo the error obviously it's going to show up

the log is there to see it happens, but if the line is commented out the problem still happens (was happening before I started logging the error)

[Aaron Liu]

what's the problem you are experiencing

[Francisco Lima]

partial def loop (n := 0) : TacticM String :=
  withMainContext do
    try
      let goal ← getMainGoal
      admitGoal goal
      let rest ← loop (n + 1)
      return s!"sorry\n{rest}"
    catch e =>
      -- Lean.logInfo m!"Error: {e.toMessageData}"
      return "error"

still gives the same 'error', that is, does not close with sorry the last goal

[Aaron Liu]

it seems to me that all the goals are closed though?

[Aaron Liu]

you can put done at the end of your by block and it doesn't complain

[Francisco Lima]

image.png

[Francisco Lima]

has the same error, does not close the last goal

[Aaron Liu]

interesting

[Aaron Liu]

if you return "" instead of return "error" I don't get a problem

[Francisco Lima]

In the actual code I do a return "" and the problem is still there

[Francisco Lima]

The content os the string, not doing some sort of throw should not matter for the final result

[Francisco Lima]

don't know if it matters but the problem doesn't seem to be connected with the try/catch since the following code has another error

import Lean

open Lean Elab Meta Tactic

partial def loop (n := 0) : TacticM String :=
  withMainContext do
    let goals ← getUnsolvedGoals
    match goals with
    | [] => return ""
    | goal::_ =>
      admitGoal goal
      let rest ← loop (n + 1)
      return s!"sorry\n{rest}"

syntax (name := endSorry) "sorry?" : tactic

elab_rules : tactic
  | `(tactic| sorry?) => do
    let raw ← loop
    Lean.logInfo raw
    return

theorem test : True := by
  sorry?
  done

theorem test2 : a → b → a ∧ b := by
  intro a
  intro b
  apply And.intro
  sorry?
  done

[Damiano Testa]

Shouldn't loop call itself at n - 1, rather than n + 1? Also, if n = 0, you should exit "manually".

[Francisco Lima]

n in this case does not matter for the recursion or not, I am using it to keep track here of how deep it has gone, in the actual code it increases as it goes along to keep track of variable naming (crude solution but it works)

[Francisco Lima]

with a bit more of logging I discovered it throws the error before the getMainGoal call (or at least it supresses the log)

import Lean

open Lean Elab Meta Tactic

partial def loop (n := 0) : TacticM String :=
  withMainContext do
    try
      Lean.logInfo s!"Pre {n}"
      let goal ← getMainGoal
      admitGoal goal
      let rest ← loop (n + 1)
      return s!"sorry {n}\n{rest}"
    catch e =>
      -- Lean.logInfo m!"Error: {e.toMessageData}"
      return s!"error {n}"

syntax (name := endSorry) "sorry?" : tactic

elab_rules : tactic
  | `(tactic| sorry?) => do
    let raw ← loop
    Lean.logInfo raw
    return

theorem test {a : Prop} : a → a := by
  intro a
  sorry?
-- Expect:
  -- sorry 0
  -- error 1
  done

theorem test2 : a → b → a ∧ b := by
  intro a
  intro b
  apply And.intro
  sorry?
-- Expect:
  -- sorry 0
  -- sorry 1
  -- error 2
  done