unexpected identifier while trying to define a tactic

Stream: new members

[Paweł Balawender]

Hey, I have a weird problem. I am trying to define my first tactic, so I pasted this example to an empty file (I have a lean project with mathlib in the parent directory):

meta def my_first_tactic : tactic unit := tactic.trace "Hello, World."

example : true :=
begin
  my_first_tactic,
  trivial
end

but it gives me just unexpected identifier; expected command error at the meta keyword. What am I doing wrong?

[Kevin Buzzard]

My guess: you're using an LLM to generate lean code instead of reading a book about the basics? That code you posted is lean 3 code.

[Paweł Balawender]

Ah yes, as if books never contain Lean 3 code: https://leanprover-community.github.io/extras/tactic_writing.html

[Paweł Balawender]

But that page being a wrong resource is a good piece of information, thanks - it's not clear from the banner on top of it that these examples won't work

[Eric Wieser]

Strictly speaking these examples do still work, but they have to be run in Lean 3 to do so!

[Kevin Buzzard]

Yes sorry, it looks like that page needs a complete rewrite :-/ Is it linked from somewhere else?

[Paweł Balawender]

Hm I landed on it from google search, so it might not be referred elsewhere. I will be happy to help rewriting it if we find no volunteer :) (I would surely be very slow because I'm not proficient in it, but maybe even translating these examples to Lean 4 while preserving the tutorial structure would be of help, and that I could probably do)

[Kevin Buzzard]

A lot of the lean 3 docs have been rewritten; the problem with that one is that the tactic framework has completely changed from Lean 3 to Lean 4, so the thing needs some attention from an expert (and many users of the system (e.g. me) do not know about metaprogramming at all, so are compeltely unable to take it on).

[Kyle Miller]

I just pushed some changes with an explicit warning about incompatibility.

For someone just coming to Lean 4 it's easy to miss that the languages are completely different. It's one of those things that goes without saying if you used to use Lean 3 (or Lean 2!)

[Derek Rhodes]

There is also a section on custom tactics in the new and improved language reference
https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Custom-Tactics/#custom-tactics

[Kyle Miller]

Thanks @Derek Rhodes, I added a link.