hello world tactic

Stream: lean4

[David Renshaw]

I want to write a tactic that logs a "hello world" message and does nothing else.
Here's my current attempt:

syntax "helloworld" : tactic

@[tactic helloworld] def elabHelloWorld : Lean.Elab.Tactic.Tactic
| _ => do Lean.Elab.logInfo "Hello, world!"
          pure ()

theorem foo {p : Prop} (h : p) : p :=
  by helloworld
     exact h

This fails with:

128:25:
invalid syntax node kind 'helloworld'
133:5:
tactic 'tacticHelloworld' has not been implemented

What can I change to make it work?

[David Renshaw]

Here's another attempt:

syntax "helloworld" : tactic

@[tactic ident] def elabHelloWorld : Lean.Elab.Tactic.Tactic
| `(tactic| helloworld) => do Lean.Elab.logInfo "Hello, world!"
                              pure ()
| _ => Lean.Elab.throwUnsupportedSyntax

theorem foo {p : Prop} (h : p): p :=
  by helloworld
     exact h

That still fails with "tactic 'tacticHelloworld' has not been implemented".

[Mac]

Try this:

syntax (name := «helloworld») "helloworld" : tactic

@[tactic «helloworld»] def elabHelloWorld : Lean.Elab.Tactic.Tactic
| _ => do Lean.Elab.logInfo "Hello, world!"
          pure ()

theorem foo {p : Prop} (h : p) : p :=
  by helloworld
     exact h

[David Renshaw]

nice!

[David Renshaw]

that works

[Mac]

The problem is that the name of your new tactic syntax needs to be feed into the @[tactic] annotation. You can do this either by giving it explicit name (like my example above) or by using the auto-generated name (i.e., tacticHelloworld).

[David Renshaw]

it looks like the guillemets might not actually be necessary?

[Wojciech Nawrocki]

^ As Mac is saying, the syntax node kind is tacticHelloworld. So this works

syntax "helloworld" : tactic
@[tactic tacticHelloworld] def elabHelloWorld : Lean.Elab.Tactic.Tactic
...