all_goals + apply elaboration = lost errors

Stream: metaprogramming / tactics

[Claudio Sacerdoti Coen]

Does anyone know a workaround for the following issue, until the bug is fixed? It pops up in a set of tactics I implemented for didactics and it is currently affecting my class badly

https://github.com/leanprover/lean4/issues/4888

Basically, if all_goals is fed a tactic that uses a term that fails to typecheck, the error is completely swallowed and ignored
and the tactic succeds.

theorem bug: True := by
 all_goals exact Nat.succ True   -- Nat.succ True is not well typed, but the tactic succeeds
 trivial

[Damiano Testa]

This is very interesting! I wonder whether it is related to the fact that logStuff does not get reliably logged. The error that the tactic is trying to generate is

here type mismatch
  (sorryAx Nat true).succ
has type
  Nat : Type
but is expected to have type
  True : Prop

I think, but logException of that does nothing.

[Damiano Testa]

See docs#Lean.Elab.Tactic.evalAllGoals, this line.

[Damiano Testa]

It looks like the code goes there, but logException does not do its thing.

[Damiano Testa]

In fact, replacing that line with logInfo ex.toMessageData shows the "correct" error message.

[Damiano Testa]

This may be a minimization of sorts. It also highlights a problem that I have observed elsewhere that logInfo and friends can be really slow if you do not explicitly add a type ascription.

[Damiano Testa]

import Lean.Elab.Command

open Lean Elab Tactic

elab "all_goals1 " stx:tactic : tactic => do
  let mvarIds ← getGoals
  for _mvarId in mvarIds do
      try
        evalTactic stx.raw
      catch ex =>
        if (← read).recover then
          dbg_trace "I am printed"
          (logException ex : TacticM Unit) -- this speeds up a lot!

theorem bug: True := by
 all_goals1 exact Nat.succ True   -- Nat.succ True is not well typed, but the tactic succeeds
 trivial

[Damiano Testa]

Actually, this is enough for the reported issue:

elab "all_goals1 " stx:tactic : tactic => do
  try
    evalTactic stx
  catch ex =>
    dbg_trace "I am printed"
    logException ex

[Claudio Sacerdoti Coen]

Wrapping calls to all_goals (and to all Lean tactics implemented on top of it, like <;>) with either withoutRecover or withouthErrToSorry yields the behaviour I would expect. At this point I am quite confused though: is my reported issue valid or are tactic invocations like "all_goals exact Nat.succ True" or " tac <.> exact Nat.succ True" really NOT supposed to fail?

[Damiano Testa]

My expectation is that they should fail. The logException step makes me suspect that this is indeed the intended (and unachieved) behaviour as well.

[Kim Morrison]

@Claudio Sacerdoti Coen would you be able to open an issue on the lean4 repository reporting this?

[Yaël Dillies]

Is it not lean4#4888 ?

[Claudio Sacerdoti Coen]

Yes, it is. I added there a link to this chat as well

[Damiano Testa]

I suspect that this is an even further minimization:

import Lean.Elab.Command

open Lean Elab Tactic

elab "done_or_fail" : tactic => do
  try
    evalTactic (← `(tactic| done))
  catch ex =>
    logInfo ex.toMessageData
    logException ex

/-- info: internal exception #4 -/
#guard_msgs in
example : 0 = 0 := by
  done_or_fail
  rfl