Macro vs. code action

Stream: lean4

[Joachim Breitner]

I tried to define a helper macro that uses #guard_msgs. It does elaborate corrrectly, but the code action doesn’t show up. I tried to alias that code, but that didn’t work. Any suggestions? The Elab.Tactic.GuardMsgs.guardMsgsCodeAction code does not seem to look specifically for the guardMsgsCmd syntax or so, I believe.

import Lean

open Lean Meta

/--
`/-- ... -/ #guard_sig ident` checks that the type of the identifier matches the type given in the
docstring.

This is a combination of `#guard_msgs` with `#check`, confgured to let trace messages pass through.
-/
macro (name := guardSigCmd)
  doc?:(docComment)? tk:"#guard_sig " i:ident : command =>
  `(command|$[$doc?]? #guard_msgs%$tk (pass trace, all) in #check $i)

open CodeAction in
@[builtin_command_code_action guardSigCmd]
def guardSigCodeAction : CommandCodeAction := Elab.Tactic.GuardMsgs.guardMsgsCodeAction

#guard_sig True

[Eric Wieser]

Is the code action attached to a particular piece of syntax, and only exercised if that syntax is not synthetic?

[Joachim Breitner]

Here is the code of that code action; I didn’t immediately see anything like that:
https://github.com/leanprover/lean4/blob/81b85203c90439fb7d7e0cec32130d62d8cb7a2e/src/Lean/Elab/GuardMsgs.lean#L180-L212

[Aaron Liu]

With #guard_msgs (pass trace, all) in #check True the infotree structure the code action is seeing is this (pardon the ugly representation):

node(commandInfo) [
  context (
    node(commandInfo) [
      (context (context (node(termInfo) []))),
      (context (context (node(completionInfo) [])))
    ]),
  node(customInfo) []
]

but with #guard_sig True you get

node(commandInfo) [
  node(macroExpansionInfo) [
    context (
      node(commandInfo) [
        context (
          node(commandInfo) [
            context (context (node(termInfo) [])),
            context (context (node(completionInfo) []))
          ]),
        node(customInfo) []
      ])
  ]
]

The custom info is the one containing the replacement and the one the code action is searching for, but it doesn't find it because it expects it to be a child of the top node, and the code action doesn't search recursively.

[Joachim Breitner]

TIL, thanks for the investigation!

[Kyle Miller]

Watch out that #guard_msgs is treated specially in elabCommandTopLevel: https://github.com/leanprover/lean4/blob/528fe0b0ed673accd37d986d80a7c49f876a3087/src/Lean/Elab/Command.lean#L610-L615

[Joachim Breitner]

Oh wey, I’ll park my attempts for now :-)