Code action for `success_if_fails_with_msg`

Stream: mathlib4

[Patrick Massot]

For people looking for a nice meta-project in order to kill time until next year, it seems https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/SuccessIfFailWithMsg.lean misses a code action proposing to fix the message when the target tactic fails but with an unexpected message. This would align nicely with what guard_msgs is doing for instance.

[Patrick Massot]

For inspiration, the corresponding code for guard_msgs is at https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/GuardMsgs.lean#L177-L210

[Edward van de Meent]

Lean.Meta.Tactic.TryThis.addSuggestion seems relevant too

[Patrick Massot]

I think a code action is enough here, although I would be happy with a try this widget if you fancy doing that.

[Edward van de Meent]

right, these are different things :idea:

[Patrick Massot]

One is contained in the other: addSuggestion does create a code action in addition to the widget.

[Edward van de Meent]

doing this is a bit troublesome: it seems to require either nailing down docs#Mathlib.Tactic.successIfFailWithMessage to some meta monad (i'm guessing TacticM), or parsing an error message to recover the concrete message, or messing about with custom infotree nodes?

[Edward van de Meent]

option 2 is definitely bad, option 1 might cause some breakage but is doable i think, and i'm not very knowledgable w/r/t dealing with infotree manipulation, so i'm wary of myself doing option 3...

[Joachim Breitner]

Its in the tactic namespace, so option 1 seems reasonable?

[Edward van de Meent]

#20378 implements option 1

[Edward van de Meent]

(now with less pinning down, more MonadLiftT)

[Patrick Massot]

Thanks!

[Edward van de Meent]

It has landed in master, for those interested

[Julian Berman]

If requests for additional code actions are tempting, one for extract_goal (which adds the lemma above the current declaration) seems like it also might be nice to have as well. CC @Bhavik Mehta

[Johan Commelin]

And it should replace the extract_goal call with apply extracted_lemma.

[Johan Commelin]

Also, extract_goal doesn't make use of the existing variables and it has a lot of [_inst_37 : SomeClass X Y Z] assumptions that shouldn't have the _isnt_37 : .

[Kim Morrison]

I noticed actually that LeanAide's autoformalized statements also have lots of the unwanted _inst_37s. (@Siddhartha Gadgil). Perhaps there is a common fix.

[Siddhartha Gadgil]

LeanAide uses (at least most of the time) the Lean commands delab, ppExpr and ppTerm to generate the strings shown. Perhaps one of these is the source of the inst_37s.